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

Tactic:
simp

Result:
no goals

Proof state:
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
T : Triplet (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) := Triplet.mk' w₁ w₂ ⋯
⊢ z ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base)

Tactic:
obtain ⟨t, _, ht₂⟩ := T.exists_preimage

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

Proof state:
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
⊢ (ConcreteCategory.hom (pullback.fst (pullback.fst f' g') i₁).base) w₁ =
    (ConcreteCategory.hom (pullback.fst (pullback.snd f' g') i₂).base) w₂

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

Result:
no goals

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

Tactic:
constructor

Result:
case h.mp
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
⊢ z ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base) →
    z ∈
      ⇑(ConcreteCategory.hom (pullback.fst f' g').base) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁.base) ∩
        ⇑(ConcreteCategory.hom (pullback.snd f' g').base) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂.base)

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