-- Mathlib/AlgebraicGeometry/ResidueField.lean
/-- A helper lemma to work with `AlgebraicGeometry.Scheme.SpecToEquivOfField`. -/
lemma SpecToEquivOfField_eq_iff {K : Type*} [Field K] {X : Scheme}
    {f₁ f₂ : Σ x : X.carrier, X.residueField x ⟶ .of K} :
    f₁ = f₂ ↔ ∃ e : f₁.1 = f₂.1, f₁.2 = (X.residueFieldCongr e).hom ≫ f₂.2

Proof state:
case mpr.mk.mk.intro
K : Type u_1
inst✝ : Field K
X : Scheme
f : ↑↑X.toPresheafedSpace
snd✝¹ snd✝ : X.residueField f ⟶ CommRingCat.of K
h : ⟨f, snd✝¹⟩.snd = (residueFieldCongr ⋯).hom ≫ ⟨f, snd✝⟩.snd
⊢ ⟨f, snd✝¹⟩ = ⟨f, snd✝⟩

Tactic:
simpa

Result:
no goals

Proof state:
case mp
K : Type u_1
inst✝ : Field K
X : Scheme
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)
⊢ f₁ = f₂ → ∃ (e : f₁.fst = f₂.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₂.snd

Tactic:
rintro rfl

Result:
case mp
K : Type u_1
inst✝ : Field K
X : Scheme
f₁ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)
⊢ ∃ (e : f₁.fst = f₁.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₁.snd

Proof state:
case mpr.mk
K : Type u_1
inst✝ : Field K
X : Scheme
f₂ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)
f : ↑↑X.toPresheafedSpace
snd✝ : X.residueField f ⟶ CommRingCat.of K
⊢ (∃ (e : ⟨f, snd✝⟩.fst = f₂.fst), ⟨f, snd✝⟩.snd = (residueFieldCongr e).hom ≫ f₂.snd) → ⟨f, snd✝⟩ = f₂

Tactic:
obtain ⟨g, _⟩ := f₂

Result:
case mpr.mk.mk
K : Type u_1
inst✝ : Field K
X : Scheme
f : ↑↑X.toPresheafedSpace
snd✝¹ : X.residueField f ⟶ CommRingCat.of K
g : ↑↑X.toPresheafedSpace
snd✝ : X.residueField g ⟶ CommRingCat.of K
⊢ (∃ (e : ⟨f, snd✝¹⟩.fst = ⟨g, snd✝⟩.fst), ⟨f, snd✝¹⟩.snd = (residueFieldCongr e).hom ≫ ⟨g, snd✝⟩.snd) →
    ⟨f, snd✝¹⟩ = ⟨g, snd✝⟩

Proof state:
case mpr
K : Type u_1
inst✝ : Field K
X : Scheme
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)
⊢ (∃ (e : f₁.fst = f₂.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₂.snd) → f₁ = f₂

Tactic:
obtain ⟨f, _⟩ := f₁

Result:
case mpr.mk
K : Type u_1
inst✝ : Field K
X : Scheme
f₂ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)
f : ↑↑X.toPresheafedSpace
snd✝ : X.residueField f ⟶ CommRingCat.of K
⊢ (∃ (e : ⟨f, snd✝⟩.fst = f₂.fst), ⟨f, snd✝⟩.snd = (residueFieldCongr e).hom ≫ f₂.snd) → ⟨f, snd✝⟩ = f₂

Proof state:
case mp
K : Type u_1
inst✝ : Field K
X : Scheme
f₁ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)
⊢ ∃ (e : f₁.fst = f₁.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₁.snd

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
X : Scheme
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)
⊢ f₁ = f₂ ↔ ∃ (e : f₁.fst = f₂.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₂.snd

Tactic:
constructor

Result:
case mp
K : Type u_1
inst✝ : Field K
X : Scheme
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)
⊢ f₁ = f₂ → ∃ (e : f₁.fst = f₂.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₂.snd

case mpr
K : Type u_1
inst✝ : Field K
X : Scheme
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)
⊢ (∃ (e : f₁.fst = f₂.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₂.snd) → f₁ = f₂

Proof state:
case mpr.mk.mk
K : Type u_1
inst✝ : Field K
X : Scheme
f : ↑↑X.toPresheafedSpace
snd✝¹ : X.residueField f ⟶ CommRingCat.of K
g : ↑↑X.toPresheafedSpace
snd✝ : X.residueField g ⟶ CommRingCat.of K
⊢ (∃ (e : ⟨f, snd✝¹⟩.fst = ⟨g, snd✝⟩.fst), ⟨f, snd✝¹⟩.snd = (residueFieldCongr e).hom ≫ ⟨g, snd✝⟩.snd) →
    ⟨f, snd✝¹⟩ = ⟨g, snd✝⟩

Tactic:
rintro ⟨(rfl : f = g), h⟩

Result:
case mpr.mk.mk.intro
K : Type u_1
inst✝ : Field K
X : Scheme
f : ↑↑X.toPresheafedSpace
snd✝¹ snd✝ : X.residueField f ⟶ CommRingCat.of K
h : ⟨f, snd✝¹⟩.snd = (residueFieldCongr ⋯).hom ≫ ⟨f, snd✝⟩.snd
⊢ ⟨f, snd✝¹⟩ = ⟨f, snd✝⟩