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

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

Tactic:
use a, ha.right

Result:
no goals

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.snd f g).base) a ∈
    ⇑(ConcreteCategory.hom g.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom f.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 f.base) y = (ConcreteCategory.hom (pullback.fst f g ≫ f).base) a

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

Tactic:
ext x

Result:
case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑Y.toPresheafedSpace
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g).base) ↔
    x ∈ ⇑(ConcreteCategory.hom g.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom f.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 f.base) y = (ConcreteCategory.hom (pullback.fst f g ≫ f).base) a

Tactic:
simp

Result:
no goals

Proof state:
case h.refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↑↑Y.toPresheafedSpace
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g).base) →
    x ∈ ⇑(ConcreteCategory.hom g.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom f.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.snd f g).base) a ∈
    ⇑(ConcreteCategory.hom g.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom f.base)

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

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

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

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

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

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

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