awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
s : Finset ι
hI : ∀ i ∈ s, (I i).FG
hI' : ∀ i ∈ s, Finite.{u_1 + 1} (R ⧸ I i)
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
have empty : ∀ (hI : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (I i).FG)
  (hI' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Finite.{u_1 + 1} (R ⧸ I i)),
  Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ ∅, I i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, one_eq_top]; infer_instance
  | insert a s has IH =>
    rw [Finset.prod_insert has, mul_comm]
    have := hI' a (by simp)
    have := IH (fun i hi ↦ hI _ (by simp [hi])) (fun i hi ↦ hI' _ (by simp [hi]))
    exact Submodule.finite_quotient_smul _ (hI a (by simp))
Cleared hypotheses: s, hI, hI'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
s : Finset ι
hI : ∀ i ∈ s, (I i).FG
hI' : ∀ i ∈ s, Finite.{u_1 + 1} (R ⧸ I i)
empty :
  ∀ (hI : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (I i).FG)
    (hI' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Finite.{u_1 + 1} (R ⧸ I i)),
    Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ ∅, I i))
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (IH :
    ∀ (hI : ∀ i ∈ s, (I i).FG) (hI' : ∀ i ∈ s, Finite.{u_1 + 1} (R ⧸ I i)),
      Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i)))
  (hI : ∀ i ∈ insert a s, (I i).FG) (hI' : ∀ i ∈ insert a s, Finite.{u_1 + 1} (R ⧸ I i)),
  Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ insert a s, I i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, one_eq_top]; infer_instance
  | insert a s has IH =>
    rw [Finset.prod_insert has, mul_comm]
    have := hI' a (by simp)
    have := IH (fun i hi ↦ hI _ (by simp [hi])) (fun i hi ↦ hI' _ (by simp [hi]))
    exact Submodule.finite_quotient_smul _ (hI a (by simp))
Cleared hypotheses: s, hI, hI'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hI : I.FG
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
⊢ Finite.{u_1 + 1} (R ⧸ HPow.hPow (β := ℕ) I 0)
have zero : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊤)
Tactic: simp only [pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hI : I.FG
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
n : ℕ
⊢ Finite.{u_1 + 1} (R ⧸ I ^ n)
have zero : Finite.{u_1 + 1} (R ⧸ HPow.hPow (β := ℕ) I 0)
Tactic: induction n with
  | zero =>
    simp only [pow_zero, Ideal.one_eq_top]
    infer_instance
  | succ n _ =>
    exact Submodule.finite_quotient_smul (I ^ n) hI
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hI : I.FG
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
n : ℕ
zero : Finite.{u_1 + 1} (R ⧸ HPow.hPow (β := ℕ) I 0)
⊢ Finite.{u_1 + 1} (R ⧸ I ^ n)
have succ : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n) → Finite.{u_1 + 1} (R ⧸ I ^ (n + 1))
Tactic: induction n with
  | zero =>
    simp only [pow_zero, Ideal.one_eq_top]
    infer_instance
  | succ n _ =>
    exact Submodule.finite_quotient_smul (I ^ n) hI
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
s : Finset R
hs : span (↑s : Set R) = I
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
n : ℕ
⊢ AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i)
have this : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)
Tactic: have := Ideal.finite_quotient_pow ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
s : Finset R
hs : span (↑s : Set R) = I
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
this : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)
n : ℕ
IH :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i)
⊢ AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ (n + 1))) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
have succ : AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ^ s.card *
    AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
  HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
    (∑ i ∈ Finset.range (n + 1), s.card ^ i)
Tactic: refine (Submodule.index_smul_le (I ^ n) s hs).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
s : Finset R
hs : span (↑s : Set R) = I
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
this : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)
n : ℕ
IH :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i)
⊢ AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ^ s.card *
      AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
have succ : HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i) ^
      s.card *
    AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
  HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
    (∑ i ∈ Finset.range (n + 1), s.card ^ i)
Tactic: refine (Nat.mul_le_mul (Nat.pow_le_pow_left IH _) le_rfl).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
s : Finset R
hs : span (↑s : Set R) = I
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
this : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)
n : ℕ
IH :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i)
⊢ HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i) ^
        s.card *
      AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
have succ : AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ ((∑ i ∈ Finset.range n, s.card ^ i) * s.card) *
    AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
  HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
    (∑ i ∈ Finset.range (n + 1), s.card ^ i)
