-- Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean
lemma IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop
    [IsJointlySurjectivePreserving P] {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S} [HasPullback f g]
    (hf : P f) (x : X) (y : Y) (h : f.base x = g.base y) :
    ∃ a : ↑(pullback f g), (pullback.snd f g).base a = y

Proof state:
case h
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↑↑(pullback g f).toPresheafedSpace
ha : (ConcreteCategory.hom (pullback.fst g f).base) a = y
⊢ (ConcreteCategory.hom (pullback.snd f g).base) ((ConcreteCategory.hom (pullbackSymmetry f g).inv.base) a) = y

Tactic:
rwa [← Scheme.comp_base_apply, pullbackSymmetry_inv_comp_snd]

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g).base) a = y

Tactic:
obtain ⟨a, ha⟩ := exists_preimage_fst_triplet_of_prop hf y x h.symm

Result:
case intro
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↑↑(pullback g f).toPresheafedSpace
ha : (ConcreteCategory.hom (pullback.fst g f).base) a = y
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g).base) a = y

Proof state:
case intro
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↑↑(pullback g f).toPresheafedSpace
ha : (ConcreteCategory.hom (pullback.fst g f).base) a = y
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g).base) a = y

Tactic:
use (pullbackSymmetry f g).inv.base a

Result:
case h
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↑↑(pullback g f).toPresheafedSpace
ha : (ConcreteCategory.hom (pullback.fst g f).base) a = y
⊢ (ConcreteCategory.hom (pullback.snd f g).base) ((ConcreteCategory.hom (pullbackSymmetry f g).inv.base) a) = y

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) y
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g).base) a = y

Tactic:
let iso := pullbackSymmetry f g

Result:
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g).base) a = y

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g).base) a = y

Tactic:
haveI : HasPullback g f := hasPullback_symmetry f g

Result:
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g).base) a = y