awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
rw : IsUnit x ↔ IsLeftRegular x ∧ IsRightRegular x
rw₁ : IsUnit x ↔ IsUnit x ∧ IsRightRegular x
⊢ IsUnit x ↔ IsRegular x
have rw₂ : IsUnit x ↔ IsUnit x
Tactic: rw [isRegular_iff, ← isUnit_iff_isLeftRegular, and_iff_left_of_imp (·.isRegular.2)]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
a : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
⊢ IsUnit a
have rwa : IsRegular a
Tactic: rwa [isUnit_iff_isRegular, isRegular_iff_mem_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
a : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
⊢ IsUnit a
have rwa : IsRegular a
Tactic: rwa [isUnit_iff_isRegular_of_mulOpposite, isRegular_iff_mem_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
a : R
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid R) R⁰ a
have rw : IsRegular a ↔ Membership.mem (γ := Submonoid R) R⁰ a
Tactic: rw [isUnit_iff_isRegular, isRegular_iff_mem_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
a : R
rw : IsRegular a ↔ Membership.mem (γ := Submonoid R) R⁰ a
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid R) R⁰ a
have rw₁ : Membership.mem (γ := Submonoid R) R⁰ a ↔ Membership.mem (γ := Submonoid R) R⁰ a
Tactic: rw [isUnit_iff_isRegular, isRegular_iff_mem_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
a : R
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid R) R⁰ a
have rw : IsRegular a ↔ Membership.mem (γ := Submonoid R) R⁰ a
Tactic: rw [isUnit_iff_isRegular_of_mulOpposite, isRegular_iff_mem_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
a : R
rw : IsRegular a ↔ Membership.mem (γ := Submonoid R) R⁰ a
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid R) R⁰ a
have rw₁ : Membership.mem (γ := Submonoid R) R⁰ a ↔ Membership.mem (γ := Submonoid R) R⁰ a
Tactic: rw [isUnit_iff_isRegular_of_mulOpposite, isRegular_iff_mem_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
⊢ Eq (α := Submonoid R) (IsUnit.submonoid R : Submonoid R) (R⁰ : Submonoid R)
have h : ∀ (x : R),
  Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
⊢ Eq (α := Submonoid R) (IsUnit.submonoid R : Submonoid R) (R⁰ : Submonoid R)
have h : ∀ (x : R),
  Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
⊢ Eq (α := Submonoid R) (IsUnit.submonoid R : Submonoid R) (nonZeroDivisorsRight R : Submonoid R)
have h : ∀ (x : R),
  Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R : Submonoid R) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
x : R
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R : Submonoid R) x
have h : Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ IsRightRegular x
Tactic: rw [← isRightRegular_iff_mem_nonZeroDivisorsRight]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
⊢ Eq (α := Submonoid R) (IsUnit.submonoid R : Submonoid R) (nonZeroDivisorsLeft R : Submonoid R)
have h : ∀ (x : R),
  Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R : Submonoid R) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R : Submonoid R) x