Tactic: rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
s : Finset R
hs : span (↑s : Set R) = I
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
this : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)
n : ℕ
IH :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i)
succ :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ ((∑ i ∈ Finset.range n, s.card ^ i) * s.card) *
      AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
⊢ HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i) ^
        s.card *
      AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
have succ₁ : AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ ((∑ i ∈ Finset.range n, s.card ^ i) * s.card + 1) ≤
  HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
    (∑ i ∈ Finset.range (n + 1), s.card ^ i)
Tactic: rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
s : Finset R
hs : span (↑s : Set R) = I
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
this : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)
n : ℕ
IH :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i)
succ :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ ((∑ i ∈ Finset.range n, s.card ^ i) * s.card) *
      AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
succ₁ :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ ((∑ i ∈ Finset.range n, s.card ^ i) * s.card + 1) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
⊢ HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i) ^
        s.card *
      AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
have succ₂ : AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ ((∑ i ∈ Finset.range n, s.card ^ i) * s.card + 1) ≤
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ (s.card * ∑ i ∈ Finset.range n, s.card ^ i + 1)
Tactic: rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
s : Finset R
hs : span (↑s : Set R) = I
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
this : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)
n : ℕ
IH :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i)
succ :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ ((∑ i ∈ Finset.range n, s.card ^ i) * s.card) *
      AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
succ₁ :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ ((∑ i ∈ Finset.range n, s.card ^ i) * s.card + 1) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
succ₂ :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ ((∑ i ∈ Finset.range n, s.card ^ i) * s.card + 1) ≤
    AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ (s.card * ∑ i ∈ Finset.range n, s.card ^ i + 1)
⊢ HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i) ^
        s.card *
      AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
have succ₃ : AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ (s.card * ∑ i ∈ Finset.range n, s.card ^ i + 1) ≤
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I) ^ (s.card * ∑ i ∈ Finset.range n, s.card ^ i + 1)
Tactic: rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
s : Finset R
hs : span (↑s : Set R) = I
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
n : ℕ
this : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)
⊢ AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i)
have zero : AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (HPow.hPow (β := ℕ) I 0)) ≤
  HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range 0, s.card ^ i)
Tactic: induction n with
  | zero =>
    simp
  | succ n IH =>
    refine (Submodule.index_smul_le (I ^ n) s hs).trans ?_
    refine (Nat.mul_le_mul (Nat.pow_le_pow_left IH _) le_rfl).trans ?_
    rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
s : Finset R
hs : span (↑s : Set R) = I
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
n : ℕ
this : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)
zero :
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (HPow.hPow (β := ℕ) I 0)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range 0, s.card ^ i)
⊢ AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) (∑ i ∈ Finset.range n, s.card ^ i)
have succ : ∀ (n : ℕ)
  (IH :
    AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ n)) ≤
      HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
        (∑ i ∈ Finset.range n, s.card ^ i)),
  AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup (I ^ (n + 1))) ≤
    HPow.hPow (β := ℕ) (AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I))
      (∑ i ∈ Finset.range (n + 1), s.card ^ i)
Tactic: induction n with
  | zero =>
    simp
  | succ n IH =>
    refine (Submodule.index_smul_le (I ^ n) s hs).trans ?_
    refine (Nat.mul_le_mul (Nat.pow_le_pow_left IH _) le_rfl).trans ?_
    rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
| I.IsRadical
have rw : IsRadical (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I))
Tactic: rw [← @Ideal.mk_ker R _ I]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ I.IsRadical ↔ IsReduced.{u_1} (R ⧸ I)
have conv_lhs : IsRadical (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)) ↔ IsReduced.{u_1} (R ⧸ I)
Tactic: conv_lhs => rw [← @Ideal.mk_ker R _ I]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
hI : IsNilpotent I
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
⊢ P I
have obtain : ∀ (n : ℕ) (hI : I ^ n = ⊥), P I
Tactic: obtain ⟨n, hI : I ^ n = ⊥⟩ := hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
n : ℕ
hI : I ^ n = ⊥
⊢ P I
have h : ∀ (n : ℕ) (H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I) {S : Type u_1}
  [inst : CommRing S] (I : Ideal S) (hI : I ^ n = ⊥), P I
