case intro
R : Type ?u.1313
S : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing S
inst✝ : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI : I ^ n = ⊥
⊢ P I
R : Type ?u.1313
S : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing S
inst✝ : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
⊢ P I
obtain ⟨n, hI : I ^ n = ⊥⟩ := hI
case intro.h
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : I ^ n = ⊥
⊢ P I
case intro
R : Type ?u.1313
S : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing S
inst✝ : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI : I ^ n = ⊥
⊢ P I
induction' n using Nat.strong_induction_on with n H generalizing S
case pos
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : I ^ n = ⊥
hI' : I = ⊥
⊢ P I

case neg
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : I ^ n = ⊥
hI' : ¬I = ⊥
⊢ P I
case intro.h
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : I ^ n = ⊥
⊢ P I
by_cases hI' : I = ⊥
case neg.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ (m : ℕ), m < Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.zero = ⊥
⊢ P I

case neg.succ
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ), m < Nat.succ n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ n = ⊥
⊢ P I
case neg
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : I ^ n = ⊥
hI' : ¬I = ⊥
⊢ P I
cases' n with n
case neg.succ.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H :
  ∀ (m : ℕ),
    m < Nat.succ Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ Nat.zero = ⊥
⊢ P I

case neg.succ.succ
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ P I
case neg.succ
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ), m < Nat.succ n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ n = ⊥
⊢ P I
cases' n with n
case neg.succ.succ.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ P (I ^ 2)

case neg.succ.succ.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ P (map (Quotient.mk (I ^ 2)) I)
case neg.succ.succ
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ P I
apply h₂ (I ^ 2) _ (Ideal.pow_le_self two_ne_zero)
case pos
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
hI : ⊥ ^ n = ⊥
⊢ P ⊥
case pos
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : I ^ n = ⊥
hI' : I = ⊥
⊢ P I
subst hI'
case pos.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
hI : ⊥ ^ n = ⊥
⊢ ⊥ ^ 2 = ⊥
case pos
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
hI : ⊥ ^ n = ⊥
⊢ P ⊥
apply h₁
case pos.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
hI : ⊥ ^ n = ⊥
⊢ 0 < 2
case pos.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
hI : ⊥ ^ n = ⊥
⊢ ⊥ ^ 2 = ⊥
rw [← Ideal.zero_eq_bot, zero_pow]
no goals
case pos.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
hI : ⊥ ^ n = ⊥
⊢ 0 < 2
exact zero_lt_two
case neg.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ (m : ℕ), m < Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : ⊤ = ⊥
⊢ P I
case neg.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ (m : ℕ), m < Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.zero = ⊥
⊢ P I
rw [pow_zero, Ideal.one_eq_top] at hI
case neg.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ (m : ℕ), m < Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : ⊤ = ⊥
this : Subsingleton (Ideal S)
⊢ P I
case neg.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ (m : ℕ), m < Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : ⊤ = ⊥
⊢ P I
haveI := subsingleton_of_bot_eq_top hI.symm
no goals
case neg.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ (m : ℕ), m < Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : ⊤ = ⊥
this : Subsingleton (Ideal S)
⊢ P I
exact (hI' (Subsingleton.elim _ _)).elim
case neg.succ.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H :
  ∀ (m : ℕ),
    m < Nat.succ Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I = ⊥
⊢ P I
case neg.succ.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H :
  ∀ (m : ℕ),
    m < Nat.succ Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ Nat.zero = ⊥
⊢ P I
rw [pow_one] at hI
no goals
case neg.succ.zero
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H :
  ∀ (m : ℕ),
    m < Nat.succ Nat.zero → ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I = ⊥
⊢ P I
exact (hI' hI).elim
case neg.succ.succ.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ (I ^ 2) ^ Nat.succ n = ⊥

R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ Nat.succ n < Nat.succ (Nat.succ n)
case neg.succ.succ.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ P (I ^ 2)
apply H n.succ _ (I ^ 2)
case neg.succ.succ.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ I ^ (2 * (n + 1)) ≤ I ^ (n + 1 + 1)
case neg.succ.succ.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ (I ^ 2) ^ Nat.succ n = ⊥
rw [← pow_mul, eq_bot_iff, ← hI, Nat.succ_eq_add_one, Nat.succ_eq_add_one]
no goals
case neg.succ.succ.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ I ^ (2 * (n + 1)) ≤ I ^ (n + 1 + 1)
apply Ideal.pow_le_pow (by linarith)
no goals
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ n + 1 + 1 ≤ 2 * (n + 1)
linarith
no goals
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ Nat.succ n < Nat.succ (Nat.succ n)
exact n.succ.lt_succ_self
case neg.succ.succ.a.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ map (Quotient.mk (I ^ 2)) I ^ 2 = ⊥
case neg.succ.succ.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ P (map (Quotient.mk (I ^ 2)) I)
apply h₁
no goals
case neg.succ.succ.a.a
R : Type ?u.1313
S✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R 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), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ map (Quotient.mk (I ^ 2)) I ^ 2 = ⊥
rw [← Ideal.map_pow, Ideal.map_quotient_self]