awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥U) ⇑iU) x
pos :
  ∀ (x : ↥U),
    Membership.mem (α := ↥X) (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) (iU x : ↥X) ↔
      Membership.mem (α := ↥X) (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X) (iU x : ↥X)
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)

Tactic:
obtain ⟨x, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥U
pos : Membership.mem (α := ↥X) (iU ''ᵁ f' ⁻¹ᵁ W) (iU x : ↥X) ↔ Membership.mem (α := ↥Y) (iV ''ᵁ W) ((f' ≫ iV) x : ↥Y)
⊢ Membership.mem (α := ↥X) (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) (iU x : ↥X) ↔
    Membership.mem (α := ↥X) (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X) (iU x : ↥X)

Tactic:
simp only [SetLike.mem_coe, Opens.map_coe, Set.mem_preimage, ← Scheme.Hom.comp_apply, ← H.w]

Premises used: TopologicalSpace.Opens.map_coe, AlgebraicGeometry.Scheme.Hom.comp_apply, SetLike.mem_coe, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, Set.mem_preimage
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥U
⊢ Membership.mem (α := ↥X) (iU ''ᵁ f' ⁻¹ᵁ W) (iU x : ↥X) ↔ Membership.mem (α := ↥Y) (iV ''ᵁ W) ((f' ≫ iV) x : ↥Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range (ι := ↥U) ⇑iU
neg : x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) → x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
neg₁ : x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X) → x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X)
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥U
hx_1 : x ∈ (↑(f' ⁻¹ᵁ W) : Set ↥U)
hx :
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom iU)).hom.base :
          (a : ↥U) → ↥X)
        x :
      ↥X) ∉
    Set.range (ι := ↥U) ⇑iU
⊢ Membership.mem (α := ↥X) (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom iU)).hom.base :
          (a : ↥U) → ↥X)
        x :
      ↥X)

Tactic:
cases hx ⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range (ι := ↥U) ⇑iU
y : ↥V
hy : y ∈ (↑W : Set ↥V)
e : Eq (α := ↥Y) (iV y : ↥Y) (f x : ↥Y)
neg :
  ∀ (x : ↥(pullback iV f)) (hx : ((pullback.snd iV f) x : ↥X) ∉ Set.range (ι := ↥U) ⇑iU)
    (e : Eq (α := ↥Y) (iV y : ↥Y) (f ((pullback.snd iV f) x : ↥X) : ↥Y)),
    Membership.mem (α := ↥X) (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ((pullback.snd iV f) x : ↥X)
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X)

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

Premises used: Eq.ge, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↥V
hy : y ∈ (↑W : Set ↥V)
x : ↥(pullback iV f)
hx : ((pullback.snd iV f) x : ↥X) ∉ Set.range (ι := ↥U) ⇑iU
e : Eq (α := ↥Y) (iV y : ↥Y) (f ((pullback.snd iV f) x : ↥X) : ↥Y)
⊢ ((Iso.inv H.isoPullback ≫ iU) x : ↥X) ∉ Set.range (ι := ↥U) ⇑iU

Tactic:
rw [← H.isoPullback_inv_snd] at hx

Premises used: CategoryTheory.IsPullback.isoPullback_inv_snd
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↥V
hy : y ∈ (↑W : Set ↥V)
x : ↥(pullback iV f)
hx : ((pullback.snd iV f) x : ↥X) ∉ Set.range (ι := ↥U) ⇑iU
e : Eq (α := ↥Y) (iV y : ↥Y) (f ((pullback.snd iV f) x : ↥X) : ↥Y)
hx₁ : ((Iso.inv H.isoPullback ≫ iU) x : ↥X) ∉ Set.range (ι := ↥U) ⇑iU
⊢ Eq (α := ↥Y) (iV y : ↥Y) (f ((pullback.snd iV f) x : ↥X) : ↥Y)

Tactic:
rw [← H.isoPullback_inv_snd] at hx

