mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹'
      ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) '' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹'
      ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) '' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
x : ↥X
⊢ ∃ i, x ∈ Set.range ⇑(𝒰.f i)

Tactic:
]

Goal state after:
K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
x : ↥X
⊢ ∃ i, x ∈ Set.range ⇑(𝒰.f i)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
l : Y ⟶ X
hl : l ≫ f = g
⊢ g = g

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop f g).hom

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop f g).hom
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰 : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
x✝ : R ∈ (precoverage P).coverings X
x : ↥X
hR : ∀ (x : forget.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map f))
right✝ : R ∈ P.precoverage.coverings X
⊢ ∃ Y g, R g ∧ x ∈ Set.range ⇑g

Tactic:
]

Goal state after:
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰 : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
x✝ : R ∈ (precoverage P).coverings X
x : ↥X
hR : ∀ (x : forget.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map f))
right✝ : R ∈ P.precoverage.coverings X
⊢ ∃ Y g, R g ∧ x ∈ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) ''
      ⇑(ConcreteCategory.hom (pullback.snd g.base f.base)) ⁻¹' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom)

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) ''
      ⇑(ConcreteCategory.hom (pullback.snd g.base f.base)) ⁻¹' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : JointlySurjective K
𝒰 : Cover K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(𝒰.f i)) ∧ ∀ (i : 𝒰.I₀), Q (𝒰.f i)

Tactic:
]

Goal state after:
K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : JointlySurjective K
𝒰 : Cover K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(𝒰.f i)) ∧ ∀ (i : 𝒰.I₀), Q (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := obj, f := map }.f i)) ∧
    ∀ (i : { I₀ := J, X := obj, f := map }.I₀), P ({ I₀ := J, X := obj, f := map }.f i)

Tactic:
]

Goal state after:
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := obj, f := map }.f i)) ∧
    ∀ (i : { I₀ := J, X := obj, f := map }.I₀), P ({ I₀ := J, X := obj, f := map }.f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop g f).hom

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop g f).hom
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (pullback.snd f g).hom

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (pullback.snd f g).hom
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑f ∩ Set.range ⇑g = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑g ∩ Set.range ⇑f = Set.range ⇑g ∩ Set.range ⇑f

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y✝ Z : Scheme
𝒰✝ : Cover K X✝
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f✝) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑((𝒰.add f).f i)) ∧ ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)

Tactic:
]

Goal state after:
K : Precoverage Scheme
X✝ Y✝ Z : Scheme
𝒰✝ : Cover K X✝
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f✝) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑((𝒰.add f).f i)) ∧ ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right =
    limit.π (cospan f g ⋙ forget) right
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right =
    limit.π (cospan f g ⋙ forget) right
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: 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
y : ↥V
hy : y ∈ ↑W
x : ↥(pullback iV f)
hx : (H.isoPullback.inv ≫ iU) x ∉ Set.range ⇑iU
e : iV y = f ((pullback.snd iV f) x)
⊢ (pullback.snd iV f) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
]

Goal state after:
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
y : ↥V
hy : y ∈ ↑W
x : ↥(pullback iV f)
hx : (H.isoPullback.inv ≫ iU) x ∉ Set.range ⇑iU
e : iV y = f ((pullback.snd iV f) x)
⊢ (pullback.snd iV f) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover P X
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)) ∧
    ∀ (i : { I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.I₀),
      P ({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)

Tactic:
]

Goal state after:
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover P X
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)) ∧
    ∀ (i : { I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.I₀),
      P ({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right =
    limit.π (cospan f g ⋙ forget) right
⊢ PresheafedSpace.IsOpenImmersion
    ((preservesLimitIso forget (cospan f g)).hom ≫
      (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right =
    limit.π (cospan f g ⋙ forget) right
⊢ PresheafedSpace.IsOpenImmersion
    ((preservesLimitIso forget (cospan f g)).hom ≫
      (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
𝒰 : Cover (precoverage P) X
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.f i)) ∧
    ∀ (i : { I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.I₀),
      P ({ I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.f i)

Tactic:
]

Goal state after:
K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
𝒰 : Cover (precoverage P) X
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.f i)) ∧
    ∀ (i : { I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.I₀),
      P ({ I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.f i)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (pullback.fst g f).hom

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (pullback.fst g f).hom
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = Scheme.Hom.app f V

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ U

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ (Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv) ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ (Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv) ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left =
    limit.π (cospan g f ⋙ forget) left
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left =
    limit.π (cospan g f ⋙ forget) left
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ IsOpenImmersion f ∧ Epi f.base

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ IsOpenImmersion f ∧ Epi f.base
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Set.range ⇑f = Set.univ

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Set.range ⇑f = Set.univ
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left =
    limit.π (cospan g f ⋙ forget) left
⊢ PresheafedSpace.IsOpenImmersion
    ((preservesLimitIso forget (cospan g f)).hom ≫
      (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left =
    limit.π (cospan g f ⋙ forget) left
⊢ PresheafedSpace.IsOpenImmersion
    ((preservesLimitIso forget (cospan g f)).hom ≫
      (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) left ≫ f)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) left ≫ f)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) ≤ Hom.opensRange f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) ≤ Hom.opensRange f