awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst_1 : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
ne : Ne.{u_3 + 1} (α := Option I) none none
⊢ Option.elim none x e * Option.elim none x e = 0

Tactic:
cases ne rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst_1 : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
j : I
ne : none ≠ some j
⊢ Option.elim none x e * (some j).elim x e = 0

Tactic:
simpa only [mul_assoc, Finset.sum_mul, he.mul_eq, Finset.sum_ite_eq', Finset.mem_univ,
        ↓reduceIte, zero_mul] using congr_arg (· * e j) hx₁

Premises used: Finset.mem_univ, HMul.hMul, Finset.sum_ite_eq', MulZeroClass.zero_mul, mul_assoc, congr_arg, OrthogonalIdempotents.mul_eq, reduceIte, Finset.sum_mul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst_1 : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
i : I
ne : some i ≠ none
⊢ (some i).elim x e * Option.elim none x e = 0

Tactic:
simpa only [Option.elim_some, Option.elim_none, ← mul_assoc, Finset.mul_sum, he.mul_eq,
        Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, mul_zero] using congr_arg (e i * ·) hx₂

Premises used: Finset.mem_univ, Finset.mul_sum, HMul.hMul, mul_assoc, Option.elim_none, Option.elim_some, MulZeroClass.mul_zero, congr_arg, OrthogonalIdempotents.mul_eq, reduceIte, Finset.sum_ite_eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst_1 : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0

Tactic:
he.ortho (Option.some_inj.ne.mp ne)

Premises used: OrthogonalIdempotents.ortho, Iff.ne, Iff.mp, Option.some_inj
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst_1 : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0

Tactic:
exact he.ortho (Option.some_inj.ne.mp ne)

Premises used: OrthogonalIdempotents.ortho, Iff.ne, Iff.mp, Option.some_inj
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst_1 : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
i j : Option I
ne : i ≠ j
none : ∀ (ne : Option.none ≠ j), Option.elim Option.none x e * j.elim x e = 0
some : ∀ (i : I) (ne : Option.some i ≠ j), (Option.some i).elim x e * j.elim x e = 0
none₁ : ∀ (ne : Option.none ≠ j), Option.elim Option.none x e * j.elim x e = 0
some₁ : ∀ (i : I) (ne : Option.some i ≠ j), (Option.some i).elim x e * j.elim x e = 0
none₂ : ∀ (ne : Option.none ≠ j), Option.elim Option.none x e * j.elim x e = 0
some₂ : ∀ (i : I) (ne : Option.some i ≠ j), (Option.some i).elim x e * j.elim x e = 0
none₃ : ∀ (ne : Option.none ≠ j), Option.elim Option.none x e * j.elim x e = 0
some₃ : ∀ (i : I) (ne : Option.some i ≠ j), (Option.some i).elim x e * j.elim x e = 0
none₄ :
  ∀ (ne : Ne.{u_3 + 1} (α := Option I) Option.none Option.none),
    Option.elim Option.none x e * Option.elim Option.none x e = 0
none₅ : ∀ (j : I) (ne : Option.none ≠ Option.some j), Option.elim Option.none x e * (Option.some j).elim x e = 0
some₄ : ∀ (i : I) (ne : Option.some i ≠ Option.none), (Option.some i).elim x e * Option.elim Option.none x e = 0
some₅ : ∀ (i j : I) (ne : Option.some i ≠ Option.some j), (Option.some i).elim x e * (Option.some j).elim x e = 0
none₆ : ∀ (j : I) (ne : Option.none ≠ Option.some j), Option.elim Option.none x e * (Option.some j).elim x e = 0
some₆ : ∀ (i : I) (ne : Option.some i ≠ Option.none), (Option.some i).elim x e * Option.elim Option.none x e = 0
some₇ : ∀ (i j : I) (ne : Option.some i ≠ Option.some j), (Option.some i).elim x e * (Option.some j).elim x e = 0
some₈ : ∀ (i : I) (ne : Option.some i ≠ Option.none), (Option.some i).elim x e * Option.elim Option.none x e = 0
some₉ some₁₀ : ∀ (i j : I) (ne : Option.some i ≠ Option.some j), (Option.some i).elim x e * (Option.some j).elim x e = 0
⊢ i.elim x e * j.elim x e = 0

