awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
have 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
Tactic: refine ⟨_, (h₁.option _ h₃ h₅ h₆).embedding (finSuccEquiv n).toEmbedding, funext fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ 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
have 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)
Tactic: obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ 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
have 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))
Tactic: obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have 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
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 [*]
Cleared hypotheses: n, e, he, he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have 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
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 [*]
Cleared hypotheses: n, e, he, he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ ∃ (e' : I → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have intro : ∀ (val : Fintype I), ∃ (e' : I → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: cases nonempty_fintype I
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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' : I → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have 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
Tactic: obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker_aux f h
    (he.embedding (Fintype.equivFin I).symm.toEmbedding) (fun _ ↦ he' _)
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ (⇑f : (a : R) → S) ∘ e' ∘ (⇑(Equiv.toEmbedding (Fintype.equivFin I)) : (a : I) → Fin (Fintype.card I)) = e
have h₃ : ∀ (x : I),
  ((⇑f : (a : R) → S) ∘ e' ∘ (⇑(Equiv.toEmbedding (Fintype.equivFin I)) : (a : I) → Fin (Fintype.card I))) x = e x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x
have rw : y = 1 - x → (x * y = 0 ∧ y * x = 0 ↔ IsIdempotentElem x)
Tactic: rw [pair_iff'ₛ, ← eq_sub_iff_add_eq', ← and_assoc, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
I : Type u_3
e : I → R
inst_1 : Fintype I
he : OrthogonalIdempotents e
⊢ Eq.{u_1 + 1} (α := R) (∑ i : Option I, i.elim (HSub.hSub (α := R) 1 (∑ i : I, e i)) e) 1
have rw : Option.elim none (HSub.hSub (α := R) 1 (∑ i : I, e i)) e +
    ∑ i : I, (some i).elim (HSub.hSub (α := R) 1 (∑ i : I, e i)) e =
  1
Tactic: rw [Fintype.sum_option]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inl : Subsingleton R → ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
inl : Subsingleton R → ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inr : Nontrivial R → ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
h_1 : Subsingleton R
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inl : ∀ (e' : (i : Fin n) → R) (he' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i),
  ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: choose e' he' using he'
Cleared hypotheses: he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
h_1 : Nontrivial R
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inr : Subsingleton S → ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: cases subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
h_1 : Nontrivial R
inr : Subsingleton S → ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inr₁ : Nontrivial S → ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: cases subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
h_1 : Nontrivial R
h_2 : Subsingleton S
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inr : ∀ (n_1 : ℕ) (hn : HPow.hPow (α := R) 1 n_1 = 0),
  ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: obtain ⟨n, hn⟩ := h 1 (Subsingleton.elim _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
h_1 : Nontrivial R
h_2 : Nontrivial S
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inr : ∀ {e : Fin 0 → S} (he : CompleteOrthogonalIdempotents e)
  (he' : ∀ (i : Fin 0), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
  ∃ (e' : Fin 0 → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: rcases n with - | n
Cleared hypotheses: n, e, he, he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
h_1 : Nontrivial R
h_2 : Nontrivial S
inr :
  ∀ {e : Fin 0 → S} (he : CompleteOrthogonalIdempotents e)
    (he' : ∀ (i : Fin 0), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin 0 → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inr₁ : ∀ (n : ℕ) {e : Fin (n + 1) → S} (he : CompleteOrthogonalIdempotents 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), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: rcases n with - | n
Cleared hypotheses: n, e, he, he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
h_1 : Nontrivial R
h_2 : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents 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), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inr : ∀ (e' : Fin (n + 1) → R) (h₁ : OrthogonalIdempotents e') (h₂ : (⇑f : (a : R) → S) ∘ e' = e),
  ∃ (e' : Fin (n + 1) → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: obtain ⟨e', h₁, h₂⟩ := OrthogonalIdempotents.lift_of_isNilpotent_ker f h he.1 he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
h_1 : Nontrivial R
h_2 : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents 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
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : Fin (n + 1) → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have inr : ∀ (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 (HSub.hSub (α := R) 1 (∑ i : Fin n, (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))) i))
            (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1)))) ∘
        (⇑(finSuccEquiv n) : (a : Fin (n + 1)) → Option (Fin n)))
      i =
    e i
Tactic: refine ⟨_, (equiv (finSuccEquiv n)).mpr
    (CompleteOrthogonalIdempotents.option (h₁.embedding (Fin.succEmb _))), funext fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (hypothesis)
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
h_1 : Nontrivial R
h_2 : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents 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
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e
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 (HSub.hSub (α := R) 1 (∑ i : Fin n, (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))) i))
            (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1)))) ∘
        (⇑(finSuccEquiv n) : (a : Fin (n + 1)) → Option (Fin n)))
      i =
    e i
have this : ∀ (i : Fin (n + 1)), (f : (a : R) → S) (e' i) = e i
Tactic: have (i : _) : f (e' i) = e i := congr_fun h₂ i
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
h_1 : Nontrivial R
h_2 : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents 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
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e
i : Fin (n + 1)
this : ∀ (i : Fin (n + 1)), (f : (a : R) → S) (e' i) = e i
⊢ Function.comp.{1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S)
      ((fun (x : Option (Fin n)) ↦
          x.elim (HSub.hSub (α := R) 1 (∑ i : Fin n, (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))) i))
            (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1)))) ∘
        (⇑(finSuccEquiv n) : (a : Fin (n + 1)) → Option (Fin n)))
      i =
    e i
have inr : Function.comp.{1, u_1 + 1, u_2 + 1} (α := Fin (n + 1)) (β := R) (⇑f : (a : R) → S)
    ((fun (x : Option (Fin n)) ↦
        x.elim (HSub.hSub (α := R) 1 (∑ i : Fin n, (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))) i))
          (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1)))) ∘
      (⇑(finSuccEquiv n) : (a : Fin (n + 1)) → Option (Fin n)))
    0 =
  e 0
Tactic: cases i using Fin.cases with
  | zero => simp [this, Fin.sum_univ_succ, ← he.complete]
  | succ i => simp [this]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
h_1 : Nontrivial R
h_2 : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents 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
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e
i : Fin (n + 1)
this : ∀ (i : Fin (n + 1)), (f : (a : R) → S) (e' i) = e i
inr :
  Function.comp.{1, u_1 + 1, u_2 + 1} (α := Fin (n + 1)) (β := R) (⇑f : (a : R) → S)
      ((fun (x : Option (Fin n)) ↦
          x.elim (HSub.hSub (α := R) 1 (∑ i : Fin n, (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))) i))
            (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1)))) ∘
        (⇑(finSuccEquiv n) : (a : Fin (n + 1)) → Option (Fin n)))
      0 =
    e 0
⊢ Function.comp.{1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S)
      ((fun (x : Option (Fin n)) ↦
          x.elim (HSub.hSub (α := R) 1 (∑ i : Fin n, (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))) i))
            (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1)))) ∘
        (⇑(finSuccEquiv n) : (a : Fin (n + 1)) → Option (Fin n)))
      i =
    e i
have inr₁ : ∀ (i : Fin n),
  Function.comp.{1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S)
      ((fun (x : Option (Fin n)) ↦
          x.elim (HSub.hSub (α := R) 1 (∑ i : Fin n, (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))) i))
            (e' ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1)))) ∘
        (⇑(finSuccEquiv n) : (a : Fin (n + 1)) → Option (Fin n)))
      i.succ =
    e i.succ
Tactic: cases i using Fin.cases with
  | zero => simp [this, Fin.sum_univ_succ, ← he.complete]
  | succ i => simp [this]
Cleared hypotheses: i