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
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)
x : I
⊢ ((⇑f : (a : R) → S) ∘ e' ∘ (⇑(Equiv.toEmbedding (Fintype.equivFin I)) : (a : I) → Fin (Fintype.card I))) x = e x

Tactic:
simpa using congr_fun h₂ (Fintype.equivFin I x)

Premises used: Fintype.equivFin, congr_fun, 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)
⊢ ∃ (e' : I → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
refine ⟨_, h₁.embedding (Fintype.equivFin I).toEmbedding,
    by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x y : R
rw : y = 1 - x → (x * y = 0 ∧ y * x = 0 ↔ IsIdempotentElem x)
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x

Tactic:
rw [pair_iff'ₛ, ← eq_sub_iff_add_eq', ← and_assoc, and_congr_left_iff]

Premises used: eq_sub_iff_add_eq', and_congr_left_iff, and_assoc, CompleteOrthogonalIdempotents.pair_iff'ₛ
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
⊢ x * (1 - x) = 0 ∧ (1 - x) * x = 0 ↔ IsIdempotentElem x

Tactic:
simp [mul_sub, sub_mul, IsIdempotentElem, sub_eq_zero, eq_comm]

Premises used: mul_sub, sub_eq_zero, eq_comm, sub_mul, IsIdempotentElem
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
e : R
he : IsIdempotentElem e
⊢ CompleteOrthogonalIdempotents ![e, 1 - e]

Tactic:
pair_iff.mpr ⟨he, rfl⟩

Premises used: Iff.mpr, CompleteOrthogonalIdempotents.pair_iff, And.intro, rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
I : Type u_3
e : I → R
inst_1 : Fintype I
he : OrthogonalIdempotents e
⊢ HSub.hSub (α := R) 1 (∑ i : I, e i) * ∑ i : I, e i = 0

Tactic:
simp [sub_mul, he.isIdempotentElem_sum.eq]

Premises used: OrthogonalIdempotents.isIdempotentElem_sum, sub_mul, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
I : Type u_3
e : I → R
inst_1 : Fintype I
he : OrthogonalIdempotents e
⊢ (∑ i : I, e i) * HSub.hSub (α := R) 1 (∑ i : I, e i) = 0

Tactic:
simp [mul_sub, he.isIdempotentElem_sum.eq]

Premises used: OrthogonalIdempotents.isIdempotentElem_sum, mul_sub, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
I : Type u_3
e : I → R
inst_1 : Fintype I
he : OrthogonalIdempotents e
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i : Option I, i.elim (HSub.hSub (α := R) 1 (∑ i : I, e i)) e) 1

Tactic:
rw [Fintype.sum_option]

Premises used: Fintype.sum_option
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
I : Type u_3
e : I → R
inst_1 : Fintype I
he : OrthogonalIdempotents e
⊢ 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:
sub_add_cancel _ _

Premises used: sub_add_cancel
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
I : Type u_3
e : I → R
inst_1 : Fintype I
he : OrthogonalIdempotents e
⊢ 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:
exact sub_add_cancel _ _

Premises used: sub_add_cancel
-- 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 : 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
inr : Nontrivial 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

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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 : 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
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
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
choose e' he' using he'
-- 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 : CompleteOrthogonalIdempotents e
h_1 : Subsingleton R
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:
⟨e', .of_subsingleton, funext he'⟩

Premises used: CompleteOrthogonalIdempotents.of_subsingleton, funext, And.intro, Exists.intro
-- 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 : CompleteOrthogonalIdempotents e
h_1 : Subsingleton R
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:
exact ⟨e', .of_subsingleton, funext he'⟩
-- 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 : 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
inr₁ : Nontrivial 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

Tactic:
cases subsingleton_or_nontrivial S

Premises used: subsingleton_or_nontrivial
-- 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 : 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
inr :
  ∀ (n_1 : ℕ) (hn : HPow.hPow (α := R) 1 n_1 = 0),
    ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
obtain ⟨n, hn⟩ := h 1 (Subsingleton.elim _ _)

