awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_1 : (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'
refine_1₁ : (1 - e₂) * (e' * ((1 - e₂) * e')) = (1 - e₂) * e'
refine_1₂ : (1 - e₂) * (e' * (1 - e₂) * e') = (1 - e₂) * e'
refine_1₃ : (1 - e₂) * ((e' * 1 - e' * e₂) * e') = (1 - e₂) * e'
refine_1₄ : (1 - e₂) * ((e' - e' * e₂) * e') = (1 - e₂) * e'
refine_1₅ : (1 - e₂) * ((e' - 0) * e') = (1 - e₂) * e'
refine_1₆ : (1 - e₂) * (e' * e') = (1 - e₂) * e'
refine_1₇ refine_1₈ : (1 - e₂) * e' = (1 - e₂) * e'
⊢ IsIdempotentElem ((1 - e₂) * e')

Tactic:
rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.eq]

Premises used: mul_sub, sub_zero, mul_assoc, IsIdempotentElem, IsIdempotentElem.eq, mul_one
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_2 :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (1 - e₂) : S) ((f : (a : R) → S) e' : S) = (f : (a : R) → S) e'
refine_2₁ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) 1 : S) ((f : (a : R) → S) e₂ : S))
      ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₂ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) e₂ : S)) ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₃ :
  HMul.hMul (α := S) (β := S) (1 : S) ((f : (a : R) → S) e' : S) -
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₄ :
  HSub.hSub (α := S) ((f : (a : R) → S) e' : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S)) =
    (f : (a : R) → S) e'
refine_2₅ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e' : S) (0 : S) = (f : (a : R) → S) e'
refine_2₆ refine_2₇ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e' : S)
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)

Tactic:
rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero]

Premises used: map_sub, sub_zero, sub_mul, map_mul, map_one, one_mul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_3 : (1 - e₂) * (e' * e₂) = 0
refine_3₁ : (1 - e₂) * 0 = 0
refine_3₂ refine_3₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (1 - e₂) * e' * e₂ = 0

Tactic:
rw [mul_assoc, h₂, mul_zero]

Premises used: mul_assoc, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_4 : e₂ * (1 - e₂) * e' = 0
refine_4₁ : (e₂ * 1 - e₂ * e₂) * e' = 0
refine_4₂ : (e₂ - e₂ * e₂) * e' = 0
refine_4₃ : (e₂ - e₂) * e' = 0
refine_4₄ : 0 * e' = 0
refine_4₅ refine_4₆ : Eq.{u_1 + 1} (α := R) 0 0
⊢ e₂ * ((1 - e₂) * e') = 0

Tactic:
rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul]

Premises used: mul_sub, sub_self, MulZeroClass.zero_mul, mul_assoc, IsIdempotentElem.eq, mul_one
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : S
he : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) e
he' : IsIdempotentElem e
⊢ HMul.hMul (β := S) e ((f : (a : R) → S) 0 : S) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : S
he : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) e
he' : IsIdempotentElem e
⊢ ∃ (e' : R), IsIdempotentElem e' ∧ (f : (a : R) → S) e' = e

Tactic:
simpa using exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h e he he' 0 .zero (by simp)

Premises used: IsIdempotentElem.zero, OfNat.ofNat, exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : Fin 0 → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin 0), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
⊢ ∃ (e' : Fin 0 → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

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

Premises used: finZeroElim, funext, And.intro, Exists.intro, OrthogonalIdempotents.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : Fin 0 → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin 0), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
⊢ ∃ (e' : Fin 0 → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
refine ⟨0, ⟨finZeroElim, finZeroElim⟩, funext finZeroElim⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
succ :
  ∀ (e' : Fin n → R) (h₁ : OrthogonalIdempotents e')
    (h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))),
    ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

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

Premises used: Fin.succEmb, OrthogonalIdempotents.embedding, DFunLike.coe
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
⊢ ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ

