-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma ext_iff (f g : X.PartialMap Y) :
    f = g ↔ ∃ e : f.domain = g.domain, f.hom = (X.isoOfEq e).hom ≫ g.hom

Proof state:
case mp
X Y : Scheme
f g : X.PartialMap Y
⊢ f = g → ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
rintro rfl

Result:
case mp
X Y : Scheme
f : X.PartialMap Y
⊢ ∃ (e : f.domain = f.domain), f.hom = (X.isoOfEq e).hom ≫ f.hom

Proof state:
case mpr.mk.mk.intro.e_hom
X Y : Scheme
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
hV : Dense ↑U
g : ↑U ⟶ Y
e :
  { domain := U, dense_domain := hU, hom := f }.hom =
    (X.isoOfEq ⋯).hom ≫ { domain := U, dense_domain := hV, hom := g }.hom
⊢ f = g

Tactic:
simpa using e

Result:
no goals

Proof state:
X Y : Scheme
f g : X.PartialMap Y
⊢ f = g ↔ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
constructor

Result:
case mp
X Y : Scheme
f g : X.PartialMap Y
⊢ f = g → ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

case mpr
X Y : Scheme
f g : X.PartialMap Y
⊢ (∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom) → f = g

Proof state:
case mpr.mk.mk.intro
X Y : Scheme
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
hV : Dense ↑U
g : ↑U ⟶ Y
e :
  { domain := U, dense_domain := hU, hom := f }.hom =
    (X.isoOfEq ⋯).hom ≫ { domain := U, dense_domain := hV, hom := g }.hom
⊢ { domain := U, dense_domain := hU, hom := f } = { domain := U, dense_domain := hV, hom := g }

Tactic:
congr 1

Result:
case mpr.mk.mk.intro.e_hom
X Y : Scheme
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
hV : Dense ↑U
g : ↑U ⟶ Y
e :
  { domain := U, dense_domain := hU, hom := f }.hom =
    (X.isoOfEq ⋯).hom ≫ { domain := U, dense_domain := hV, hom := g }.hom
⊢ f = g

Proof state:
case mpr.mk
X Y : Scheme
g : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
⊢ (∃ (e : { domain := U, dense_domain := hU, hom := f }.domain = g.domain),
      { domain := U, dense_domain := hU, hom := f }.hom = (X.isoOfEq e).hom ≫ g.hom) →
    { domain := U, dense_domain := hU, hom := f } = g

Tactic:
obtain ⟨V, hV, g⟩ := g

Result:
case mpr.mk.mk
X Y : Scheme
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
V : X.Opens
hV : Dense ↑V
g : ↑V ⟶ Y
⊢ (∃ (e : { domain := U, dense_domain := hU, hom := f }.domain = { domain := V, dense_domain := hV, hom := g }.domain),
      { domain := U, dense_domain := hU, hom := f }.hom =
        (X.isoOfEq e).hom ≫ { domain := V, dense_domain := hV, hom := g }.hom) →
    { domain := U, dense_domain := hU, hom := f } = { domain := V, dense_domain := hV, hom := g }

Proof state:
case mpr
X Y : Scheme
f g : X.PartialMap Y
⊢ (∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom) → f = g

Tactic:
obtain ⟨U, hU, f⟩ := f

Result:
case mpr.mk
X Y : Scheme
g : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
⊢ (∃ (e : { domain := U, dense_domain := hU, hom := f }.domain = g.domain),
      { domain := U, dense_domain := hU, hom := f }.hom = (X.isoOfEq e).hom ≫ g.hom) →
    { domain := U, dense_domain := hU, hom := f } = g

Proof state:
case mp
X Y : Scheme
f : X.PartialMap Y
⊢ ∃ (e : f.domain = f.domain), f.hom = (X.isoOfEq e).hom ≫ f.hom

Tactic:
simp only [exists_true_left, Scheme.isoOfEq_rfl, Iso.refl_hom, Category.id_comp]

Result:
no goals

Proof state:
case mpr.mk.mk
X Y : Scheme
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
V : X.Opens
hV : Dense ↑V
g : ↑V ⟶ Y
⊢ (∃ (e : { domain := U, dense_domain := hU, hom := f }.domain = { domain := V, dense_domain := hV, hom := g }.domain),
      { domain := U, dense_domain := hU, hom := f }.hom =
        (X.isoOfEq e).hom ≫ { domain := V, dense_domain := hV, hom := g }.hom) →
    { domain := U, dense_domain := hU, hom := f } = { domain := V, dense_domain := hV, hom := g }

Tactic:
rintro ⟨rfl : U = V, e⟩

Result:
case mpr.mk.mk.intro
X Y : Scheme
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
hV : Dense ↑U
g : ↑U ⟶ Y
e :
  { domain := U, dense_domain := hU, hom := f }.hom =
    (X.isoOfEq ⋯).hom ≫ { domain := U, dense_domain := hV, hom := g }.hom
⊢ { domain := U, dense_domain := hU, hom := f } = { domain := U, dense_domain := hV, hom := g }