-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
lemma range_fst : Set.range (pullback.fst f g).base = f.base ⁻¹' Set.range g.base

Proof state:
case h.refine_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑X.toPresheafedSpace
x✝ : x ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom f.base) x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g).base)

Tactic:
obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' x y hy.symm)

Result:
case h.refine_2.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑X.toPresheafedSpace
x✝ : x ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom f.base) x
a : ↑↑(pullback f g).toPresheafedSpace
ha :
  (ConcreteCategory.hom (pullback.fst f g).base) a = (Triplet.mk' x y ⋯).x ∧
    (ConcreteCategory.hom (pullback.snd f g).base) a = (Triplet.mk' x y ⋯).y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g).base)

Proof state:
case h.refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑X.toPresheafedSpace
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g).base) →
    x ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
rintro ⟨a, rfl⟩

Result:
case h.refine_1.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↑↑(pullback f g).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst f g).base) a ∈
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Proof state:
case h.refine_2.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑X.toPresheafedSpace
x✝ : x ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom f.base) x
a : ↑↑(pullback f g).toPresheafedSpace
ha :
  (ConcreteCategory.hom (pullback.fst f g).base) a = (Triplet.mk' x y ⋯).x ∧
    (ConcreteCategory.hom (pullback.snd f g).base) a = (Triplet.mk' x y ⋯).y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g).base)

Tactic:
use a, ha.left

Result:
no goals

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g).base) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
ext x

Result:
case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑X.toPresheafedSpace
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g).base) ↔
    x ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Proof state:
case h.refine_1.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↑↑(pullback f g).toPresheafedSpace
⊢ ∃ y, (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom (pullback.snd f g ≫ g).base) a

Tactic:
simp

Result:
no goals

Proof state:
case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑X.toPresheafedSpace
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g).base) ↔
    x ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩

Result:
case h.refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑X.toPresheafedSpace
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g).base) →
    x ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

case h.refine_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑X.toPresheafedSpace
x✝ : x ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)
y : ↑↑Y.toPresheafedSpace
hy : (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom f.base) x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g).base)

Proof state:
case h.refine_1.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↑↑(pullback f g).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst f g).base) a ∈
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
simp only [Set.mem_preimage, Set.mem_range, ← Scheme.comp_base_apply, pullback.condition]

Result:
case h.refine_1.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↑↑(pullback f g).toPresheafedSpace
⊢ ∃ y, (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom (pullback.snd f g ≫ g).base) a