Premises used: CategoryTheory.IsPullback.isoPullback_inv_snd
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↥V
hy : y ∈ (↑W : Set ↥V)
x : ↥(pullback iV f)
hx : ((Iso.inv H.isoPullback ≫ iU) x : ↥X) ∉ Set.range (ι := ↥U) ⇑iU
e : Eq (α := ↥Y) (iV y : ↥Y) (f ((pullback.snd iV f) x : ↥X) : ↥Y)
⊢ Membership.mem (α := ↥X) (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ((pullback.snd iV f) x : ↥X)

Tactic:
cases hx ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Subset (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥X) ⇑f)
⊢ lift f g H' ≫ f = g

Tactic:
Scheme.Hom.ext' <| LocallyRingedSpace.IsOpenImmersion.lift_fac f.toLRSHom g.toLRSHom H'

Premises used: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac, AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.Scheme.Hom.ext'
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Subset (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥X) ⇑f)
l : Y ⟶ X
hl : l ≫ f = g
⊢ l = lift f g H'

Tactic:
Scheme.Hom.ext' <| LocallyRingedSpace.IsOpenImmersion.lift_uniq
    f.toLRSHom g.toLRSHom H' l.toLRSHom congr(($hl).toLRSHom)

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.Scheme.Hom.ext', congrArg, id, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_uniq
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H_1 : IsOpenImmersion f
Y' : Scheme
g' : Y' ⟶ Y
H : Subset (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥X) ⇑f)
⊢ Subset (α := Set ↥Z) (Set.range (ι := ↥Y') ⇑(g' ≫ g)) (Set.range (ι := ↥Y) ⇑g)

Tactic:
simp [Set.range_comp_subset_range]

Premises used: Set.range_comp_subset_range
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H_1 : IsOpenImmersion f
Y' : Scheme
g' : Y' ⟶ Y
H : Subset (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥X) ⇑f)
⊢ g' ≫ lift f g H = lift f (g' ≫ g) ⋯

Tactic:
simp [← cancel_mono f]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst : IsOpenImmersion g
H : Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥U) ⇑g)
⊢ IsPullback (lift g f H ≫ 𝟙 U) (𝟙 X) g (lift g f H ≫ g)

Tactic:
IsPullback.of_id_snd.paste_horiz (IsKernelPair.id_of_mono g)

Premises used: CategoryTheory.IsPullback.of_id_snd, CategoryTheory.IsKernelPair.id_of_mono, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst : IsOpenImmersion g
H : Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥U) ⇑g)
h : lift g f H = lift g f H ≫ 𝟙 U
h₁ : f = lift g f H ≫ g
convert_2 : X ⟶ U
⊢ IsPullback (lift g f H) (𝟙 X) g f

Tactic:
convert! IsPullback.of_id_snd.paste_horiz (IsKernelPair.id_of_mono g)

Premises used: CategoryTheory.IsPullback.of_id_snd, CategoryTheory.IsKernelPair.id_of_mono, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst : IsOpenImmersion g
H : Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥U) ⇑g)
⊢ lift g f H = lift g f H ≫ 𝟙 U

Tactic:
(Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst : IsOpenImmersion g
H : Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥U) ⇑g)
⊢ lift g f H = lift g f H ≫ 𝟙 U

