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

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

Tactic:
let T : Triplet (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) :=
  Triplet.mk' w₁ w₂ <| by simp [hw₁.left, hw₂.left, T₁, T₂]

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

Proof state:
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)

Tactic:
rintro ⟨t, rfl⟩

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

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

Tactic:
intro ⟨⟨x, hx⟩, ⟨y, hy⟩⟩

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

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

Proof state:
case h.mp.intro.left
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.fst f' g').base) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁.base)

Tactic:
use (pullback.fst 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.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)