Tactic:
classical
    rcases i with - | i <;> rcases j with - | j
    · cases ne rfl
    · simpa only [mul_assoc, Finset.sum_mul, he.mul_eq, Finset.sum_ite_eq', Finset.mem_univ,
        ↓reduceIte, zero_mul] using congr_arg (· * e j) hx₁
    · simpa only [Option.elim_some, Option.elim_none, ← mul_assoc, Finset.mul_sum, he.mul_eq,
        Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, mul_zero] using congr_arg (e i * ·) hx₂
    · exact he.ortho (Option.some_inj.ne.mp ne)

Premises used: Finset.mem_univ, Finset.mul_sum, Finset.sum_ite_eq', MulZeroClass.zero_mul, mul_assoc, Option.elim_none, Option.elim_some, MulZeroClass.mul_zero, reduceIte, Finset.sum_ite_eq, Finset.sum_mul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
rw :
  (Pairwise fun (x1 x2 : I) ↦ e x1 * e x2 = 0) ∧ Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1 →
    ∀ (i : I), IsIdempotentElem (e i)
⊢ CompleteOrthogonalIdempotents e ↔
    (Pairwise fun (x1 x2 : I) ↦ e x1 * e x2 = 0) ∧ Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1

Tactic:
rw [completeOrthogonalIdempotents_iff, orthogonalIdempotents_iff, and_assoc, and_iff_right_of_imp]

Premises used: orthogonalIdempotents_iff, completeOrthogonalIdempotents_iff, and_assoc, and_iff_right_of_imp
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
ortho : Pairwise fun (x1 x2 : I) ↦ e x1 * e x2 = 0
complete : Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
i : I
⊢ e i * ∑ i : I, e i = e i * 1

Tactic:
apply_fun (e i * ·) at complete

Premises used: HMul.hMul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
ortho : Pairwise fun (x1 x2 : I) ↦ e x1 * e x2 = 0
i : I
complete : e i * ∑ i : I, e i = e i * 1
rwa : ∀ (complete : ∑ i_1 : I, e i * e i_1 = e i * 1), IsIdempotentElem (e i)
rwa₁ : ∀ (complete : e i * e i = e i * 1), IsIdempotentElem (e i)
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (complete : e i * e i = e i), IsIdempotentElem (e i)
⊢ IsIdempotentElem (e i)

Tactic:
rwa [Finset.mul_sum, Finset.sum_eq_single i (fun _ _ ne ↦ ortho ne.symm) (by simp at ·), mul_one]
    at complete

Premises used: Finset.mul_sum, Ne.symm, Finset.sum_eq_single, mul_one
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ y * x = 0 ∧ x + y = 1

Tactic:
simp [iff_ortho_complete, Pairwise, Fin.forall_fin_two, and_assoc]

Premises used: Fin.forall_fin_two, CompleteOrthogonalIdempotents.iff_ortho_complete, and_assoc, Pairwise
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_4
inst : CommSemiring R
x y : R
rw : x * y = 0 ∧ x + y = 1 → y * x = 0
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ x + y = 1

