awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
e : pullback (X := pullback f g) (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
⊢ Q (X :=
    PreZeroHypercover.X (S := pullback f g)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i :
      PreZeroHypercover.X (S := pullback f g)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
          i ⟶
        X.affineCover.X i)
have this₁ : e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g =
  Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i
Tactic: have : e.hom ≫ pullback.fst _ _ = X.affineCover.pullbackHom (pullback.fst _ _) i := by
    simp [e, Scheme.Cover.pullbackHom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this_1 : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
e : pullback (X := pullback f g) (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
this :
  e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g =
    Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i
⊢ Q (X :=
    PreZeroHypercover.X (S := pullback f g)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i :
      PreZeroHypercover.X (S := pullback f g)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
          i ⟶
        X.affineCover.X i)
have rw : Q (X := pullback (X.affineCover.f i ≫ f) g) (pullback.fst (X.affineCover.f i ≫ f) g)
Tactic: rw [← this, Q.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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
⊢ P (X := pullback f g) (pullback.fst f g)
have rw : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀),
  P (X := pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
    (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
Tactic: rw [P.iff_of_zeroHypercover_target (S.affineCover.pullback₁ f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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₀
⊢ 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)
have refine : pullback ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g ≅
  pullback (X := pullback f (S.affineCover.f i)) (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
Tactic: refine pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g _ ≪≫ ?_ ≪≫
          (pullbackRightPullbackFstIso (S.affineCover.f i) g
            (pullback.snd f (S.affineCover.f i))).symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (hypothesis)
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)))
⊢ P (X := pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
    (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
have this : 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)
Tactic: have : e.hom ≫ pullback.fst _ _ =
          pullback.snd (pullback.fst f g) ((S.affineCover.pullback₁ f).f i) := by
        simp [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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 :
  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)
⊢ P (X := pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
    (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
have rw : P (X :=
  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))
  (pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g))
Tactic: rw [← this, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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 :
  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)
⊢ P (X :=
    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))
    (pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g))
have H₁ : Q (X := pullback (S.affineCover.f i) g) (pullback.fst (S.affineCover.f i) g)
Tactic: apply HasAffineProperty.pullback_fst_of_right hP'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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 (S.affineCover.f i) g) (pullback.fst (S.affineCover.f i) g)
have H₁ : Q (X := pullback g (S.affineCover.f i)) (pullback.snd g (S.affineCover.f i))
Tactic: rw [← pullbackSymmetry_hom_comp_snd, Q.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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
have refine : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
Tactic: refine .mk_of_iff ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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
⊢ P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
have 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))
Tactic: simp_rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top _ (iSup_affineOpens_eq_top Y)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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))) ↔
    ∀ (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))
have 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))
Tactic: rw [forall_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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))
have 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))
Tactic: refine forall_congr' fun U ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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)
⊢ 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))
have 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))
Tactic: simp_rw [HasAffineProperty.iff_of_isAffine, morphismRestrict_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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)
⊢ P f
have have : ∀ (this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤), P f
Tactic: have : (f ≫ g) ⁻¹ᵁ g.opensRange = ⊤ := by simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (hypothesis)
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 = ⊤
⊢ P f
have this₁ : f =
  X.topIso.inv ≫
    (X.isoOfEq this).inv ≫
      (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g sorry).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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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 f
have simp_rw : P (X := (↑((f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) ((f ≫ g) ∣_ Scheme.Hom.opensRange g)
Tactic: simp_rw [this, cancel_left_of_respectsIso (P := P), cancel_right_of_respectsIso (P := P)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
⊢ @IsClosedImmersion =
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓
      @SurjectiveOnStalks
have h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y),
  IsClosedImmersion f ↔
    ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓
        @SurjectiveOnStalks)
      f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔
    ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓
        @SurjectiveOnStalks)
      f
have h : IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f ∧ SurjectiveOnStalks f ↔
  ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓
      @SurjectiveOnStalks)
    f
Tactic: rw [isClosedImmersion_iff, and_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
have rw : SurjectiveOnStalks f ∧ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f ↔
  IsPreimmersion f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
Tactic: rw [isClosedImmersion_iff, isPreimmersion_iff, and_assoc, isClosedEmbedding_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
⊢ IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
have rw₁ : SurjectiveOnStalks f ∧ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f ↔
  (SurjectiveOnStalks f ∧ IsEmbedding (X := ↥X) (Y := ↥Y) ⇑f) ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
Tactic: rw [isClosedImmersion_iff, isPreimmersion_iff, and_assoc, isClosedEmbedding_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
⊢ IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
have rw₂ : SurjectiveOnStalks f ∧ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f ↔
  SurjectiveOnStalks f ∧ IsEmbedding (X := ↥X) (Y := ↥Y) ⇑f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
Tactic: rw [isClosedImmersion_iff, isPreimmersion_iff, and_assoc, isClosedEmbedding_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
⊢ IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
have 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)
Tactic: rw [isClosedImmersion_iff, isPreimmersion_iff, and_assoc, isClosedEmbedding_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y : Scheme
inst : IsEmpty.{u + 1} ↥X
f : X ⟶ Y
⊢ IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
have rw : IsClosed.{u} (X := ↥Y) ∅
Tactic: rw [Set.range_eq_empty]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
⊢ MorphismProperty.RespectsIso @IsClosedImmersion
have hprecomp : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z), IsClosedImmersion f → IsClosedImmersion (e.hom ≫ f)
Tactic: apply MorphismProperty.RespectsIso.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
hprecomp : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z), IsClosedImmersion f → IsClosedImmersion (e.hom ≫ f)
⊢ MorphismProperty.RespectsIso @IsClosedImmersion
have hpostcomp : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y), IsClosedImmersion f → IsClosedImmersion (f ≫ e.hom)
Tactic: apply MorphismProperty.RespectsIso.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
have 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)
Tactic: rw [← RingHom.toMorphismProperty_respectsIso_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
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)
⊢ Function.Surjective (α := (↑((Spec R).presheaf.stalk ((Spec.map f) x)) : Type u_1)) (β :=
    (↑((Spec S).presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap (Spec.map f) x)) :
      (a : (↑((Spec R).presheaf.stalk ((Spec.map f) x)) : Type u_1)) → (↑((Spec S).presheaf.stalk x) : Type u_1))
have this : (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