awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
    (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        Iso.symm (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i)))
this_1 :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
this : Q.IsLocal := ⋯
H₁ : Q (X := pullback g (S.affineCover.f i)) (pullback.snd g (S.affineCover.f i))
⊢ Q (X := pullback (S.affineCover.f i) g) (pullback.fst (S.affineCover.f i) g)

Tactic:
rw [← pullbackSymmetry_hom_comp_snd, Q.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
    (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        Iso.symm (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i)))
this_1 :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
this : Q.IsLocal := ⋯
⊢ Q (X := pullback g (S.affineCover.f i)) (pullback.snd g (S.affineCover.f i))

Tactic:
apply of_isPullback (.of_hasPullback _ _) H

Premises used: AlgebraicGeometry.HasAffineProperty.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
⊢ IsZariskiLocalAtSource P

Tactic:
.mk_of_iff ?_

Premises used: CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
refine :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ IsZariskiLocalAtSource P

Tactic:
refine .mk_of_iff ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
simp_rw :
  (∀ (i : (↑Y.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))) ↔
    ∀ (i : 𝒰.I₀) (i_1 : (↑Y.affineOpens : Type u)),
      P (X := (↑((𝒰.f i ≫ f) ⁻¹ᵁ (↑i_1 : Y.Opens)) : Scheme)) ((𝒰.f i ≫ f) ∣_ (↑i_1 : Y.Opens))
⊢ P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)

Tactic:
simp_rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top _ (iSup_affineOpens_eq_top Y)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
rw :
  (∀ (i : (↑Y.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))) ↔
    ∀ (b : (↑Y.affineOpens : Type u)) (a : 𝒰.I₀),
      P (X := (↑((𝒰.f a ≫ f) ⁻¹ᵁ (↑b : Y.Opens)) : Scheme)) ((𝒰.f a ≫ f) ∣_ (↑b : Y.Opens))
⊢ (∀ (i : (↑Y.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))) ↔
    ∀ (i : 𝒰.I₀) (i_1 : (↑Y.affineOpens : Type u)),
      P (X := (↑((𝒰.f i ≫ f) ⁻¹ᵁ (↑i_1 : Y.Opens)) : Scheme)) ((𝒰.f i ≫ f) ∣_ (↑i_1 : Y.Opens))

Tactic:
rw [forall_comm]

Premises used: forall_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
⊢ (∀ (i : (↑Y.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))) ↔
    ∀ (b : (↑Y.affineOpens : Type u)) (a : 𝒰.I₀),
      P (X := (↑((𝒰.f a ≫ f) ⁻¹ᵁ (↑b : Y.Opens)) : Scheme)) ((𝒰.f a ≫ f) ∣_ (↑b : Y.Opens))

