CechH1ToH1_mk_eq_of_cechH1ToH1_pullbackAlong_mk_eq.lean

theorem adicValuation_le_one_iff_mem (v : Place K F) (f : F) :
    v.adicValuation f ≤ 1 ↔ f ∈ v.toValuationSubring

theorem mem_restrictAlong_iff (φ : F →ₐ[K] F₁) (hφ : φ.toRingHom.IsIntegral) (w : Place K F₁) (f :
  F) :
    f ∈ (w.restrictAlong φ hφ).toValuationSubring ↔ φ f ∈ w.toValuationSubring

theorem restrictAlong_id (hid : (AlgHom.id K F).toRingHom.IsIntegral) (v : Place K F) :
    v.restrictAlong (AlgHom.id K F) hid = v

theorem restrictAlong_injective_of_surjective (φ : F →ₐ[K] F₁) (hφ : φ.toRingHom.IsIntegral)
    (hsurj : Function.Surjective φ) : Function.Injective (fun w : Place K F₁ => w.restrictAlong φ
      hφ) := by
  intro w w' h
  apply Place.ext
  ext y
  obtain ⟨x, rfl⟩ := hsurj y
  rw [← mem_restrictAlong_iff φ hφ w x, ← mem_restrictAlong_iff φ hφ w' x]
  exact congrArg (fun v : Place K F => x ∈ v.toValuationSubring) h |>.to_iff

theorem _root_.AlgebraicCurve.cechH1ToH1_mk_eq_of_cechH1ToH1_pullbackAlong_mk_eq
    {K : Type*} {F F₁ : Type*} [Field K] [Field F] [Algebra K F] [Field F₁] [Algebra K F₁]
    (θ : F →ₐ[K] F₁) (hθ : θ.toRingHom.IsIntegral) (hbij : Function.Bijective θ)
    {S₀ S₁ : Set (Place K F)} (hS : S₀ ∪ S₁ = Set.univ)
    (a b : ↥(lSpaceOn (S₀ ∩ S₁) (0 : Divisor K F)))
    (h : cechH1ToH1 (preimage_restrictAlong_union_eq_univ θ hθ hS) 0
        (cechH1.pullbackAlong θ hθ S₀ S₁ (Submodule.Quotient.mk a)) =
      cechH1ToH1 (preimage_restrictAlong_union_eq_univ θ hθ hS) 0
        (cechH1.pullbackAlong θ hθ S₀ S₁ (Submodule.Quotient.mk b))) :
    cechH1ToH1 hS 0 (Submodule.Quotient.mk a) = cechH1ToH1 hS 0 (Submodule.Quotient.mk b)