-- 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
⊢ z ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base)

Tactic:
let T₂ : Triplet (pullback.snd f' g') i₂ := Triplet.mk' z y hy.symm

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
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)

Proof state:
case h.mp.intro.right
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₃
t : ↑↑(pullback f g).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base) t ∈
    ⇑(ConcreteCategory.hom (pullback.snd f' g').base) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂.base)

Tactic:
use (pullback.snd f g).base t

Result:
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₃
t : ↑↑(pullback f g).toPresheafedSpace
⊢ (ConcreteCategory.hom i₂.base) ((ConcreteCategory.hom (pullback.snd f g).base) t) =
    (ConcreteCategory.hom (pullback.snd f' g').base)
      ((ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base) t)

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.map f g f' g' i₁ i₂ i₃ e₁ e₂).base)
      ((ConcreteCategory.hom (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom.base) t) =
    z

Tactic:
rw [pullback_map_eq_pullbackFstFstIso_inv, ← Scheme.comp_base_apply, Iso.hom_inv_id_assoc]

Result:
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

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₃
t : ↑↑(pullback f g).toPresheafedSpace
⊢ (ConcreteCategory.hom i₁.base) ((ConcreteCategory.hom (pullback.fst f g).base) t) =
    (ConcreteCategory.hom (pullback.fst f' g').base)
      ((ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base) t)

Tactic:
rw [← Scheme.comp_base_apply, ← Scheme.comp_base_apply]

Result:
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₃
t : ↑↑(pullback f g).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst f g ≫ i₁).base) t =
    (ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ pullback.fst f' g').base) t