Tactic:
forall_congr' fun U ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
refine :
  ∀ (U : (↑Y.affineOpens : Type u)),
    P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens)) ↔
      ∀ (a : 𝒰.I₀), P (X := (↑((𝒰.f a ≫ f) ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) ((𝒰.f a ≫ f) ∣_ (↑U : Y.Opens))
⊢ (∀ (i : (↑Y.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))) ↔
    ∀ (b : (↑Y.affineOpens : Type u)) (a : 𝒰.I₀),
      P (X := (↑((𝒰.f a ≫ f) ⁻¹ᵁ (↑b : Y.Opens)) : Scheme)) ((𝒰.f a ≫ f) ∣_ (↑b : Y.Opens))

Tactic:
refine forall_congr' fun U ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
U : (↑Y.affineOpens : Type u)
simp_rw :
  Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens)) ↔
    ∀ (a : 𝒰.I₀),
      Q (X := (↑((𝒰.f a ≫ f) ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (𝒰.f a ∣_ f ⁻¹ᵁ (↑U : Y.Opens) ≫ f ∣_ (↑U : Y.Opens))
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens)) ↔
    ∀ (a : 𝒰.I₀), P (X := (↑((𝒰.f a ≫ f) ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) ((𝒰.f a ≫ f) ∣_ (↑U : Y.Opens))

Tactic:
simp_rw [HasAffineProperty.iff_of_isAffine, morphismRestrict_comp]

Premises used: AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
U : (↑Y.affineOpens : Type u)
⊢ Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens)) ↔
    ∀ (a : 𝒰.I₀),
      Q (X := (↑((𝒰.f a ≫ f) ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (𝒰.f a ∣_ f ⁻¹ᵁ (↑U : Y.Opens) ≫ f ∣_ (↑U : Y.Opens))

Tactic:
@H _ _ (f ∣_ U.1) U.2 (Scheme.OpenCover.restrict 𝒰 (f ⁻¹ᵁ U.1))

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.OpenCover.restrict, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.restrict, Set.preimage, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.PresheafedSpace.restrict, Subtype.val, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.morphismRestrict, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
U : (↑Y.affineOpens : Type u)
⊢ Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens)) ↔
    ∀ (a : 𝒰.I₀),
      Q (X := (↑((𝒰.f a ≫ f) ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (𝒰.f a ∣_ f ⁻¹ᵁ (↑U : Y.Opens) ≫ f ∣_ (↑U : Y.Opens))

Tactic:
exact @H _ _ (f ∣_ U.1) U.2 (Scheme.OpenCover.restrict 𝒰 (f ⁻¹ᵁ U.1))

Premises used: AlgebraicGeometry.Scheme.OpenCover.restrict, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, Subtype.val, AlgebraicGeometry.morphismRestrict, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
⊢ (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
have : ∀ (this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤), P f
⊢ P f

Tactic:
have : (f ≫ g) ⁻¹ᵁ g.opensRange = ⊤ := by simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(↑(Scheme.Hom.opensRange g) : Scheme)) ⇑(Scheme.Hom.opensRange g).ι)
    (Set.range (ι := ↥Y) ⇑g)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
⊢ f =
    X.topIso.inv ≫
      (X.isoOfEq this).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom

Tactic:
simp [← cancel_mono g]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
⊢ f =
    X.topIso.inv ≫
      (X.isoOfEq this).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom

Tactic:
have : f = X.topIso.inv ≫ (X.isoOfEq this).inv ≫ (f ≫ g) ∣_ g.opensRange ≫
        (IsOpenImmersion.isoOfRangeEq g.opensRange.ι g (by simp)).hom := by
      simp [← cancel_mono g]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this_1 : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
this :
  f =
    X.topIso.inv ≫
      (X.isoOfEq this_1).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom
simp_rw : P (X := (↑((f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) ((f ≫ g) ∣_ Scheme.Hom.opensRange g)
⊢ P f

Tactic:
simp_rw [this, cancel_left_of_respectsIso (P := P), cancel_right_of_respectsIso (P := P)]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this_1 : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
this :
  f =
    X.topIso.inv ≫
      (X.isoOfEq this_1).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) ((f ≫ g) ∣_ Scheme.Hom.opensRange g)

Tactic:
H _ _ hfg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this_1 : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
this :
  f =
    X.topIso.inv ≫
      (X.isoOfEq this_1).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) ((f ≫ g) ∣_ Scheme.Hom.opensRange g)

Tactic:
exact H _ _ hfg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
⊢ P.HasOfPostcompProperty IsOpenImmersion

Tactic:
HasOfPostcompProperty.of_le P (.monomorphisms Scheme) (fun _ _ f _ ↦ inferInstanceAs (Mono f))

Premises used: CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_le, AlgebraicGeometry.Scheme, CategoryTheory.MorphismProperty.monomorphisms, _private.0.AlgebraicGeometry.instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange._proof_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
h :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y),
    IsClosedImmersion f ↔
      ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓
          @SurjectiveOnStalks)
        f
⊢ @IsClosedImmersion =
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓
      @SurjectiveOnStalks

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f ∧ SurjectiveOnStalks f ↔
    ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓
        @SurjectiveOnStalks)
      f
⊢ IsClosedImmersion f ↔
    ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓
        @SurjectiveOnStalks)
      f

Tactic:
rw [isClosedImmersion_iff, and_comm]

Premises used: and_comm, AlgebraicGeometry.isClosedImmersion_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f ∧ SurjectiveOnStalks f ↔
    ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓
        @SurjectiveOnStalks)
      f

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
rw :
  SurjectiveOnStalks f ∧ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f ↔
    IsPreimmersion f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
