-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma image_preimage_eq_preimage_image_of_isPullback {X Y U V : Scheme.{u}}
    {f : X ⟶ Y} {f' : U ⟶ V} {iU : U ⟶ X} {iV : V ⟶ Y} [IsOpenImmersion iV] [IsOpenImmersion iU]
    (H : IsPullback f' iU iV f) (W : V.Opens) : iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W

Proof state:
case neg.mp.intro.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑U.toPresheafedSpace
hx✝ : x ∈ ↑(f' ⁻¹ᵁ W)
hx : (ConcreteCategory.hom (Scheme.Hom.toLRSHom iU).base) x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ (ConcreteCategory.hom (Scheme.Hom.toLRSHom iU).base) x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
cases hx ⟨x, rfl⟩

Result:
no goals

Proof state:
case neg.mpr.intro.intro.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↑↑V.toPresheafedSpace
hy : y ∈ ↑W
x : ↑↑(pullback iV f).toPresheafedSpace
hx : (ConcreteCategory.hom (H.isoPullback.inv ≫ iU).base) x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
e : (ConcreteCategory.hom iV.base) y = (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.snd iV f).base) x)
⊢ (ConcreteCategory.hom (pullback.snd iV f).base) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
cases hx ⟨_, rfl⟩

Result:
no goals

Proof state:
case pos
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
obtain ⟨x, rfl⟩ := hx

Result:
case pos.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑U.toPresheafedSpace
⊢ (ConcreteCategory.hom iU.base) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ (ConcreteCategory.hom iU.base) x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Proof state:
case neg
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
constructor

Result:
case neg.mp
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) → x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W) → x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Proof state:
case neg.mp
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) → x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case neg.mp.intro.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑U.toPresheafedSpace
hx✝ : x ∈ ↑(f' ⁻¹ᵁ W)
hx : (ConcreteCategory.hom (Scheme.Hom.toLRSHom iU).base) x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ (ConcreteCategory.hom (Scheme.Hom.toLRSHom iU).base) x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Proof state:
case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W) → x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
rintro ⟨y, hy, e : iV.base y = f.base x⟩

Result:
case neg.mpr.intro.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
y : ↑↑V.toPresheafedSpace
hy : y ∈ ↑W
e : (ConcreteCategory.hom iV.base) y = (ConcreteCategory.hom f.base) x
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Proof state:
case pos.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑U.toPresheafedSpace
⊢ (ConcreteCategory.hom f'.base) x ∈ W ↔
    (ConcreteCategory.hom (f' ≫ iV).base) x ∈ (fun a => (ConcreteCategory.hom (Scheme.Hom.toLRSHom iV).base) a) '' ↑W

Tactic:
simp only [Scheme.comp_coeBase, TopCat.comp_app,
  iV.isOpenEmbedding.injective.mem_set_image, SetLike.mem_coe]

Result:
no goals

Proof state:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
⊢ iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W

Tactic:
ext x

Result:
case h.h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Proof state:
case neg.mpr.intro.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
y : ↑↑V.toPresheafedSpace
hy : y ∈ ↑W
e : (ConcreteCategory.hom iV.base) y = (ConcreteCategory.hom f.base) x
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
obtain ⟨x, rfl⟩ := (IsOpenImmersion.range_pullback_snd_of_left iV f).ge ⟨y, e⟩

Result:
case neg.mpr.intro.intro.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↑↑V.toPresheafedSpace
hy : y ∈ ↑W
x : ↑↑(pullback iV f).toPresheafedSpace
hx : (ConcreteCategory.hom (pullback.snd iV f).base) x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
e : (ConcreteCategory.hom iV.base) y = (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.snd iV f).base) x)
⊢ (ConcreteCategory.hom (pullback.snd iV f).base) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Proof state:
case h.h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
by_cases hx : x ∈ Set.range iU.base

Result:
case pos
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

case neg
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)