Tactic:
rw [pair_iff'ₛ, and_left_comm, and_iff_right_of_imp]

Premises used: and_left_comm, CompleteOrthogonalIdempotents.pair_iff'ₛ, and_iff_right_of_imp
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_4
inst : CommSemiring R
x y : R
⊢ x * y = 0 ∧ x + y = 1 → y * x = 0

Tactic:
(mul_comm x y ▸ ·.1)

Premises used: Eq.rec, And.left, mul_comm
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_4
inst : CommSemiring R
x y : R
⊢ x * y = 0 ∧ x + y = 1 → y * x = 0

Tactic:
exact (mul_comm x y ▸ ·.1)
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
inst_2 : Unique I
rw : e default = 1 → IsIdempotentElem (e default)
⊢ CompleteOrthogonalIdempotents e ↔ e default = 1

Tactic:
rw [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.unique, Fintype.sum_unique,
    and_iff_right_iff_imp]

Premises used: Fintype.sum_unique, completeOrthogonalIdempotents_iff, and_iff_right_iff_imp, OrthogonalIdempotents.unique
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
inst_2 : Unique I
⊢ e default = 1 → IsIdempotentElem (e default)

Tactic:
(· ▸ IsIdempotentElem.one)

Premises used: IsIdempotentElem.one, Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
inst_2 : Unique I
⊢ e default = 1 → IsIdempotentElem (e default)

Tactic:
exact (· ▸ IsIdempotentElem.one)
-- Module: Mathlib.RingTheory.Idempotents
Goal:
I : Type u_4
inst : Fintype I
inst_1 : DecidableEq I
R : I → Type u_5
inst_2 : (i : I) → Semiring (R i)
⊢ ∀ (i : I), IsIdempotentElem (M := (j : I) → R j) (Pi.single (M := R) i 1)

Tactic:
simp [IsIdempotentElem, ← Pi.single_mul]

Premises used: IsIdempotentElem, Pi.single_mul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
I : Type u_4
inst : Fintype I
inst_1 : DecidableEq I
R : I → Type u_5
inst_2 : (i : I) → Semiring (R i)
refine :
  Pairwise fun (x1 x2 : I) ↦ HMul.hMul (α := (j : I) → R j) (Pi.single (M := R) x1 1) (Pi.single (M := R) x2 1) = 0
⊢ CompleteOrthogonalIdempotents (R := (j : I) → R j) fun (x : I) ↦ Pi.single (M := R) x 1

Tactic:
refine ⟨⟨by simp [IsIdempotentElem, ← Pi.single_mul], ?_⟩, Finset.univ_sum_single 1⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
I : Type u_4
inst : Fintype I
inst_1 : DecidableEq I
R : I → Type u_5
inst_2 : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
h :
  ∀ (k : I),
    HMul.hMul (α := (j : I) → R j) (β := (j : I) → R j) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) k = 0 k
⊢ HMul.hMul (α := (j : I) → R j) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) = 0

Tactic:
ext k
-- Module: Mathlib.RingTheory.Idempotents
Goal:
I : Type u_4
inst : Fintype I
inst_1 : DecidableEq I
R : I → Type u_5
inst_2 : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
pos :
  ∀ (hi : i = k),
    HMul.hMul (α := (j : I) → R j) (β := (j : I) → R j) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) k = 0 k
neg :
  ∀ (hi : ¬i = k),
    HMul.hMul (α := (j : I) → R j) (β := (j : I) → R j) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) k = 0 k
⊢ HMul.hMul (α := (j : I) → R j) (β := (j : I) → R j) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) k = 0 k

Tactic:
by_cases hi : i = k
-- Module: Mathlib.RingTheory.Idempotents
Goal:
I : Type u_4
inst : Fintype I
inst_1 : DecidableEq I
R : I → Type u_5
inst_2 : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
hi : i = k
pos : HMul.hMul (α := (j : I) → R j) (β := (j : I) → R j) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) i = 0 i
⊢ HMul.hMul (α := (j : I) → R j) (β := (j : I) → R j) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) k = 0 k

Tactic:
subst hi
-- Module: Mathlib.RingTheory.Idempotents
Goal:
I : Type u_4
inst : Fintype I
inst_1 : DecidableEq I
R : I → Type u_5
inst_2 : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
⊢ HMul.hMul (α := (j : I) → R j) (β := (j : I) → R j) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) i = 0 i

Tactic:
simp [hij]
-- Module: Mathlib.RingTheory.Idempotents
Goal:
I : Type u_4
inst : Fintype I
inst_1 : DecidableEq I
R : I → Type u_5
inst_2 : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
hi : ¬i = k
⊢ HMul.hMul (α := (j : I) → R j) (β := (j : I) → R j) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) k = 0 k

Tactic:
simp [hi]
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
I : Type u_3
e : I → R
inst_2 : Fintype I
he : CompleteOrthogonalIdempotents e
⊢ Eq.{u_2 + 1} (α := S) (∑ i : I, ((⇑f : (a : R) → S) ∘ e) i) 1

Tactic:
simp only [Function.comp_apply, ← map_sum, he.complete, map_one]