rw₁ :
  SurjectiveOnStalks f ∧ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f ↔
    (SurjectiveOnStalks f ∧ IsEmbedding (X := ↥X) (Y := ↥Y) ⇑f) ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
rw₂ :
  SurjectiveOnStalks f ∧ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f ↔
    SurjectiveOnStalks f ∧ IsEmbedding (X := ↥X) (Y := ↥Y) ⇑f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
rw₃ rw₄ :
  SurjectiveOnStalks f ∧ IsEmbedding (X := ↥X) (Y := ↥Y) ⇑f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f) ↔
    SurjectiveOnStalks f ∧ IsEmbedding (X := ↥X) (Y := ↥Y) ⇑f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
⊢ IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)

Tactic:
rw [isClosedImmersion_iff, isPreimmersion_iff, and_assoc, isClosedEmbedding_iff]

Premises used: Topology.isClosedEmbedding_iff, AlgebraicGeometry.isPreimmersion_iff, and_assoc, AlgebraicGeometry.isClosedImmersion_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsPreimmersion f
hf : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
⊢ IsClosedImmersion f

Tactic:
iff_isPreimmersion.mpr ⟨‹_›, hf⟩

Premises used: Iff.mpr, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
⊢ IsPreimmersion f

Tactic:
(iff_isPreimmersion.mp ‹_›).1

Premises used: AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, And.left, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsEmpty.{u + 1} ↥X
f : X ⟶ Y
rw : IsClosed.{u} (X := ↥Y) ∅
⊢ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)

Tactic:
rw [Set.range_eq_empty]

Premises used: Set.range_eq_empty
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsEmpty.{u + 1} ↥X
f : X ⟶ Y
⊢ IsClosed.{u} (X := ↥Y) ∅

Tactic:
isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsEmpty.{u + 1} ↥X
f : X ⟶ Y
⊢ IsClosed.{u} (X := ↥Y) ∅

Tactic:
exact isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion f
inst_1 : IsClosedImmersion g
⊢ IsClosedImmersion (f ≫ g)

Tactic:
MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
hprecomp : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z), IsClosedImmersion f → IsClosedImmersion (e.hom ≫ f)
hpostcomp : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y), IsClosedImmersion f → IsClosedImmersion (f ≫ e.hom)
⊢ MorphismProperty.RespectsIso @IsClosedImmersion

Tactic:
apply MorphismProperty.RespectsIso.mk

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
hf : IsClosedImmersion f
⊢ IsClosedImmersion (e.hom ≫ f)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
hf : IsClosedImmersion f
⊢ IsClosedImmersion (f ≫ e.hom)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
I : X.IdealSheafData
⊢ IsClosedImmersion I.subschemeι

Tactic:
.of_isPreimmersion _ (I.range_subschemeι ▸ I.support.isClosed)

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, TopologicalSpace.Closeds.isClosed, AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, Eq.rec, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
f : R ⟶ S
h :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
x : ↥(Spec S)
rw :
  RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)
⊢ (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)).RespectsIso

Tactic:
rw [← RingHom.toMorphismProperty_respectsIso_iff]

Premises used: RingHom.toMorphismProperty_respectsIso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
f : R ⟶ S
h :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
x : ↥(Spec S)
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
RingHom.surjective_respectsIso

Premises used: RingHom.surjective_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
f : R ⟶ S
h :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
x : ↥(Spec S)
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
exact RingHom.surjective_respectsIso

Premises used: RingHom.surjective_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
f : R ⟶ S
h :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
x : ↥(Spec S)
⊢ (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)).RespectsIso

Tactic:
haveI : (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f)).RespectsIso := by
      rw [← RingHom.toMorphismProperty_respectsIso_iff]
      exact RingHom.surjective_respectsIso