Tactic:
exact (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst : IsOpenImmersion g
H : Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥U) ⇑g)
⊢ f = lift g f H ≫ g

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
e : Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
rw : (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f
⊢ lift g f ⋯ ≫ lift f g ⋯ = 𝟙 X

Tactic:
rw [← cancel_mono f]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
e : Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
e : Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
rw : (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g
⊢ lift f g ⋯ ≫ lift g f ⋯ = 𝟙 Y

Tactic:
rw [← cancel_mono g]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
e : Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
e : Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
⊢ (isoOfRangeEq f g e).hom ≫ g = f

Tactic:
lift_fac _ _ (le_of_eq e)

Premises used: le_of_eq, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
e : Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
⊢ (isoOfRangeEq f g e).inv ≫ f = g

Tactic:
lift_fac _ _ (le_of_eq e.symm)

Premises used: le_of_eq, Eq.symm, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
fg : Y ⟶ X
H : fg = f ≫ g
h : IsOpenImmersion g
V : U.Opens
⊢ f ⁻¹ᵁ V = fg ⁻¹ᵁ g ''ᵁ V

Tactic:
simp_all
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
fg : Y ⟶ X
H : fg = f ≫ g
h : IsOpenImmersion g
V : U.Opens
subst :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app fg (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
subst H
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U : Scheme
f : U ⟶ Y
g : X ⟶ Y
inst : IsOpenImmersion f
H : Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑g) (Set.range (ι := ↥U) ⇑f)
V : U.Opens
⊢ Scheme.Hom.app (lift f g H) V =
    CategoryStruct.comp (Y := Γ(Y, f ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso f V))
      (Scheme.Hom.app g (f ''ᵁ V) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq _ _ _ (lift_fac _ _ _).symm _

Premises used: AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, Eq.symm, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst : IsOpenImmersion iU
inst_1 : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(pullback iV f)) ⇑(pullback.snd iV f)) (Set.range (ι := ↥U) ⇑iU)

Tactic:
simpa [range_pullbackSnd] using congr(($H').1)

Premises used: AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst : IsOpenImmersion iU
inst_1 : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
e : pullback iV f ≅ U := isoOfRangeEq (pullback.snd iV f) iU ⋯
⊢ e.inv ≫ pullback.snd iV f = iU ≫ 𝟙 X

Tactic:
simp [e]
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst : IsOpenImmersion iU
inst_1 : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
e : pullback iV f ≅ U := isoOfRangeEq (pullback.snd iV f) iU ⋯
h : g = e.inv ≫ pullback.fst iV f
⊢ IsPullback g iU iV f

Tactic:
convert!
    (IsPullback.of_horiz_isIso
          (show CommSq e.inv iU (pullback.snd iV f) (𝟙 X) from ⟨by simp [e]⟩)).paste_horiz
      (IsPullback.of_hasPullback iV f)

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.paste_horiz, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst : IsOpenImmersion iU
inst_1 : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
e : pullback iV f ≅ U := isoOfRangeEq (pullback.snd iV f) iU ⋯
⊢ g = e.inv ≫ pullback.fst iV f

Tactic:
simp [← cancel_mono iV, e, pullback.condition, H]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
H : IsOpenImmersion f_1
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion f
U : Y.Opens
rw : f ⁻¹ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ f ⁻¹ᵁ U
rw₁ rw₂ : f ⁻¹ᵁ U ≤ f ⁻¹ᵁ U
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ (Scheme.Hom.opensRange f ⊓ U)

Tactic:
rw [← f.image_preimage_eq_opensRange_inf, f.preimage_image_eq]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.Scheme.Hom.preimage_image_eq
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
⊢ Eq (α := Γ(Y, Scheme.Hom.opensRange f ⊓ U) ⟶ Γ(X, f ⁻¹ᵁ U)) (Iso.inv (ΓIso f U))
    (Scheme.Hom.appLE f (Scheme.Hom.opensRange f ⊓ U) (f ⁻¹ᵁ U) ⋯)

Tactic:
simp only [ΓIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv, eqToHom_op,
    Iso.symm_inv, Scheme.Hom.appIso_hom', Scheme.Hom.map_appLE]

Premises used: CategoryTheory.Iso.op_inv, AlgebraicGeometry.IsOpenImmersion.ΓIso, CategoryTheory.Iso.symm_inv, AlgebraicGeometry.Scheme.Hom.appIso_hom', CategoryTheory.eqToHom_op, CategoryTheory.Functor.mapIso_inv, AlgebraicGeometry.Scheme.Hom.map_appLE, CategoryTheory.Iso.trans_inv, CategoryTheory.eqToIso.inv
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
⊢ CategoryStruct.comp (Y := Y.presheaf.obj (op (Scheme.Hom.opensRange f ⊓ U)))
      (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (Iso.inv (ΓIso f U)) =
    Scheme.Hom.app f U

Tactic:
simp [Scheme.Hom.appLE_eq_app]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE_eq_app
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
rw :
  Eq (α := Γ(Y, U) ⟶ Γ(Y, Scheme.Hom.opensRange f ⊓ U))
    (CategoryStruct.comp (Y := Y.presheaf.obj (op (Scheme.Hom.opensRange f ⊓ U)))
        (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (Iso.inv (ΓIso f U)) ≫
      Iso.hom (ΓIso f U))
    (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α := Γ(Y, U) ⟶ Γ(Y, Scheme.Hom.opensRange f ⊓ U)) (Scheme.Hom.app f U ≫ Iso.hom (ΓIso f U))
    (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rw [← map_ΓIso_inv]

Premises used: AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
⊢ Eq (α := Γ(Y, U) ⟶ Γ(Y, Scheme.Hom.opensRange f ⊓ U))
    (CategoryStruct.comp (Y := Y.presheaf.obj (op (Scheme.Hom.opensRange f ⊓ U)))
        (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (Iso.inv (ΓIso f U)) ≫
      Iso.hom (ΓIso f U))
    (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp [-ΓIso_inv]

Premises used: AlgebraicGeometry.IsOpenImmersion.ΓIso_inv
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z_1 : Scheme
f_1 : X ⟶ Z_1
g_1 : Y ⟶ Z_1
H : IsOpenImmersion f_1
Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsOpenImmersion f
H' : Subset (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥X) ⇑f)
inst_2 : IsOpenImmersion g
⊢ IsOpenImmersion (lift f g H' ≫ f)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
rw : IsOpenImmersion f ∧ Epi f.base
⊢ IsIso f

Tactic:
rw [isIso_iff_isOpenImmersion_and_epi_base]

Premises used: AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ IsOpenImmersion f ∧ Epi f.base

Tactic:
⟨inferInstance, ?_⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
refine : Epi f.base
⊢ IsOpenImmersion f ∧ Epi f.base

Tactic:
refine ⟨inferInstance, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
rw : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ
⊢ Epi f.base

Tactic:
rw [TopCat.epi_iff_surjective, ← Set.range_eq_univ]

Premises used: Set.range_eq_univ, TopCat.epi_iff_surjective
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ

Tactic:
TopologicalSpace.Opens.ext_iff.mp hf

Premises used: Set.univ, setOf, Iff.mp, Set.range, TopologicalSpace.Opens.ext_iff
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ

Tactic:
exact TopologicalSpace.Opens.ext_iff.mp hf

Premises used: Iff.mp, TopologicalSpace.Opens.ext_iff
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
hP : MorphismProperty.isomorphisms Scheme ≤ IsOpenImmersion
⊢ IsOpenImmersion.RespectsIso

Tactic:
apply MorphismProperty.respectsIso_of_isStableUnderComposition

Premises used: CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : Scheme
hP : ∀ ⦃Y : Scheme.{u_1}⦄ (f : X ⟶ Y), MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f
⊢ ∀ ⦃Y : Scheme.{u_1}⦄ (f : X ⟶ Y), MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
hP : ∀ (hf : IsIso f), IsOpenImmersion f
⊢ MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f

Tactic:
(hf : IsIso f)
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
hf : IsIso f
⊢ IsIso f

Tactic:
have : IsIso f := hf
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
hf this : IsIso f
⊢ IsOpenImmersion f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
_ : ∀ [inst : HasPullback f g], IsOpenImmersion g → IsOpenImmersion (X := pullback f g) (pullback.fst f g)
⊢ ∀ [inst : HasPullback f g], IsOpenImmersion g → IsOpenImmersion (X := pullback f g) (pullback.fst f g)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
H : IsOpenImmersion g
⊢ IsOpenImmersion (X := pullback f g) (pullback.fst f g)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    X.basicOpen (U := f ⁻¹ᵁ f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, f ''ᵁ U)) (Hom.app f (f ''ᵁ U)) :
          (a : (↑Γ(Y, f ''ᵁ U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
            r :
          (↑Γ(Y, f ''ᵁ U) : Type u)))

Tactic:
have e := Scheme.preimage_basicOpen f ((f.appIso U).inv r)