awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
⊢ ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
have obtain : ∀ (V : Opens ↥X) (hV : V ∈ X.affineOpens) (hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X))
  (hVU : V ≤ f ⁻¹ᵁ U), ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
Tactic: obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU : V ≤ f ⁻¹ᵁ U⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
⊢ g₁.base = g₂.base
have w : ∀ (x : ↥Z), Eq (α := ↥X) (g₁ x : ↥X) (g₂ x : ↥X)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this : IsDominant i
x_1 : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x_1 : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x_1 : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
x : ↥Z
⊢ Eq (α := ↥X) (g₁ x : ↥X) (g₂ x : ↥X)
have w : ∀ (x : ↥Z'), Eq (α := ↥X) (g₁ (i x : ↥Z) : ↥X) (g₂ (i x : ↥Z) : ↥X)
Tactic: obtain ⟨x, rfl⟩ := i.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this : g₁.base = g₂.base
⊢ ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
have obtain : ∀ (W : Opens ↥Z) (hW : W ∈ Z.affineOpens) (hxW : x ∈ (↑W : Set ↥Z)) (hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V),
  ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
Tactic: obtain ⟨_, ⟨W, hW, rfl⟩, hxW, hWV : W ≤ _⟩ := Z.isBasis_affineOpens.exists_subset_of_mem_open
    (And.intro hxV (by simpa [← this])) (g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V).isOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
⊢ ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
have refine : Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂
Tactic: refine ⟨W, hxW, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
⊢ Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂
have this₁ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
Tactic: have := f.formallyUnramified_appLE hU hV hVU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
⊢ W ≤ (g₁ ≫ f) ⁻¹ᵁ U
have grw : g₁ ⁻¹ᵁ f ⁻¹ᵁ U ≤ g₁ ⁻¹ᵁ f ⁻¹ᵁ U
Tactic: grw [hWV, inf_le_left, hVU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
⊢ Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂
have algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
Tactic: algebraize [(f.appLE U V hVU).hom,
    ((g₁ ≫ f).appLE U W (by grw [hWV, inf_le_left, hVU]; rfl)).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
ψ₁ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
⊢ Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂
have suffices : ψ₁ = ψ₂
Tactic: suffices ψ₁ = ψ₂ by
    simpa [ψ₁, ψ₂, -Iso.cancel_iso_hom_left, IsAffineOpen.isoSpec_hom] using
      congr(hW.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom ($this).toRingHom) ≫ hV.fromSpec)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
ψ₁ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
⊢ ψ₁ = ψ₂
have refine_1 : IsNilpotent (R := Ideal (↑Γ(Z, W) : Type u)) (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))
Tactic: refine Algebra.FormallyUnramified.ext' (i.app W).hom ?_ ψ₁ ψ₂ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
ψ₁ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
refine_1 : IsNilpotent (R := Ideal (↑Γ(Z, W) : Type u)) (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))
⊢ ψ₁ = ψ₂
have refine_2 : ∀ (x : (↑Γ(X, V) : Type u)),
  Eq (α := (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.app i W) : (a : (↑Γ(Z, W) : Type u)) → (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
        ((ψ₁ : (a : (↑Γ(X, V) : Type u)) → (↑Γ(Z, W) : Type u)) x : (↑Γ(Z, W) : Type u)) :
      (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.app i W) : (a : (↑Γ(Z, W) : Type u)) → (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
        ((ψ₂ : (a : (↑Γ(X, V) : Type u)) → (↑Γ(Z, W) : Type u)) x : (↑Γ(Z, W) : Type u)) :
      (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
Tactic: refine Algebra.FormallyUnramified.ext' (i.app W).hom ?_ ψ₁ ψ₂ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
ψ₁ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
⊢ IsNilpotent (R := Ideal (↑Γ(Z, W) : Type u)) (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))
have refine_1 : ∀ (n : ℕ) (hn : Scheme.Hom.ker i ^ n = 0),
  IsNilpotent (R := Ideal (↑Γ(Z, W) : Type u)) (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))
Tactic: obtain ⟨n, hn⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
⊢ FormallyUnramified f
have refine : ∀ {U : Y.Opens} {hU : IsAffineOpen U} {V : X.Opens} {hV : IsAffineOpen V} {hVU : V ≤ f ⁻¹ᵁ U},
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
Tactic: refine ⟨fun {U hU V hV hVU} ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
have refine : ∀ (R : Type u) (x : CommRing R) (x_1 : Algebra (↑Γ(Y, U) : Type u) R) (I : Ideal R) (hI : HPow.hPow (β := ℕ) I 2 = ⊥)
  (g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R)
  (hg₁g₂ :
    Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
      (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
      (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)),
  g₁ = g₂
Tactic: refine Algebra.FormallyUnramified.iff_comp_injective.mpr fun R _ _ I hI g₁ g₂ hg₁g₂ ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
⊢ g₁ = g₂
have hg₁ : Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
  (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
  (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
Tactic: have hg₁ : f.appLE U V hVU ≫ CommRingCat.ofHom g₁ = CommRingCat.ofHom (algebraMap _ R) :=
    CommRingCat.hom_ext g₁.comp_algebraMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
⊢ g₁ = g₂
have hg₂ : Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
  (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
  (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
Tactic: have hg₂ : f.appLE U V hVU ≫ CommRingCat.ofHom g₂ = CommRingCat.ofHom (algebraMap _ R) :=
    CommRingCat.hom_ext g₂.comp_algebraMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
hg₂ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
⊢ g₁ = g₂
have this₁ : Eq (α := Spec (CommRingCat.of R) ⟶ X)
  (Spec.map (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec)
  (Spec.map (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec)
Tactic: have := H (.of R) (.of (R ⧸ I)) (CommRingCat.ofHom (Ideal.Quotient.mkₐ Γ(Y, U) I))
    Ideal.Quotient.mk_surjective (by simpa)
    (Spec.map (CommRingCat.ofHom g₁) ≫ hV.fromSpec) (Spec.map (CommRingCat.ofHom g₂) ≫ hV.fromSpec)
    (by simp only [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, ← AlgHom.comp_toRingHom, *])
    (by simp only [Category.assoc, ← hU.SpecMap_appLE_fromSpec f hV hVU, ← Spec.map_comp_assoc, *])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
hg₂ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
this :
  Eq (α := Spec (CommRingCat.of R) ⟶ X)
    (Spec.map (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec)
    (Spec.map (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec)
⊢ g₁ = g₂
have this₁ : Eq (α := CommRingCat.of (↑(X.presheaf.1 (op V)) : Type u) ⟶ CommRingCat.of R)
  (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
  (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
Tactic: rw [cancel_mono, Spec.map_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
| f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
have enter : TopologicalSpace.Opens.map f.base
Tactic: enter [1]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
| TopologicalSpace.Opens.map f.base
have rw : TopologicalSpace.Opens.map (liftCoborder f ≫ (coborderRange f).ι).base
Tactic: rw [← f.liftCoborder_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
| f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
have enter : TopologicalSpace.Opens.map (liftCoborder f ≫ (coborderRange f).ι).base
Tactic: enter [1]; rw [← f.liftCoborder_ι]