awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this_1 :
  IsClosedImmersion (X := (↑(pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱) : Scheme))
    (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this :
  IsImmersion (X := (↑(pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱) : Scheme))
    (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ≫ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι)
rwa :
  ∀
    (this :
      IsImmersion (Y := pullback.diagonalObj f)
        ((pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱).ι ≫ pullback.diagonal f)),
    IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
rwa₁ :
  ∀ (this : IsImmersion (X := (↑⊤ : Scheme)) (Y := pullback.diagonalObj f) (Scheme.Opens.ι ⊤ ≫ pullback.diagonal f)),
    IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have rwa₂ : ∀ (this : IsImmersion (Y := pullback.diagonalObj f) (X.topIso.hom ≫ pullback.diagonal f)),
  IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: rwa [morphismRestrict_ι, H, ← Scheme.topIso_hom,
    MorphismProperty.cancel_left_of_respectsIso (P := @IsImmersion)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this_1 :
  IsClosedImmersion (X := (↑(pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱) : Scheme))
    (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this :
  IsImmersion (X := (↑(pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱) : Scheme))
    (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ≫ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι)
rwa :
  ∀
    (this :
      IsImmersion (Y := pullback.diagonalObj f)
        ((pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱).ι ≫ pullback.diagonal f)),
    IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
rwa₁ :
  ∀ (this : IsImmersion (X := (↑⊤ : Scheme)) (Y := pullback.diagonalObj f) (Scheme.Opens.ι ⊤ ≫ pullback.diagonal f)),
    IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
rwa₂ :
  ∀ (this : IsImmersion (Y := pullback.diagonalObj f) (X.topIso.hom ≫ pullback.diagonal f)),
    IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have rwa₃ : ∀ (this : IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)),
  IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: rwa [morphismRestrict_ι, H, ← Scheme.topIso_hom,
    MorphismProperty.cancel_left_of_respectsIso (P := @IsImmersion)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X))
have rw : IsImmersion (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
  (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
    X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
Tactic: rw [← MorphismProperty.cancel_right_of_respectsIso @IsImmersion _ (prodIsoPullback X X).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
have h : Eq (α := X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
  (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
    X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
  (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
Tactic: convert! (inferInstance : IsImmersion (pullback.diagonal (terminal.from X)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ Eq (α := X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
have h : CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.fst (terminal.from X) (terminal.from X) :
      pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X) =
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
h :
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.fst (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X))
⊢ Eq (α := X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
have h₁ : CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.snd (terminal.from X) (terminal.from X) :
      pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X) =
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X)) (pullback.snd (terminal.from X) (terminal.from X))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
⊢ IsPullback (Hom.toImage f) (Hom.liftCoborder f) (Hom.imageι f) (Hom.coborderRange f).ι
have refine : (Hom.ker (Hom.imageι f)).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)
Tactic: refine (isPullback_of_isClosedImmersion _ _ _ _ (by simp) ?_).flip
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
⊢ (Hom.ker (Hom.imageι f)).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)
have rw : (Hom.ker f).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)
Tactic: rw [Hom.imageι, IdealSheafData.ker_subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
⊢ (Hom.ker f).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)
have h : ∀ (U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)),
  ((Hom.ker f).comap (Hom.coborderRange f).ι).ideal U = IdealSheafData.ideal (Hom.ker (Hom.liftCoborder f)) U
Tactic: ext U : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)
⊢ ((Hom.ker f).comap (Hom.coborderRange f).ι).ideal U = IdealSheafData.ideal (Hom.ker (Hom.liftCoborder f)) U
have h : Eq (α := Ideal (↑Γ((↑(Hom.coborderRange f) : Scheme), (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
  (RingHom.ker
    (CommRingCat.Hom.hom
      (𝟙 Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) ≫
        Hom.app f ((Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)))))
  (RingHom.ker (F :=
    (↑Γ((↑(Hom.coborderRange f) : Scheme), (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
      (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
Tactic: simp only [IdealSheafData.ideal_comap_of_isOpenImmersion, Opens.ι_appIso, Iso.refl_inv,
    Hom.ker_apply, RingHom.comap_ker, ← CommRingCat.hom_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)
⊢ Eq (α := Ideal (↑Γ((↑(Hom.coborderRange f) : Scheme), (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (RingHom.ker
      (CommRingCat.Hom.hom
        (𝟙 Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) ≫
          Hom.app f ((Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)))))
    (RingHom.ker (F :=
      (↑Γ((↑(Hom.coborderRange f) : Scheme), (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
        (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
      (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
have h : Eq (α := Ideal (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
  (RingHom.ker (F :=
    (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
      (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (RingHom.comp
      (CommRingCat.Hom.hom (Hom.app f ((Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
      (RingHom.id (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))))
  (RingHom.ker (F :=
    (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
      (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
Tactic: dsimp [Opens.toScheme_presheaf_obj]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)
⊢ Eq (α := Ideal (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (RingHom.ker (F :=
      (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
        (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
      (RingHom.comp
        (CommRingCat.Hom.hom (Hom.app f ((Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
        (RingHom.id (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))))
    (RingHom.ker (F :=
      (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
        (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
      (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
have h : Function.Injective (α :=
  (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u)) (β :=
  (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
  (⇑(CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))) :
    (a : (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u)) →
      (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
Tactic: rw [RingHomCompTriple.comp_eq, liftCoborder_app,
    CommRingCat.hom_comp, RingHom.ker_comp_of_injective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)
⊢ Function.Injective (α :=
    (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u)) (β :=
    (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (⇑(CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) :
      (a : (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u)) →
        (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
have h : Mono (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [← ConcreteCategory.mono_iff_injective_of_preservesPullback]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X Y Z S : Scheme
⊢ HasAffineProperty (@IsIntegralHom) (affineAnd fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.IsIntegral)
have rw : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y),
  IsIntegralHom f ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral
Tactic: rw [HasAffineProperty.affineAnd_iff _ RingHom.isIntegral_respectsIso
    RingHom.isIntegral_isStableUnderBaseChange.localizationPreserves.away
    RingHom.isIntegral_ofLocalizationSpan]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
⊢ IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral
have this : (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral).RespectsIso
Tactic: have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
this :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral).RespectsIso
⊢ IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral
have rw : RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type u_1)) (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)) ↔
  (CommRingCat.Hom.hom φ).IsIntegral
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom), and_iff_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
this :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral).RespectsIso
rw :
  RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type u_1)) (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)) ↔
    (CommRingCat.Hom.hom φ).IsIntegral
⊢ IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral
have rw₁ : IsAffine.{u_1} (Spec S)
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom), and_iff_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X_1 Y Z S U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsIntegralHom f
inst_1 : IsIntegralHom g
⊢ IsIntegralHom (X := U ⨿ V) (Limits.coprod.desc f g)
have refine : ∀ {R S T : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : CommRing T] (f : R →+* S) (g : R →+* T),
  f.IsIntegral → g.IsIntegral → (f.prod g).IsIntegral
Tactic: refine hasAffineProperty.coprodDesc_affineAnd RingHom.isIntegral_respectsIso ?_ _ _ ‹_› ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (hypothesis)
Goal:
X_1 Y Z S_1 U V X : Scheme
f_1 : U ⟶ X
g_1 : V ⟶ X
inst : IsIntegralHom f_1
inst_1 : IsIntegralHom g_1
R S T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
inst_4 : CommRing T
f : R →+* S
g : R →+* T
h : f.IsIntegral
h_1 : g.IsIntegral
⊢ RingHom.IsIntegral.{u, u} (R := R) (A := S × T) (f.prod g)
have algebraizeInst : let algInst := f.toAlgebra;
Algebra.IsIntegral R S
Tactic: algebraize [f, g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (hypothesis)
Goal:
X_1 Y Z S_1 U V X : Scheme
f_1 : U ⟶ X
g_1 : V ⟶ X
inst : IsIntegralHom f_1
inst_1 : IsIntegralHom g_1
R S T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
inst_4 : CommRing T
f : R →+* S
g : R →+* T
h : f.IsIntegral
h_1 : g.IsIntegral
algebraizeInst :
  let algInst := f.toAlgebra;
  Algebra.IsIntegral R S
⊢ RingHom.IsIntegral.{u, u} (R := R) (A := S × T) (f.prod g)
have algebraizeInst₁ : let algInst := g.toAlgebra;
Algebra.IsIntegral R T
Tactic: algebraize [f, g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X Y Z S : Scheme
f : X ⟶ Y
inst : IsIntegralHom f
⊢ UniversallyClosed f
have revert : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f], UniversallyClosed f
Tactic: revert X Y f ‹IsIntegralHom f›
Cleared hypotheses: X, Y, f, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S : Scheme
⊢ ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f], UniversallyClosed f
have rw : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [universally (@IsIntegralHom) f], (topologically @IsClosedMap).universally f
Tactic: rw [universallyClosed_eq, ← IsStableUnderBaseChange.universally_eq (P := @IsIntegralHom)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S : Scheme
⊢ ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [universally (@IsIntegralHom) f], (topologically @IsClosedMap).universally f
have a : @IsIntegralHom ≤ topologically @IsClosedMap
Tactic: apply universally_mono
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S X Y : Scheme
f : X ⟶ Y
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
have a : ∀
  (this :
    ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
      IsIntegralHom f → topologically (@IsClosedMap) f)
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f → topologically (@IsClosedMap) f
Tactic: wlog hY : ∃ R, Y = Spec R generalizing X Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S X Y : Scheme
f : X ⟶ Y
a :
  ∀
    (this :
      ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
        IsIntegralHom f → topologically (@IsClosedMap) f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f → topologically (@IsClosedMap) f
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
have wlog : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
  IsIntegralHom f → topologically (@IsClosedMap) f
Tactic: wlog hY : ∃ R, Y = Spec R generalizing X Y
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S X Y : Scheme
f : X ⟶ Y
this :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIntegralHom f → topologically (@IsClosedMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
have a : (∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsIntegralHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)) →
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    topologically @IsClosedMap (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := topologically _) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S X Y : Scheme
f : X ⟶ Y
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R), IsIntegralHom f → topologically (@IsClosedMap) f
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
have inr : ∀
  (this :
    ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
      IsIntegralHom f → topologically (@IsClosedMap) f)
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f → topologically (@IsClosedMap) f
Tactic: wlog hX : ∃ S, X = Spec S generalizing X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inr :
  ∀
    (this :
      ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
        IsIntegralHom f → topologically (@IsClosedMap) f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f → topologically (@IsClosedMap) f
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
have wlog : ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
  IsIntegralHom f → topologically (@IsClosedMap) f
Tactic: wlog hX : ∃ S, X = Spec S generalizing X
Cleared hypotheses: X, f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (hypothesis)
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this :
  ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
H : IsIntegralHom f
⊢ topologically (@IsClosedMap) f
have inst : IsAffine X
Tactic: have inst : IsAffine X := isAffine_of_isAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this :
  ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
H : IsIntegralHom f
inst : IsAffine X
⊢ topologically (@IsClosedMap) f
have inr : topologically (@IsClosedMap) (X.isoSpec.inv ≫ f)
Tactic: rw [← cancel_left_of_respectsIso (P := topologically _) X.isoSpec.inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (hypothesis)
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this :
  ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
H : IsIntegralHom f
inst : IsAffine X
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ f)
have H₁ : IsIntegralHom (X.isoSpec.inv ≫ f)
Tactic: rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S : Scheme
R : CommRingCat
X : Scheme
f : X ⟶ Spec R
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R), IsIntegralHom f → topologically (@IsClosedMap) f
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, hX