awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipal (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x x_1 : Associates ↥R⁰
⊢ Equiv.toFun (associatesNonZeroDivisorsEquivIsPrincipal R) (x * x_1) =
    Equiv.toFun (associatesNonZeroDivisorsEquivIsPrincipal R) x *
      Equiv.toFun (associatesNonZeroDivisorsEquivIsPrincipal R) x_1
have rw : HMul.hMul (α := Ideal R)
    (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
              x) :
          ↥(Ideal R)⁰) :
      Ideal R)
    (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
              x_1) :
          ↥(Ideal R)⁰) :
      Ideal R) =
  (↑(↑(HMul.hMul (α := ↥(isPrincipalNonZeroDivisorsSubmonoid R)) (β := ↥(isPrincipalNonZeroDivisorsSubmonoid R))
            ((associatesNonZeroDivisorsEquivIsPrincipal R :
                  (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                x :
              { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
            ((associatesNonZeroDivisorsEquivIsPrincipal R :
                  (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                x_1 :
              { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })) :
        ↥(Ideal R)⁰) :
    Ideal R)
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff, Equiv.toFun_as_coe,
      associatesNonZeroDivisorsEquivIsPrincipal_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipal (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
hI : I ≠ ⊥
x : R := IsPrincipal.generator I
⊢ x ≠ 0
have rwa : ¬x = 0
Tactic: rwa [Ne, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipal (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
hI : I ≠ ⊥
x : R := IsPrincipal.generator I
rwa : ¬x = 0
⊢ x ≠ 0
have rwa₁ : ¬I = ⊥
Tactic: rwa [Ne, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipal (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
h : I ≠ ⊥
⊢ Submodule.subtype I ∘ₗ (↑(isoBaseOfIsPrincipal h) : R →ₗ[R] ↥I) =
    (LinearMap.mul R R : (a : R) → R →ₗ[R] R) (IsPrincipal.generator I)
have h₁ : Eq (α := R) ((Submodule.subtype I ∘ₗ (↑(isoBaseOfIsPrincipal h) : R →ₗ[R] ↥I) : (a : R) → R) 1 : R)
  ((((LinearMap.mul R R : (a : R) → R →ₗ[R] R) (IsPrincipal.generator I) : R →ₗ[R] R) : (a : R) → R) 1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤
have hI : I = span {ϖ}
Tactic: have hI : I = Ideal.span {ϖ} := h.principal.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤
have hϖ : ϖ ^ n ∈ I ^ n
Tactic: have hϖ : ϖ ^ n ∈ I ^ n := hI ▸ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) n)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
x : R
⊢ Membership.mem (α := R) (I ^ n) ((HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n : (a : R) → R) x : R)
have simp : x * ϖ ^ n ∈ I ^ n
Tactic: simp only [LinearMap.pow_mulRight, LinearMap.mulRight_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
⊢ I = (f ∘ₗ g).ker
have h₁ : ∀ (x : R), x ∈ I ↔ x ∈ (f ∘ₗ g).ker
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
⊢ x ∈ I ↔ x ∈ (f ∘ₗ g).ker
have h₁ : x ∈ I ↔ x * ϖ ^ n ∈ I * I ^ n
Tactic: simp only [LinearMap.codRestrict, LinearMap.pow_mulRight, LinearMap.mulRight_apply,
      LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Submodule.mem_smul_top_iff, smul_eq_mul,
      f, g]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
⊢ x ∈ I ↔ x * ϖ ^ n ∈ I * I ^ n
have h₁ : x ∈ I → x * ϖ ^ n ∈ I * I ^ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
h₁ : x ∈ I → x * ϖ ^ n ∈ I * I ^ n
⊢ x ∈ I ↔ x * ϖ ^ n ∈ I * I ^ n
have h₂ : x * ϖ ^ n ∈ I * I ^ n → x ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
hx : x * ϖ ^ n ∈ I * I ^ n
⊢ x ∈ I
have hx₁ : ϖ ^ (n + 1) ∣ x * ϖ ^ n
Tactic: rw [← pow_succ', hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
hx : ϖ ^ (n + 1) ∣ x * ϖ ^ n
⊢ x ∈ I
have h₁ : ∀ (y : R) (hy : x * ϖ ^ n = ϖ ^ (n + 1) * y), x ∈ I
Tactic: obtain ⟨y, hy⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : x * ϖ ^ n = ϖ ^ (n + 1) * y
⊢ x ∈ I
have h₁ : ∀ (hy : x = ϖ * y), x ∈ I
Tactic: rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : x * ϖ ^ n = ϖ ^ (n + 1) * y
h₁ : ∀ (hy : x = ϖ * y), x ∈ I
⊢ x ∈ I
have rw : ∀ (hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)), ϖ ≠ 0
Tactic: rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : x = ϖ * y
⊢ x ∈ I
have h₁ : ϖ ∣ x
Tactic: rw [hI, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
⊢ ϖ ≠ 0
have contrapose : ∀ (h' : ϖ = 0), I = ⊥
Tactic: contrapose h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
h' : ϖ = 0
⊢ I = ⊥
have rw : Eq (α := Ideal R) (span {ϖ}) ⊥
Tactic: rw [hI, h', Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
h' : ϖ = 0
rw : Eq (α := Ideal R) (span {ϖ}) ⊥
⊢ I = ⊥
have rw₁ : Eq (α := Ideal R) (span {0}) ⊥
Tactic: rw [hI, h', Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
h' : ϖ = 0
rw : Eq (α := Ideal R) (span {ϖ}) ⊥
rw₁ : Eq (α := Ideal R) (span {0}) ⊥
⊢ I = ⊥
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [hI, h', Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤
have this : I = (f ∘ₗ g).ker
Tactic: have : I = LinearMap.ker (f.comp g) := by
    ext x
    simp only [LinearMap.codRestrict, LinearMap.pow_mulRight, LinearMap.mulRight_apply,
      LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Submodule.mem_smul_top_iff, smul_eq_mul,
      f, g]
    constructor <;> intro hx
    · exact Submodule.mul_mem_mul hx hϖ
    · rw [← pow_succ', hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
      obtain ⟨y, hy⟩ := hx
      rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy
      · rw [hI, Ideal.mem_span_singleton]
        exact ⟨y, hy⟩
      · contrapose h'
        rw [hI, h', Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤
have refine : Function.Surjective (α := R) (β := ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤)
  (⇑(f ∘ₗ g) : (a : R) → ↥(I ^ n) ⧸ I • ⊤)
Tactic: refine e.trans ((f.comp g).quotKerEquivOfSurjective ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
⊢ Function.Surjective (α := R) (β := ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤)
    (⇑(f ∘ₗ g) : (a : R) → ↥(I ^ n) ⧸ I • ⊤)
have refine : Function.Surjective (α := R) (β := ↥(I ^ n)) (⇑g : (a : R) → ↥(I ^ n))
Tactic: refine (Submodule.mkQ_surjective _).comp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx : x ∈ I ^ n
⊢ ∃ (a : R), (g : (a : R) → ↥(I ^ n)) a = Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx
have hx₁ : ϖ ^ n ∣ x
Tactic: rw [hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx_1 : x ∈ I ^ n
hx : ϖ ^ n ∣ x
⊢ ∃ (a : R), (g : (a : R) → ↥(I ^ n)) a = Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx_1
have refine : ∀ (a : R), x = ϖ ^ n * a → (g : (a : R) → ↥(I ^ n)) a = Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx_1
Tactic: refine hx.imp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
hp : maximalIdeal R ∈ I.minimalPrimes
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Ideal.IsMaximal (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J)
have h : Eq (α := Ideal R) (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J) (maximalIdeal R)
Tactic: convert! IsLocalRing.maximalIdeal.isMaximal R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
hp : maximalIdeal R ∈ I.minimalPrimes
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J) (maximalIdeal R)
have h : ∀ (hp : I.IsMinimalPrime (maximalIdeal R)) (J : Ideal (R ⧸ I)) (prime : J.IsPrime),
  Eq (α := Ideal R) (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J) (maximalIdeal R)
Tactic: rw [Ideal.minimalPrimes, Set.mem_setOf] at hp
Cleared hypotheses: J, prime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
hp_1 : maximalIdeal R ∈ I.minimalPrimes
hp : I.IsMinimalPrime (maximalIdeal R)
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J) (maximalIdeal R)
have this : Ideal.IsPrime (Ideal.comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)
Tactic: have := prime.comap (Ideal.Quotient.mk I)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
⊢ height (IsLocalRing.maximalIdeal R) ≤ 1
have refine : ∀ (q : Ideal R) (h₁ : q.IsPrime) (h₂ : q < IsLocalRing.maximalIdeal R), q.height < (↑1 : ℕ∞)
Tactic: refine Ideal.height_le_iff.mpr fun q h₁ h₂ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : q.height = 0
⊢ q.height < (↑1 : ℕ∞)
have rw : LT.lt (α := ℕ∞) 0 (↑1 : ℕ∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
⊢ q.height < (↑1 : ℕ∞)
have suffices : q.height = 0
Tactic: suffices q.height = 0 by rw [this]; exact zero_lt_one
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
⊢ q.height = 0
have rw : IsNilpotent (R := Ideal (Localization.AtPrime q))
  (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)
Tactic: rw [← WithBot.coe_inj,
    ← IsLocalization.AtPrime.ringKrullDim_eq_height q (Localization.AtPrime q),
    WithBot.coe_zero, ← ringKrullDimZero_iff_ringKrullDim_eq_zero,
    ← isArtinianRing_iff_krullDimLE_zero, isArtinianRing_iff_isNilpotent_maximalIdeal,
    ← Localization.AtPrime.map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
⊢ IsNilpotent (R := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)
have this : IsArtinianRing.{u_1} (R ⧸ I)
Tactic: have : IsArtinianRing (R ⧸ I) :=
    IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing I hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
⊢ IsNilpotent (R := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)
have obtain : ∀ (n : ℕ)
  (hn :
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
          ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
          ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)),
  IsNilpotent (R := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)
Tactic: obtain ⟨n, hn⟩ := IsArtinian.monotone_stabilizes qs