-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
lemma range_map {X' Y' S' : Scheme.{u}} (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X')
    (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : f ≫ i₃ = i₁ ≫ f')
    (e₂ : g ≫ i₃ = i₂ ≫ g') [Mono i₃] :
    Set.range (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base =
      (pullback.fst f' g').base ⁻¹' Set.range i₁.base ∩
        (pullback.snd f' g').base ⁻¹' Set.range i₂.base

Proof state:
case h.mpr.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↑↑(pullback f' g').toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom i₁.base) x = (ConcreteCategory.hom (pullback.fst f' g').base) z
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom i₂.base) y = (ConcreteCategory.hom (pullback.snd f' g').base) z
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↑↑(pullback (pullback.fst f' g') i₁).toPresheafedSpace
hw₁ :
  (ConcreteCategory.hom (pullback.fst (pullback.fst f' g') i₁).base) w₁ = T₁.x ∧
    (ConcreteCategory.hom (pullback.snd (pullback.fst f' g') i₁).base) w₁ = T₁.y
T₂ : Triplet (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
⊢ z ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base)

Tactic:
obtain ⟨w₂, hw₂⟩ := T₂.exists_preimage

Result:
case h.mpr.intro.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↑↑(pullback f' g').toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom i₁.base) x = (ConcreteCategory.hom (pullback.fst f' g').base) z
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom i₂.base) y = (ConcreteCategory.hom (pullback.snd f' g').base) z
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↑↑(pullback (pullback.fst f' g') i₁).toPresheafedSpace
hw₁ :
  (ConcreteCategory.hom (pullback.fst (pullback.fst f' g') i₁).base) w₁ = T₁.x ∧
    (ConcreteCategory.hom (pullback.snd (pullback.fst f' g') i₁).base) w₁ = T₁.y
T₂ : Triplet (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
w₂ : ↑↑(pullback (pullback.snd f' g') i₂).toPresheafedSpace
hw₂ :
  (ConcreteCategory.hom (pullback.fst (pullback.snd f' g') i₂).base) w₂ = T₂.x ∧
    (ConcreteCategory.hom (pullback.snd (pullback.snd f' g') i₂).base) w₂ = T₂.y
⊢ z ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base)

Proof state:
case h.mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↑↑(pullback f' g').toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom i₁.base) x = (ConcreteCategory.hom (pullback.fst f' g').base) z
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom i₂.base) y = (ConcreteCategory.hom (pullback.snd f' g').base) z
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
⊢ z ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base)

Tactic:
obtain ⟨w₁, hw₁⟩ := T₁.exists_preimage

Result:
case h.mpr.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↑↑(pullback f' g').toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom i₁.base) x = (ConcreteCategory.hom (pullback.fst f' g').base) z
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom i₂.base) y = (ConcreteCategory.hom (pullback.snd f' g').base) z
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↑↑(pullback (pullback.fst f' g') i₁).toPresheafedSpace
hw₁ :
  (ConcreteCategory.hom (pullback.fst (pullback.fst f' g') i₁).base) w₁ = T₁.x ∧
    (ConcreteCategory.hom (pullback.snd (pullback.fst f' g') i₁).base) w₁ = T₁.y
⊢ z ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base)

Proof state:
case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↑↑(pullback f' g').toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom i₁.base) x = (ConcreteCategory.hom (pullback.fst f' g').base) z
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom i₂.base) y = (ConcreteCategory.hom (pullback.snd f' g').base) z
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↑↑(pullback (pullback.fst f' g') i₁).toPresheafedSpace
hw₁ :
  (ConcreteCategory.hom (pullback.fst (pullback.fst f' g') i₁).base) w₁ = T₁.x ∧
    (ConcreteCategory.hom (pullback.snd (pullback.fst f' g') i₁).base) w₁ = T₁.y
T₂ : Triplet (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
w₂ : ↑↑(pullback (pullback.snd f' g') i₂).toPresheafedSpace
hw₂ :
  (ConcreteCategory.hom (pullback.fst (pullback.snd f' g') i₂).base) w₂ = T₂.x ∧
    (ConcreteCategory.hom (pullback.snd (pullback.snd f' g') i₂).base) w₂ = T₂.y
T : Triplet (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) := Triplet.mk' w₁ w₂ ⋯
t : ↑↑(pullback (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)).toPresheafedSpace
left✝ :
  (ConcreteCategory.hom
        (pullback.fst (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)).base)
      t =
    T.x
ht₂ :
  (ConcreteCategory.hom
        (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)).base)
      t =
    T.y
⊢ (ConcreteCategory.hom
        (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) ≫
            pullback.fst (pullback.snd f' g') i₂).base)
      t =
    z

Tactic:
simp [ht₂, T, hw₂.left, T₂]

Result:
no goals

Proof state:
case h.mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↑↑(pullback f' g').toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom i₁.base) x = (ConcreteCategory.hom (pullback.fst f' g').base) z
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom i₂.base) y = (ConcreteCategory.hom (pullback.snd f' g').base) z
⊢ z ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base)

Tactic:
let T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x hx.symm

Result:
case h.mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↑↑(pullback f' g').toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom i₁.base) x = (ConcreteCategory.hom (pullback.fst f' g').base) z
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom i₂.base) y = (ConcreteCategory.hom (pullback.snd f' g').base) z
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
⊢ z ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base)