Tactic:
have h₂' (i) : f (e' i) = e i.succ := congr_fun h₂ i
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
⊢ HMul.hMul (β := S) (e 0) ((f : (a : R) → S) (∑ i : Fin n, e' i) : S) = 0

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

Premises used: Finset.mul_sum, eq_comm, OrthogonalIdempotents.mul_eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
⊢ HMul.hMul (α := S) ((f : (a : R) → S) (∑ i : Fin n, e' i) : S) (e 0) = 0

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

Premises used: OrthogonalIdempotents.mul_eq, Finset.sum_mul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
succ :
  ∀ (e₀ : R) (h₃ : IsIdempotentElem e₀) (h₄ : (f : (a : R) → S) e₀ = e 0) (h₅ : e₀ * ∑ i : Fin n, e' i = 0)
    (h₆ : (∑ i : Fin n, e' i) * e₀ = 0),
    ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
obtain ⟨e₀, h₃, h₄, h₅, h₆⟩ :=
      exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h _ (he' 0) (he.idem 0) _
      h₁.isIdempotentElem_sum
      (by simp [Finset.mul_sum, h₂', he.mul_eq, eq_comm])
      (by simp [Finset.sum_mul, h₂', he.mul_eq])

Premises used: OrthogonalIdempotents.isIdempotentElem_sum, OrthogonalIdempotents.idem, OfNat.ofNat, exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : (f : (a : R) → S) e₀ = e 0
h₅ : e₀ * ∑ i : Fin n, e' i = 0
h₆ : (∑ i : Fin n, e' i) * e₀ = 0
⊢ ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

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

Premises used: funext, finSuccEquiv, Equiv.toEmbedding, OrthogonalIdempotents.embedding, And.intro, Exists.intro, OrthogonalIdempotents.option
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : (f : (a : R) → S) e₀ = e 0
h₅ : e₀ * ∑ i : Fin n, e' i = 0
h₆ : (∑ i : Fin n, e' i) * e₀ = 0
succ :
  ∀ (i : Fin (n + 1)),
    Function.comp.{1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S)
        ((fun (x : Option (Fin n)) ↦ x.elim e₀ e') ∘
          (⇑(finSuccEquiv n).toEmbedding : (a : Fin (n + 1)) → Option (Fin n)))
        i =
      e i
⊢ ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
refine ⟨_, (h₁.option _ h₃ h₅ h₆).embedding (finSuccEquiv n).toEmbedding, funext fun i ↦ ?_⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : (f : (a : R) → S) e₀ = e 0
h₅ : e₀ * ∑ i : Fin n, e' i = 0
h₆ : (∑ i : Fin n, e' i) * e₀ = 0
i : Fin (n + 1)
succ :
  Function.comp.{1, u_1 + 1, u_2 + 1} (α := Fin (n + 1)) (β := R) (⇑f : (a : R) → S)
      ((fun (x : Option (Fin n)) ↦ x.elim e₀ e') ∘
          (⇑(finSuccEquiv n).toEmbedding : (a : Fin (n + 1)) → Option (Fin n)) :
        Fin (n + 1) → R)
      (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) none : Fin (n + 1)) =
    e (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) none)
succ₁ :
  ∀ (i : Fin n),
    Function.comp.{1, u_1 + 1, u_2 + 1} (α := Fin (n + 1)) (β := R) (⇑f : (a : R) → S)
        ((fun (x : Option (Fin n)) ↦ x.elim e₀ e') ∘
            (⇑(finSuccEquiv n).toEmbedding : (a : Fin (n + 1)) → Option (Fin n)) :
          Fin (n + 1) → R)
        (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) (some i) : Fin (n + 1)) =
      e (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) (some i))
⊢ Function.comp.{1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S)
      ((fun (x : Option (Fin n)) ↦ x.elim e₀ e') ∘ (⇑(finSuccEquiv n).toEmbedding : (a : Fin (n + 1)) → Option (Fin n)))
      i =
    e i

Tactic:
obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i

Premises used: finSuccEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : (f : (a : R) → S) e₀ = e 0
h₅ : e₀ * ∑ i : Fin n, e' i = 0
h₆ : (∑ i : Fin n, e' i) * e₀ = 0
⊢ Function.comp.{1, u_1 + 1, u_2 + 1} (α := Fin (n + 1)) (β := R) (⇑f : (a : R) → S)
      ((fun (x : Option (Fin n)) ↦ x.elim e₀ e') ∘
          (⇑(finSuccEquiv n).toEmbedding : (a : Fin (n + 1)) → Option (Fin n)) :
        Fin (n + 1) → R)
      (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) none : Fin (n + 1)) =
    e (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) none)

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : (f : (a : R) → S) e₀ = e 0
h₅ : e₀ * ∑ i : Fin n, e' i = 0
h₆ : (∑ i : Fin n, e' i) * e₀ = 0
i : Fin n
⊢ Function.comp.{1, u_1 + 1, u_2 + 1} (α := Fin (n + 1)) (β := R) (⇑f : (a : R) → S)
      ((fun (x : Option (Fin n)) ↦ x.elim e₀ e') ∘
          (⇑(finSuccEquiv n).toEmbedding : (a : Fin (n + 1)) → Option (Fin n)) :
        Fin (n + 1) → R)
      (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) (some i) : Fin (n + 1)) =
    e (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) (some i))

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
e : Fin n → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
zero :
  ∀ {e : Fin 0 → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin 0), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin 0 → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
        (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
        ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e)
    {e : Fin (n + 1) → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
induction n with
  | zero => refine ⟨0, ⟨finZeroElim, finZeroElim⟩, funext finZeroElim⟩
  | succ n IH =>
    obtain ⟨e', h₁, h₂⟩ := IH (he.embedding (Fin.succEmb n)) (fun i ↦ he' _)
    have h₂' (i) : f (e' i) = e i.succ := congr_fun h₂ i
    obtain ⟨e₀, h₃, h₄, h₅, h₆⟩ :=
      exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h _ (he' 0) (he.idem 0) _
      h₁.isIdempotentElem_sum
      (by simp [Finset.mul_sum, h₂', he.mul_eq, eq_comm])
      (by simp [Finset.sum_mul, h₂', he.mul_eq])
    refine ⟨_, (h₁.option _ h₃ h₅ h₆).embedding (finSuccEquiv n).toEmbedding, funext fun i ↦ ?_⟩
    obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i <;> simp [*]

Premises used: rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
inst_2 : Finite I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : I → S
he : OrthogonalIdempotents e
he' : ∀ (i : I), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
intro : ∀ (val : Fintype I), ∃ (e' : I → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : I → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
cases nonempty_fintype I

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
inst_2 : Finite I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : I → S
he : OrthogonalIdempotents e
he' : ∀ (i : I), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
val : Fintype I
intro :
  ∀ (e' : Fin (Fintype.card I) → R) (h₁ : OrthogonalIdempotents e')
    (h₂ :
      (⇑f : (a : R) → S) ∘ e' =
        e ∘ (⇑(Equiv.toEmbedding (Equiv.symm (Fintype.equivFin I))) : (a : Fin (Fintype.card I)) → I)),
    ∃ (e' : I → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : I → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker_aux f h
    (he.embedding (Fintype.equivFin I).symm.toEmbedding) (fun _ ↦ he' _)

Premises used: Fintype.equivFin, Equiv.toEmbedding, OrthogonalIdempotents.embedding, OrthogonalIdempotents.lift_of_isNilpotent_ker_aux, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
inst_2 : Finite I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : I → S
he : OrthogonalIdempotents e
he' : ∀ (i : I), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
val : Fintype I
e' : Fin (Fintype.card I) → R
h₁ : OrthogonalIdempotents e'
h₂ :
  (⇑f : (a : R) → S) ∘ e' =
    e ∘ (⇑(Equiv.toEmbedding (Equiv.symm (Fintype.equivFin I))) : (a : Fin (Fintype.card I)) → I)
h₃ :
  ∀ (x : I),
    ((⇑f : (a : R) → S) ∘ e' ∘ (⇑(Equiv.toEmbedding (Fintype.equivFin I)) : (a : I) → Fin (Fintype.card I))) x = e x
⊢ (⇑f : (a : R) → S) ∘ e' ∘ (⇑(Equiv.toEmbedding (Fintype.equivFin I)) : (a : I) → Fin (Fintype.card I)) = e

Tactic:
ext x