awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
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)
this_1 : Finite.{u_1 + 1} (R ⧸ I a)
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
⊢ a ∈ insert a s

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
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)
this_1 : Finite.{u_1 + 1} (R ⧸ I a)
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
⊢ Finite.{u_1 + 1} (R ⧸ (∏ x ∈ s, I x) * I a)

Tactic:
exact Submodule.finite_quotient_smul _ (hI a (by simp))

Premises used: Submodule.finite_quotient_smul
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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))
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.insert a s, (I i).FG) (hI' : ∀ i ∈ Insert.insert a s, Finite.{u_1 + 1} (R ⧸ I i)),
    Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ Insert.insert a s, I i))
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))

Tactic:
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))

Premises used: Finset.prod_empty, Ideal.one_eq_top, Insert.insert, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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))
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.insert a s, (I i).FG) (hI' : ∀ i ∈ Insert.insert a s, Finite.{u_1 + 1} (R ⧸ I i)),
    Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ Insert.insert a s, I i))
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ 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))

Premises used: Finset.prod_empty, Ideal.one_eq_top, Insert.insert, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hI : I.FG
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
zero : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊤)
⊢ Finite.{u_1 + 1} (R ⧸ HPow.hPow (β := ℕ) I 0)

Tactic:
simp only [pow_zero, Ideal.one_eq_top]

Premises used: Ideal.one_eq_top, pow_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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} (HasQuotient.Quotient R (B := Ideal R) ⊤)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hI : I.FG
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
n : ℕ
h : Finite.{u_1 + 1} (R ⧸ I ^ n)
⊢ Finite.{u_1 + 1} (R ⧸ I ^ (n + 1))

Tactic:
Submodule.finite_quotient_smul (I ^ n) hI

Premises used: Set.Mem, Submodule.finite_quotient_smul, npowRec, HPow.hPow
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hI : I.FG
inst_1 : Finite.{u_1 + 1} (R ⧸ I)
n : ℕ
h : Finite.{u_1 + 1} (R ⧸ I ^ n)
⊢ Finite.{u_1 + 1} (R ⧸ I ^ (n + 1))

Tactic:
exact Submodule.finite_quotient_smul (I ^ n) hI

Premises used: Submodule.finite_quotient_smul, HPow.hPow
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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)
succ : ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n) → Finite.{u_1 + 1} (R ⧸ I ^ (n + 1))
⊢ Finite.{u_1 + 1} (R ⧸ I ^ n)

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

Premises used: Ideal.one_eq_top, pow_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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 : ℕ
⊢ ∀ (n : ℕ), Finite.{u_1 + 1} (R ⧸ I ^ n)

Tactic:
have := Ideal.finite_quotient_pow ⟨s, hs⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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)
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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)

Tactic:
(Submodule.index_smul_le (I ^ n) s hs).trans ?_

Premises used: Set.Mem, npowRec, HPow.hPow, LE.le.trans, Submodule.index_smul_le
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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 ^ 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)
⊢ 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:
refine (Submodule.index_smul_le (I ^ n) s hs).trans ?_

Premises used: HPow.hPow, LE.le.trans, Submodule.index_smul_le
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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)

Tactic:
(Nat.mul_le_mul (Nat.pow_le_pow_left IH _) le_rfl).trans ?_

Premises used: le_rfl, Nat.mul_le_mul, LE.le.trans, Nat.pow_le_pow_left
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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 :
  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)
⊢ 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 (Nat.mul_le_mul (Nat.pow_le_pow_left IH _) le_rfl).trans ?_

Premises used: le_rfl, Nat.mul_le_mul, LE.le.trans, Nat.pow_le_pow_left
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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)
succ₃ 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)
⊢ 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:
rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]

Premises used: pow_succ, pow_mul, mul_comm, geom_sum_succ
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
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)
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)
⊢ 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)

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]

Premises used: pow_succ, pow_mul, HPow.hPow, mul_comm, geom_sum_succ, LE.le.trans, Submodule.index_smul_le
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
rw : IsRadical (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I))
| I.IsRadical

Tactic:
rw [← @Ideal.mk_ker R _ I]

Premises used: Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
conv_lhs : IsRadical (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)) ↔ IsReduced.{u_1} (R ⧸ I)
⊢ I.IsRadical ↔ IsReduced.{u_1} (R ⧸ I)

Tactic:
conv_lhs => rw [← @Ideal.mk_ker R _ I]

Premises used: Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ IsRadical (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)) ↔ IsReduced.{u_1} (R ⧸ I)

Tactic:
RingHom.ker_isRadical_iff_reduced_of_surjective Quotient.mk_surjective

Premises used: RingHom.ker_isRadical_iff_reduced_of_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ IsRadical (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)) ↔ IsReduced.{u_1} (R ⧸ I)

Tactic:
exact RingHom.ker_isRadical_iff_reduced_of_surjective Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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
obtain : ∀ (n : ℕ) (hI : I ^ n = ⊥), P I
⊢ P I

Tactic:
obtain ⟨n, hI : I ^ n = ⊥⟩ := hI
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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 = ⊥
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
⊢ P I

Tactic:
induction n using Nat.strong_induction_on generalizing S with | _ n H
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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
neg : ∀ (hI' : ¬I = ⊥), P I
⊢ P I

Tactic:
by_cases hI' : I = ⊥
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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 = ⊥
pos : ∀ (hI : HPow.hPow (α := Ideal S) ⊥ n = ⊥), P (S := S) ⊥
⊢ P I

Tactic:
subst hI'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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) (β := ℕ) ⊥ 2 = ⊥
⊢ P (S := S) ⊥

Tactic:
apply h₁
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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
pos₁ pos₂ : Eq.{u_1 + 1} (α := Ideal S) 0 0
⊢ HPow.hPow (α := Ideal S) (β := ℕ) ⊥ 2 = ⊥

Tactic:
rw [← Ideal.zero_eq_bot, zero_pow two_ne_zero]

Premises used: Ideal.zero_eq_bot, two_ne_zero, zero_pow
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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
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
⊢ P I

Tactic:
rcases n with - | n
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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 = ⊥
⊢ Eq.{u_1 + 1} (α := Ideal S) ⊤ ⊥

Tactic:
rw [pow_zero, Ideal.one_eq_top] at hI

Premises used: Ideal.one_eq_top, pow_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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) ⊤ ⊥
neg : ∀ (this : Subsingleton.{u_1 + 1} (Ideal S)), P I
⊢ P I

Tactic:
haveI := subsingleton_of_bot_eq_top hI.symm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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) ⊤ ⊥
this : Subsingleton.{u_1 + 1} (Ideal S)
⊢ P I

Tactic:
(hI' (Subsingleton.elim _ _)).elim

Premises used: False.elim, Subsingleton.elim
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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) ⊤ ⊥
this : Subsingleton.{u_1 + 1} (Ideal S)
⊢ P I

Tactic:
exact (hI' (Subsingleton.elim _ _)).elim

Premises used: False.elim, Subsingleton.elim
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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) = ⊥
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
neg₁ :
  ∀ (n : ℕ) (H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I)
    (hI : I ^ (n + 1 + 1) = ⊥), P I
⊢ P I

Tactic:
rcases n with - | n
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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 < 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 = ⊥
⊢ I = ⊥

Tactic:
rw [pow_one] at hI

Premises used: pow_one
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
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 < HAdd.hAdd (α := ℕ) 0 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) (hI : I ^ m = ⊥), P I
hI : I = ⊥
⊢ P I

Tactic:
(hI' hI).elim

Premises used: False.elim