Tactic: induction n using Nat.strong_induction_on generalizing S with | _ n H
Cleared hypotheses: S, inst, I, n, hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
S : Type u_1
inst : CommRing S
I : Ideal S
hI : I ^ n = ⊥
⊢ P I
have pos : ∀ (hI' : I = ⊥), P I
Tactic: by_cases hI' : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
S : Type u_1
inst : CommRing S
I : Ideal S
hI : I ^ n = ⊥
pos : ∀ (hI' : I = ⊥), P I
⊢ P I
have neg : ∀ (hI' : ¬I = ⊥), P I
Tactic: by_cases hI' : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
S : Type u_1
inst : CommRing S
I : Ideal S
hI : I ^ n = ⊥
hI' : I = ⊥
⊢ P I
have pos : ∀ (hI : HPow.hPow (α := Ideal S) ⊥ n = ⊥), P (S := S) ⊥
Tactic: subst hI'
Cleared hypotheses: I, hI, hI'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
S : Type u_1
inst : CommRing S
hI : HPow.hPow (α := Ideal S) ⊥ n = ⊥
⊢ P (S := S) ⊥
have pos : HPow.hPow (α := Ideal S) (β := ℕ) ⊥ 2 = ⊥
Tactic: apply h₁
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
S : Type u_1
inst : CommRing S
hI : HPow.hPow (α := Ideal S) ⊥ n = ⊥
⊢ HPow.hPow (α := Ideal S) (β := ℕ) ⊥ 2 = ⊥
have pos : HPow.hPow (α := Ideal S) (β := ℕ) 0 2 = 0
Tactic: rw [← Ideal.zero_eq_bot, zero_pow two_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
S : Type u_1
inst : CommRing S
hI : HPow.hPow (α := Ideal S) ⊥ n = ⊥
pos : HPow.hPow (α := Ideal S) (β := ℕ) 0 2 = 0
⊢ HPow.hPow (α := Ideal S) (β := ℕ) ⊥ 2 = ⊥
have pos₁ : Eq.{u_1 + 1} (α := Ideal S) 0 0
Tactic: rw [← Ideal.zero_eq_bot, zero_pow two_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
S : Type u_1
inst : CommRing S
I : Ideal S
hI : I ^ n = ⊥
hI' : ¬I = ⊥
⊢ P I
have neg : ∀ (H : ∀ m < 0, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I)
  (hI : HPow.hPow (β := ℕ) I 0 = ⊥), P I
Tactic: rcases n with - | n
Cleared hypotheses: n, H, hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
S : Type u_1
inst : CommRing S
I : Ideal S
hI : I ^ n = ⊥
hI' : ¬I = ⊥
neg :
  ∀ (H : ∀ m < 0, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I)
    (hI : HPow.hPow (β := ℕ) I 0 = ⊥), P I
⊢ P I
have neg₁ : ∀ (n : ℕ) (H : ∀ m < n + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I)
  (hI : I ^ (n + 1) = ⊥), P I
Tactic: rcases n with - | n
Cleared hypotheses: n, H, hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (hypothesis)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
S : Type u_1
inst : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
hI : HPow.hPow (β := ℕ) I 0 = ⊥
⊢ P I
have hI₁ : Eq.{u_1 + 1} (α := Ideal S) ⊤ ⊥
Tactic: rw [pow_zero, Ideal.one_eq_top] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
S : Type u_1
inst : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
hI : Eq.{u_1 + 1} (α := Ideal S) ⊤ ⊥
⊢ P I
have neg : ∀ (this : Subsingleton.{u_1 + 1} (Ideal S)), P I
Tactic: haveI := subsingleton_of_bot_eq_top hI.symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), HPow.hPow (β := ℕ) I 2 = ⊥ → P I
h₂ :
  ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J → P I → P (S := S ⧸ I) (map (F := S →+* S ⧸ I) (Quotient.mk I) J) → P J
S : Type u_1
inst : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
hI : I ^ (n + 1) = ⊥
⊢ P I
have neg : ∀ (H : ∀ m < HAdd.hAdd (α := ℕ) 0 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I)
  (hI : I ^ HAdd.hAdd (α := ℕ) 0 1 = ⊥), P I
Tactic: rcases n with - | n
Cleared hypotheses: n, H, hI