Premises used: map_sum, map_one, CompleteOrthogonalIdempotents.complete, Function.comp_apply
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
I : Type u_3
e : I → R
inst_2 : Fintype I
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e) ↔ CompleteOrthogonalIdempotents e

Tactic:
simp [completeOrthogonalIdempotents_iff, ← hf.eq_iff,
    OrthogonalIdempotents.map_injective_iff f hf]

Premises used: Function.Injective.eq_iff, completeOrthogonalIdempotents_iff, OrthogonalIdempotents.map_injective_iff
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
J : Type u_4
inst_2 : Fintype J
i : J ≃ I
⊢ CompleteOrthogonalIdempotents.{u_1, u_4} (I := J) (e ∘ (⇑i : (a : J) → I)) ↔ CompleteOrthogonalIdempotents e

Tactic:
simp only [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.equiv, Function.comp_apply,
    Fintype.sum_equiv i _ e (fun _ ↦ rfl)]

Premises used: OrthogonalIdempotents.equiv, completeOrthogonalIdempotents_iff, Function.comp_apply, Fintype.sum_equiv, rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
inst_2 : Subsingleton R
⊢ CompleteOrthogonalIdempotents e

Tactic:
⟨⟨fun _ ↦ Subsingleton.elim _ _, fun _ _ _ ↦ Subsingleton.elim _ _⟩, Subsingleton.elim _ _⟩

Premises used: HMul.hMul, CompleteOrthogonalIdempotents.mk, OrthogonalIdempotents.mk, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
rw : (1 - (1 - x ^ n) ^ n) * (1 - x ^ n) ^ n
| 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2

Tactic:
rw [pow_two, ← mul_one_sub, sub_sub_cancel]

Premises used: pow_two, mul_one_sub, sub_sub_cancel
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
conv_rhs : (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ (1 - (1 - x ^ n) ^ n) * (1 - x ^ n) ^ n
⊢ (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2

Tactic:
conv_rhs => rw [pow_two, ← mul_one_sub, sub_sub_cancel]

Premises used: pow_two, mul_one_sub, sub_sub_cancel
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
nth_rw :
  (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ (HPow.hPow (α := R) 1 n - (1 - x ^ n) ^ n) * (HPow.hPow (α := R) 1 n - x ^ n) ^ n
⊢ (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ (1 - (1 - x ^ n) ^ n) * (1 - x ^ n) ^ n

Tactic:
nth_rw 1 3 [← one_pow n]

Premises used: one_pow
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
rw :
  (x - HPow.hPow (β := ℕ) x 2) ^ n ∣
    ((1 - (1 - x ^ n)) * ∑ i ∈ Finset.range n, HPow.hPow (α := R) 1 i * (1 - x ^ n) ^ (n - 1 - i)) *
      ((1 - x) * ∑ i ∈ Finset.range n, HPow.hPow (α := R) 1 i * x ^ (n - 1 - i)) ^ n
⊢ (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ (HPow.hPow (α := R) 1 n - (1 - x ^ n) ^ n) * (HPow.hPow (α := R) 1 n - x ^ n) ^ n

Tactic:
rw [← (Commute.one_left x).mul_geom_sum₂, ← (Commute.one_left (1 - x ^ n)).mul_geom_sum₂]

Premises used: HSub.hSub, Commute.mul_geom_sum₂, HPow.hPow, OfNat.ofNat, Commute.one_left
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
simp :
  (x - HPow.hPow (β := ℕ) x 2) ^ n ∣
    (x ^ n * ∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
      ((1 - x) * ∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n
⊢ (x - HPow.hPow (β := ℕ) x 2) ^ n ∣
    ((1 - (1 - x ^ n)) * ∑ i ∈ Finset.range n, HPow.hPow (α := R) 1 i * (1 - x ^ n) ^ (n - 1 - i)) *
      ((1 - x) * ∑ i ∈ Finset.range n, HPow.hPow (α := R) 1 i * x ^ (n - 1 - i)) ^ n

Tactic:
simp only [sub_sub_cancel, one_pow, one_mul]

Premises used: one_pow, sub_sub_cancel, one_mul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
rw :
  (x - HPow.hPow (β := ℕ) x 2) ^ n ∣
    (x - HPow.hPow (β := ℕ) x 2) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
        HPow.hPow (α := R) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) n)
h : Commute x (1 - x)
hbc : Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)
h₁ : Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))
⊢ (x - HPow.hPow (β := ℕ) x 2) ^ n ∣
    (x ^ n * ∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
      ((1 - x) * ∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n

Tactic:
rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]

Premises used: Commute.mul_mul_mul_comm, pow_two, mul_one_sub, Commute.mul_pow
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
⊢ (x - HPow.hPow (β := ℕ) x 2) ^ n ∣
    (x - HPow.hPow (β := ℕ) x 2) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
        HPow.hPow (α := R) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) n)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
⊢ (x - HPow.hPow (β := ℕ) x 2) ^ n ∣
    (x - HPow.hPow (β := ℕ) x 2) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
        HPow.hPow (α := R) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) n)

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
⊢ Commute x (1 - x)

