-- Mathlib/RingTheory/Idempotents.lean
theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux
    (h : ∀ x ∈ RingHom.ker f, IsNilpotent x)
    (e₁ : S) (he : e₁ ∈ f.range) (he₁ : IsIdempotentElem e₁)
    (e₂ : R) (he₂ : IsIdempotentElem e₂) (he₁e₂ : e₁ * f e₂ = 0) :
    ∃ e' : R, IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : MulOpposite.unop (1 ^ n - MulOpposite.op (1 - a ^ n) ^ n) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
⊢ 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n

Tactic:
simpa using hk

Result:
no goals

Proof state:
case intro.inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0

Tactic:
let a := e₁ - e₁ * e₂

Result:
case intro.inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0

Proof state:
case intro.inr.intro.refine_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : MulOpposite.unop (1 ^ n - MulOpposite.op (1 - a ^ n) ^ n) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Tactic:
have : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n := by simpa using hk

Result:
case intro.inr.intro.refine_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : MulOpposite.unop (1 ^ n - MulOpposite.op (1 - a ^ n) ^ n) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
this : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Proof state:
case intro.inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0

Tactic:
obtain ⟨n, hn⟩ := h _ hx'

Result:
case intro.inr.intro
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0

Proof state:
case intro.inr.intro.refine_2.intro.zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
k : Rᵐᵒᵖ
hn : (a - a ^ 2) ^ 0 = 0
hk : MulOpposite.unop (1 ^ 0 - MulOpposite.op (1 - a ^ 0) ^ 0) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ 0)) * k)
this : 1 - (1 - a ^ 0) ^ 0 = MulOpposite.unop k * a ^ 0
⊢ MulOpposite.unop k * (a ^ 0 * e₂) = 0

Tactic:
simp at hn

Result:
no goals

Proof state:
case intro.inr.intro.refine_2.intro.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
k : Rᵐᵒᵖ
n : ℕ
hn : (a - a ^ 2) ^ (n + 1) = 0
hk :
  MulOpposite.unop (1 ^ (n + 1) - MulOpposite.op (1 - a ^ (n + 1)) ^ (n + 1)) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ (n + 1))) * k)
this : 1 - (1 - a ^ (n + 1)) ^ (n + 1) = MulOpposite.unop k * a ^ (n + 1)
⊢ MulOpposite.unop k * (a ^ (n + 1) * e₂) = 0

Tactic:
rw [pow_succ, mul_assoc, ha', mul_zero, mul_zero]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
⊢ a - a ^ 2 ∈ RingHom.ker f

Tactic:
simp [RingHom.mem_ker, mul_sub, pow_two, ha, he₁.eq]

Result:
no goals

Proof state:
case intro.inr.intro.refine_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : 1 ^ n - MulOpposite.op (1 - a ^ n) ^ n = (1 - MulOpposite.op (1 - a ^ n)) * k
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Tactic:
apply_fun MulOpposite.unop at hk

Result:
case intro.inr.intro.refine_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : MulOpposite.unop (1 ^ n - MulOpposite.op (1 - a ^ n) ^ n) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₁ : S
he : e₁ ∈ f.range
he₁ : IsIdempotentElem e₁
e₂ : R
he₂ : IsIdempotentElem e₂
he₁e₂ : e₁ * f e₂ = 0
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0

Tactic:
obtain ⟨e₁, rfl⟩ := he

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0