awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Topology (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
hs : s ∈ 𝓝 a
t : Set A
ht : t ∈ F.addGroupFilterBasis
hts : (fun (y : A) ↦ a + y) '' t ⊆ s
⊢ ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
have mp : ∀ (I : Ideal A) (hI : I ∈ F) (hts : (fun (y : A) ↦ a + y) '' (↑I : Set A) ⊆ s),
  ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
Tactic: rcases ht with ⟨I, hI, rfl⟩
Cleared hypotheses: t, ht, hts
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Topology (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
I : Ideal A
hI : I ∈ F
hIs : HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
⊢ s ∈ 𝓝 a
have mpr : ∃ i ∈ F.addGroupFilterBasis, (fun (y : A) ↦ a + y) '' i ⊆ s
Tactic: refine ((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.2 ?_
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : DecidableEq I
he : OrthogonalIdempotents e
i j : I
⊢ e i * e j = if i = j then e i else 0
have isTrue : i = j → e i * e j = e i
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : DecidableEq I
he : OrthogonalIdempotents e
i j : I
isTrue : i = j → e i * e j = e i
⊢ e i * e j = if i = j then e i else 0
have isFalse : ¬i = j → e i * e j = 0
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ (fun (x1 x2 : Option I) ↦ x1.elim x e * x2.elim x e = 0) i j
have none : ∀ (ne : none ≠ j), Option.elim none x e * j.elim x e = 0
Tactic: rcases i with - | i
Cleared hypotheses: i, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ i.elim x e * j.elim x e = 0
have some : ∀ (i : I) (ne : some i ≠ j), (some i).elim x e * j.elim x e = 0
Tactic: rcases i with - | i
Cleared hypotheses: i, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : Option I
ne : none ≠ j
⊢ Option.elim none x e * j.elim x e = 0
have none : ∀ (ne : Ne.{u_3 + 1} (α := Option I) none none), Option.elim none x e * Option.elim none x e = 0
Tactic: rcases j with - | j
Cleared hypotheses: j, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : Option I
ne : Option.none ≠ j
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
⊢ Option.elim Option.none x e * j.elim x e = 0
have none₁ : ∀ (j : I) (ne : Option.none ≠ some j), Option.elim Option.none x e * (some j).elim x e = 0
Tactic: rcases j with - | j
Cleared hypotheses: j, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : Option I
i : I
ne : some i ≠ j
⊢ (some i).elim x e * j.elim x e = 0
have some : ∀ (ne : some i ≠ none), (some i).elim x e * Option.elim none x e = 0
Tactic: rcases j with - | j
Cleared hypotheses: j, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 : Option I
i : I
ne : Option.some i ≠ j
some : ∀ (ne : Option.some i ≠ none), (Option.some i).elim x e * Option.elim none x e = 0
⊢ (Option.some i).elim x e * j.elim x e = 0
have some₁ : ∀ (j : I) (ne : Option.some i ≠ Option.some j), (Option.some i).elim x e * (Option.some j).elim x e = 0
Tactic: rcases j with - | j
Cleared hypotheses: j, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ (fun (x1 x2 : Option I) ↦ x1.elim x e * x2.elim x e = 0) i j
have none : ∀ (ne : none ≠ j), Option.elim none 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)
Cleared hypotheses: i, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ i.elim x e * j.elim x e = 0
have some : ∀ (i : I) (ne : some i ≠ j), (some 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)
Cleared hypotheses: i, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ i.elim x e * j.elim x e = 0
have 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
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)
Cleared hypotheses: i, j, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ i.elim x e * j.elim x e = 0
have none₅ : ∀ (j : I) (ne : Option.none ≠ Option.some j), Option.elim Option.none x e * (Option.some 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)
Cleared hypotheses: i, j, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ i.elim x e * j.elim x e = 0
have some₄ : ∀ (i : I) (ne : Option.some i ≠ Option.none), (Option.some i).elim x e * Option.elim Option.none 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)
Cleared hypotheses: i, j, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ i.elim x e * j.elim x e = 0
have some₅ : ∀ (i j : I) (ne : Option.some i ≠ Option.some j), (Option.some i).elim x e * (Option.some 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)
Cleared hypotheses: i, j, ne
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
⊢ CompleteOrthogonalIdempotents e ↔
    (Pairwise fun (x1 x2 : I) ↦ e x1 * e x2 = 0) ∧ Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
have 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)
Tactic: rw [completeOrthogonalIdempotents_iff, orthogonalIdempotents_iff, and_assoc, and_iff_right_of_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (hypothesis)
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
⊢ IsIdempotentElem (e i)
have complete₁ : e i * ∑ i : I, e i = e i * 1
Tactic: apply_fun (e i * ·) at complete
Cleared hypotheses: complete
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ IsIdempotentElem (e i)
have rwa : ∀ (complete : ∑ i_1 : I, e i * e i_1 = e i * 1), 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
Cleared hypotheses: complete
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ IsIdempotentElem (e i)
have rwa₁ : ∀ (complete : e i * e i = e i * 1), 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
Cleared hypotheses: complete
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ IsIdempotentElem (e i)
have rwa₂ : ∀ (complete : e i * e i = 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
Cleared hypotheses: complete
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_4
inst : CommSemiring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ x + y = 1
have rw : x * y = 0 ∧ x + y = 1 → y * x = 0
Tactic: rw [pair_iff'ₛ, and_left_comm, and_iff_right_of_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Fintype I
inst_2 : Unique I
⊢ CompleteOrthogonalIdempotents e ↔ e default = 1
have rw : e default = 1 → IsIdempotentElem (e default)
Tactic: rw [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.unique, Fintype.sum_unique,
    and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
I : Type u_4
inst : Fintype I
inst_1 : DecidableEq I
R : I → Type u_5
inst_2 : (i : I) → Semiring (R i)
⊢ CompleteOrthogonalIdempotents (R := (j : I) → R j) fun (x : I) ↦ Pi.single (M := R) x 1
have 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
Tactic: refine ⟨⟨by simp [IsIdempotentElem, ← Pi.single_mul], ?_⟩, Finset.univ_sum_single 1⟩
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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) (Pi.single (M := R) i 1) (Pi.single (M := R) j 1) = 0
have 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
Tactic: ext k
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ 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
have 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
Tactic: by_cases hi : i = k
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ 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
have 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
Tactic: by_cases hi : i = k
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
have 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
Tactic: subst hi
Cleared hypotheses: k, hi
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
| 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2
have rw : (1 - (1 - x ^ n) ^ n) * (1 - x ^ n) ^ n
Tactic: rw [pow_two, ← mul_one_sub, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
have conv_rhs : (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ (1 - (1 - x ^ n) ^ n) * (1 - x ^ n) ^ n
Tactic: conv_rhs => rw [pow_two, ← mul_one_sub, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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) * (1 - x ^ n) ^ n
have 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
Tactic: nth_rw 1 3 [← one_pow n]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 ∣ (HPow.hPow (α := R) 1 n - (1 - x ^ n) ^ n) * (HPow.hPow (α := R) 1 n - x ^ n) ^ n
have 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
Tactic: rw [← (Commute.one_left x).mul_geom_sum₂, ← (Commute.one_left (1 - x ^ n)).mul_geom_sum₂]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)) * ∑ 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
have 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
Tactic: simp only [sub_sub_cancel, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 ^ 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
have 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)
Tactic: rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ (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
have h : Commute x (1 - x)
Tactic: rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ (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
have hbc : Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)
Tactic: rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]