Premises used: Subsingleton.elim, 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
n_1 : ℕ
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)
h_1 : Nontrivial R
h_2 : Subsingleton S
n : ℕ
hn : HPow.hPow (α := R) 1 n = 0
⊢ ∃ (e' : Fin n_1 → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
simp at hn
-- 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 : 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
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
⊢ ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
rcases n with - | n
-- 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
h_1 : Nontrivial R
h_2 : Nontrivial S
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:
simpa using he.complete

Premises used: CompleteOrthogonalIdempotents.complete
-- 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
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)
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
⊢ ∃ (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'

Premises used: CompleteOrthogonalIdempotents.toOrthogonalIdempotents, OrthogonalIdempotents.lift_of_isNilpotent_ker
-- 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
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

Tactic:
⟨_, (equiv (finSuccEquiv n)).mpr
    (CompleteOrthogonalIdempotents.option (h₁.embedding (Fin.succEmb _))), funext fun i ↦ ?_⟩

Premises used: Iff.mpr, CompleteOrthogonalIdempotents.equiv, CompleteOrthogonalIdempotents.option, funext, Fin.succEmb, finSuccEquiv, OrthogonalIdempotents.embedding, And.intro, Exists.intro
-- 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
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
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
⊢ ∃ (e' : Fin (n + 1) → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
refine ⟨_, (equiv (finSuccEquiv n)).mpr
    (CompleteOrthogonalIdempotents.option (h₁.embedding (Fin.succEmb _))), 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
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)
⊢ ∀ (i : Fin (n + 1)), (f : (a : R) → S) (e' i) = e i

Tactic:
have (i : _) : f (e' i) = e i := 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
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
this : ∀ (i : Fin (n + 1)), (f : (a : R) → S) (e' i) = e i
⊢ 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:
simp [this, Fin.sum_univ_succ, ← he.complete]

Premises used: CompleteOrthogonalIdempotents.complete, Fin.sum_univ_succ
-- 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
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
this : ∀ (i : Fin (n + 1)), (f : (a : R) → S) (e' i) = e i
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:
simp [this]
-- 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
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
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
⊢ 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:
cases i using Fin.cases with
  | zero => simp [this, Fin.sum_univ_succ, ← he.complete]
  | succ i => simp [this]

Premises used: CompleteOrthogonalIdempotents.complete, Fin.sum_univ_succ
-- 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 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
obtain :
  ∀ (e' : Fin (Fintype.card I) → R) (h₁ : CompleteOrthogonalIdempotents e')
    (h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Equiv.symm (Fintype.equivFin I)) : (a : Fin (Fintype.card I)) → I)),
    ∃ (e' : I → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
⊢ ∃ (e' : I → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

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

Premises used: Iff.mpr, CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker_aux, CompleteOrthogonalIdempotents.equiv, Fintype.equivFin, 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 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Equiv.symm (Fintype.equivFin I)) : (a : Fin (Fintype.card I)) → I)
h₃ : ∀ (x : I), ((⇑f : (a : R) → S) ∘ e' ∘ (⇑(Fintype.equivFin I) : (a : I) → Fin (Fintype.card I))) x = e x
⊢ (⇑f : (a : R) → S) ∘ e' ∘ (⇑(Fintype.equivFin I) : (a : I) → Fin (Fintype.card I)) = e

Tactic:
ext x
-- 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 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Equiv.symm (Fintype.equivFin I)) : (a : Fin (Fintype.card I)) → I)
x : I
⊢ ((⇑f : (a : R) → S) ∘ e' ∘ (⇑(Fintype.equivFin I) : (a : I) → Fin (Fintype.card I))) x = e x

Tactic:
simpa using congr_fun h₂ (Fintype.equivFin I x)

Premises used: Fintype.equivFin, congr_fun, 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 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Equiv.symm (Fintype.equivFin I)) : (a : Fin (Fintype.card I)) → I)
⊢ ∃ (e' : I → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e

Tactic:
refine ⟨_, ((equiv (Fintype.equivFin I)).mpr h₁),
    by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
simp : e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * (e₂ * e₁) - (e₂ * (e₂ * e₁) - e₂)) = e₁ - e₂
⊢ HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂

Tactic:
simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq,
      H'.eq, mul_assoc]

Premises used: mul_sub, pow_succ, mul_assoc, pow_zero, sub_mul, IsIdempotentElem.eq, Commute.eq, one_mul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
simp : e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * e₁ - (e₂ * e₁ - e₂)) = e₁ - e₂
⊢ e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * (e₂ * e₁) - (e₂ * (e₂ * e₁) - e₂)) = e₁ - e₂

Tactic:
simp only [← mul_assoc, he₂.eq]

Premises used: mul_assoc, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * e₁ - (e₂ * e₁ - e₂)) = e₁ - e₂

Tactic:
abel
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂

Tactic:
have : (e₁ - e₂) ^ 3 = (e₁ - e₂) := by
    simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq,
      H'.eq, mul_assoc]
    simp only [← mul_assoc, he₂.eq]
    abel
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
this : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
obtain : ∀ (n : ℕ) (hn : (e₁ - e₂) ^ n = 0), e₁ = e₂
⊢ e₁ = e₂

Tactic:
obtain ⟨n, hn⟩ := H
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
zero : (e₁ - e₂) ^ (HMul.hMul (α := ℕ) 2 0 + 1) = e₁ - e₂
succ : ∀ (n : ℕ), (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂ → (e₁ - e₂) ^ (2 * (n + 1) + 1) = e₁ - e₂
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂

Tactic:
induction n
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
⊢ (e₁ - e₂) ^ (HMul.hMul (α := ℕ) 2 0 + 1) = e₁ - e₂

Tactic:
simp [mul_add, add_assoc, pow_add _ (2 * _) 3, ← pow_succ, *]

Premises used: HMul.hMul, pow_succ, add_assoc, pow_add, mul_add, OfNat.ofNat
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
h : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
⊢ (e₁ - e₂) ^ (2 * (n + 1) + 1) = e₁ - e₂

Tactic:
simp [mul_add, add_assoc, pow_add _ (2 * _) 3, ← pow_succ, *]

Premises used: HMul.hMul, pow_succ, add_assoc, pow_add, mul_add, OfNat.ofNat