-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.lift_of_isNilpotent_ker_aux
    (h : ∀ x ∈ RingHom.ker f, IsNilpotent x)
    {n} {e : Fin n → S} (he : OrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) :
    ∃ e' : Fin n → R, OrthogonalIdempotents e' ∧ f ∘ e' = e

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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
⊢ e 0 * f (∑ i ∈ ?m.144356, e' i) = 0

Tactic:
simp [Finset.mul_sum, h₂', he.mul_eq, Fin.succ_ne_zero, eq_comm]

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
n : ℕ
e : Fin n → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
induction' n with n IH

Result:
case 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 : Fin 0 → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin 0), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

case 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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Proof state:
case succ.intro.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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
have h₂' (i) : f (e' i) = e i.succ := congr_fun h₂ i

Result:
case succ.intro.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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Proof state:
case succ.intro.intro.intro.intro.intro.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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i : Fin n, e' i = 0
h₆ : (∑ i : Fin n, e' i) * e₀ = 0
i : Fin (n + 1)
⊢ (⇑f ∘ (fun x => x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) i = e i

Tactic:
obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i <;> simp [*]

Result:
no goals

Proof state:
case 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 : Fin 0 → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin 0), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
refine ⟨0, ⟨finZeroElim, finZeroElim⟩, funext finZeroElim⟩

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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
⊢ f (∑ i ∈ ?m.144356, e' i) * e 0 = 0

Tactic:
simp [Finset.sum_mul, h₂', he.mul_eq, Fin.succ_ne_zero]

Result:
no goals

Proof state:
case succ.intro.intro.intro.intro.intro.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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i ∈ ?m.144356, e' i = 0
h₆ : (∑ i ∈ ?m.144356, e' i) * e₀ = 0
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
refine ⟨_, (h₁.option _ h₃ h₅ h₆).embedding (finSuccEquiv n).toEmbedding, funext fun i ↦ ?_⟩

Result:
case succ.intro.intro.intro.intro.intro.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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i : Fin n, e' i = 0
h₆ : (∑ i : Fin n, e' i) * e₀ = 0
i : Fin (n + 1)
⊢ (⇑f ∘ (fun x => x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) i = e i

Proof state:
case 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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
obtain ⟨e', h₁, h₂⟩ := IH (he.embedding (Fin.succEmb n)) (fun i ↦ he' _)

Result:
case succ.intro.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
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e