Tactic:
simp
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

Tactic:
.pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _

Premises used: Commute.pow_right
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
hbc : ∀ x_1 ∈ Finset.range n, Commute (1 - x ^ n) x
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

Tactic:
refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
x_1 : ℕ
h : x_1 ∈ Finset.range n
⊢ Commute (1 - x ^ n) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))

Tactic:
.sub_left (.one_left _) (.sum_right _ _ _ fun _ _ ↦ .pow_right rfl _)

Premises used: Commute.pow_right, HSub.hSub, Commute.sum_right, OfNat.ofNat, rfl, Commute.sub_left, Commute.one_left
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))

Tactic:
exact .sub_left (.one_left _) (.sum_right _ _ _ fun _ _ ↦ .pow_right rfl _)
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
⊢ (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2

Tactic:
have : (x - x ^ 2) ^ n ∣ (1 - (1 - x ^ n) ^ n) - (1 - (1 - x ^ n) ^ n) ^ 2 := by
    conv_rhs => rw [pow_two, ← mul_one_sub, sub_sub_cancel]
    nth_rw 1 3 [← one_pow n]
    rw [← (Commute.one_left x).mul_geom_sum₂, ← (Commute.one_left (1 - x ^ n)).mul_geom_sum₂]
    simp only [sub_sub_cancel, one_pow, one_mul]
    rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]
    · exact ⟨_, rfl⟩
    · simp
    · refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _
      simp
    · exact .sub_left (.one_left _) (.sum_right _ _ _ fun _ _ ↦ .pow_right rfl _)
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
this : (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2
rwa :
  ∀ (this : 0 ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2),
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₁ :
  ∀ (this : 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2 = 0),
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₂ :
  ∀ (this : 1 - (1 - x ^ n) ^ n = HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₃ :
  ∀ (this : HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2 = 1 - (1 - x ^ n) ^ n), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₄ rwa₅ rwa₆ rwa₇ :
  ∀ (this : (1 - (1 - x ^ n) ^ n) * (1 - (1 - x ^ n) ^ n) = 1 - (1 - x ^ n) ^ n), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
rwa [hx, zero_dvd_iff, sub_eq_zero, eq_comm, pow_two] at this

Premises used: pow_two, sub_eq_zero, zero_dvd_iff, eq_comm
-- 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
he₂ : IsIdempotentElem e₂
he₁e₂ : HMul.hMul (β := S) e₁ ((f : (a : R) → S) e₂ : S) = 0
obtain :
  ∀ (e₁ : R) (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),
    ∃ (e' : R),
      IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
⊢ ∃ (e' : R), IsIdempotentElem e' ∧ (f : (a : R) → S) e' = e₁ ∧ e' * e₂ = 0

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

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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
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
inl :
  Subsingleton R →
    ∃ (e' : R),
      IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
inr :
  Nontrivial R →
    ∃ (e' : R),
      IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0

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
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
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
h_1 : Subsingleton R
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0

Tactic:
⟨_, Subsingleton.elim _ _, rfl, Subsingleton.elim _ _⟩

Premises used: And.intro, Exists.intro, Subsingleton.elim, rfl