have h : Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ IsLeftRegular x
Tactic: rw [← isLeftRegular_iff_mem_nonZeroDivisorsLeft]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
have have : ∀ (s : Finset { I : Ideal R // I.IsMaximal })
  (H :
    ∀ (a : { I : Ideal R // I.IsMaximal }),
      s.inf (Subtype.val (p := fun (I : Ideal R) ↦ I.IsMaximal)) ≤ (↑a : Ideal R)),
  Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
Tactic: have ⟨s, H⟩ := Finset.exists_inf_le (Subtype.val (p := fun I : Ideal R ↦ I.IsMaximal))
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
s : Finset { I : Ideal R // I.IsMaximal }
H : ∀ (a : { I : Ideal R // I.IsMaximal }), s.inf (Subtype.val (p := fun (I : Ideal R) ↦ I.IsMaximal)) ≤ (↑a : Ideal R)
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
have refine : ∀ (p : (↑{I : Ideal R | I.IsMaximal} : Type u_1)), p ∈ s
Tactic: refine Set.finite_def.2 ⟨s, fun p ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
s : Finset { I : Ideal R // I.IsMaximal }
H : ∀ (a : { I : Ideal R // I.IsMaximal }), s.inf (Subtype.val (p := fun (I : Ideal R) ↦ I.IsMaximal)) ≤ (↑a : Ideal R)
p : (↑{I : Ideal R | I.IsMaximal} : Type u_1)
⊢ p ∈ s
have have : ∀ (q : { I : Ideal R // I.IsMaximal }) (hq1 : q ∈ s) (hq2 : (↑q : Ideal R) ≤ (↑p : Ideal R)), p ∈ s
Tactic: have ⟨q, hq1, hq2⟩ := p.2.isPrime.inf_le'.mp (H p)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
s : Finset { I : Ideal R // I.IsMaximal }
H : ∀ (a : { I : Ideal R // I.IsMaximal }), s.inf (Subtype.val (p := fun (I : Ideal R) ↦ I.IsMaximal)) ≤ (↑a : Ideal R)
p : (↑{I : Ideal R | I.IsMaximal} : Type u_1)
q : { I : Ideal R // I.IsMaximal }
hq1 : q ∈ s
hq2 : (↑q : Ideal R) ≤ (↑p : Ideal R)
⊢ p ∈ s
have rwa : q ∈ s
Tactic: rwa [← Subtype.ext <| q.2.eq_of_le p.2.ne_top hq2]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
⊢ IsField R
have refine : ∀ {x : R} (hx : x ≠ 0), ∃ (b : R), x * b = 1
Tactic: refine ⟨Nontrivial.exists_pair_ne, mul_comm, fun {x} hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
⊢ ∃ (b : R), x * b = 1
have obtain : ∀ (n : ℕ) (y : R) (hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1), ∃ (b : R), x * b = 1
Tactic: obtain ⟨n, y, hy⟩ := IsArtinian.exists_pow_succ_smul_dvd x (1 : R)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1
⊢ x ^ n * (x * y - 1) = 0
have rw : x ^ n * (x * y) = x ^ n * 1
Tactic: rw [mul_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1
⊢ x ^ n * (x * y) = x ^ n * 1
have h : x ^ n * (x * y) = x ^ n.succ • y
Tactic: convert! hy using 1
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1
⊢ ∃ (b : R), x * b = 1
have hy₁ : x ^ n * (x * y - 1) = 0
Tactic: replace hy : x ^ n * (x * y - 1) = 0 := by
    rw [mul_sub, sub_eq_zero]
    convert! hy using 1
    simp [Nat.succ_eq_add_one, pow_add, mul_assoc]
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n * (x * y - 1) = 0
⊢ ∃ (b : R), x * b = 1
have hy₁ : x ^ n = 0 ∨ x * y = 1
Tactic: rw [mul_eq_zero, sub_eq_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
n : ℕ
⊢ HPow.hPow (α := Ideal R) (nilradical R) n = ⨅ (I : MaximalSpectrum R), I.asIdeal ^ n
have have : ∀ (this : Fintype (MaximalSpectrum R)),
  HPow.hPow (α := Ideal R) (nilradical R) n = ⨅ (I : MaximalSpectrum R), I.asIdeal ^ n
Tactic: have : Fintype (MaximalSpectrum R) := Fintype.ofFinite (MaximalSpectrum R)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
n : ℕ
this : Fintype (MaximalSpectrum R)
⊢ HPow.hPow (α := Ideal R) (nilradical R) n = ⨅ (I : MaximalSpectrum R), I.asIdeal ^ n
have rw : HPow.hPow (α := Ideal R) (iInf PrimeSpectrum.asIdeal) n = ⨅ x ∈ (↑Finset.univ : Set (MaximalSpectrum R)), x.asIdeal ^ n
Tactic: rw [← iInf_univ, ← Finset.coe_univ, PrimeSpectrum.nilradical_eq_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
n : ℕ
this : Fintype (MaximalSpectrum R)
⊢ HPow.hPow (α := Ideal R) (iInf PrimeSpectrum.asIdeal) n =
    ⨅ (x : MaximalSpectrum R), ⨅ (_ : Membership.mem (γ := Finset (MaximalSpectrum R)) Finset.univ x), x.asIdeal ^ n
have rw : HPow.hPow (α := Ideal R) (iInf PrimeSpectrum.asIdeal) n =
  HPow.hPow (α := Ideal R)
    (⨅ (i : MaximalSpectrum R), ⨅ (_ : Membership.mem (γ := Finset (MaximalSpectrum R)) Finset.univ i), i.asIdeal) n
Tactic: rw [← Ideal.prod_eq_iInf_of_pairwise_isCoprime fun I _ _ _ ↦ .pow ∘ I.isCoprime_of_ne,
    Finset.prod_pow, Ideal.prod_eq_iInf_of_pairwise_isCoprime fun I _ _ _ ↦ I.isCoprime_of_ne]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
⊢ IsNilpotent (R := Ideal R) (Ring.jacobson R)
have have : ∀ (n : ℕ)
  (hn :
    ∀ (m : ℕ),
      n ≤ m →
        Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
          (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := sorry } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
          (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := sorry } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)),
  IsNilpotent (R := Ideal R) (Ring.jacobson R)
Tactic: have ⟨n, hn⟩ := IsArtinian.monotone_stabilizes ⟨(Jac ^ ·), @Ideal.pow_le_pow_right _ _ _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
⊢ Jac * Jac ^ n = Jac ^ n
have rw : Jac ^ (n + 1) = Jac ^ n
Tactic: rw [← Ideal.IsTwoSided.pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
⊢ IsNilpotent (R := Ideal R) (Ring.jacobson R)
have hn₁ : Jac * Jac ^ n = Jac ^ n
Tactic: have hn : Jac * Jac ^ n = Jac ^ n := by
      rw [← Ideal.IsTwoSided.pow_succ]; exact (hn _ n.le_succ).symm
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
⊢ IsNilpotent (R := Ideal R) (Ring.jacobson R)
have h : HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
⊢ HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
have h : ∀ (ne : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0), False
Tactic: by_contra ne
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
⊢ False
have h : ∀ (N : Ideal R) (eq : Jac * N = N) (ne : N ≠ ⊥)
  (min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N), False
Tactic: have ⟨N, ⟨eq, ne⟩, min⟩ := wellFounded_lt.has_min {N | Jac * N = N ∧ N ≠ ⊥} ⟨_, hn, ne⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
⊢ Jac ^ Nat.zero * N = N
have rw : 1 * N = N
Tactic: rw [Jac.pow_zero, N.one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
rw : 1 * N = N
⊢ Jac ^ Nat.zero * N = N
have rw₁ : N = N
Tactic: rw [Jac.pow_zero, N.one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n_1 : ℕ
hn_1 :
  ∀ (m : ℕ),
    n_1 ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n_1 : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn_2 : Jac * Jac ^ n_1 = Jac ^ n_1
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n_1 = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
n : ℕ
hn : Jac ^ n * N = N
⊢ Jac ^ n.succ * N = N
have rwa : Jac ^ n * Jac * N = N
Tactic: rwa [Jac.pow_succ, mul_assoc, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n_1 : ℕ
hn_1 :
  ∀ (m : ℕ),
    n_1 ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n_1 : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn_2 : Jac * Jac ^ n_1 = Jac ^ n_1
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n_1 = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
n : ℕ
hn : Jac ^ n * N = N
rwa : Jac ^ n * Jac * N = N
⊢ Jac ^ n.succ * N = N
have rwa₁ : Jac ^ n * (Jac * N) = N
Tactic: rwa [Jac.pow_succ, mul_assoc, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
⊢ False
have this : Jac ^ n * N = N
Tactic: have : Jac ^ n * N = N := n.rec (by rw [Jac.pow_zero, N.one_mul])
      fun n hn ↦ by rwa [Jac.pow_succ, mul_assoc, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
x : R
⊢ I x ≤ Ideal.span {x}
have rw : I x ≤ LinearMap.range (LinearMap.toSpanSingleton R R x)
Tactic: rw [Ideal.span, LinearMap.span_singleton_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
⊢ False
have hI : ∀ (x : R), I x ≤ Ideal.span {x}
Tactic: have hI x : I x ≤ Ideal.span {x} := by
      rw [Ideal.span, LinearMap.span_singleton_eq_range]; exact LinearMap.map_le_range
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
⊢ ∃ x ∈ N, I x ≠ ⊥
have contrapose! : ∀ (ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥), N = ⊥
Tactic: contrapose! ne
Cleared hypotheses: ne
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥
⊢ N = ⊥
have rw : ∀ r ∈ Jac ^ n, ∀ s ∈ N, Membership.mem (γ := Ideal R) ⊥ (r * s)
Tactic: rw [← this, ← le_bot_iff, Ideal.mul_le]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn_2 : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥
ri : R
hi : ri ∈ Jac ^ n
rn : R
hn : rn ∈ N
⊢ Membership.mem (γ := Ideal R) ⊥ (ri * rn)
have rw : ri * rn ∈ I rn
Tactic: rw [← ne rn hn]