awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
hn : (e₁ - e₂) ^ n = 0
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂

Tactic:
have : (e₁ - e₂) ^ (2 * n + 1) = (e₁ - e₂) := by
    clear hn; induction n <;> simp [mul_add, add_assoc, pow_add _ (2 * _) 3, ← pow_succ, *]
-- 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_1 : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
rwa : ∀ (this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₁ : ∀ (this : (e₁ - e₂) ^ (n + n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₂ : ∀ (this : (e₁ - e₂) ^ n * (e₁ - e₂) ^ n * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₃ : ∀ (this : HMul.hMul (α := R) 0 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₄ : ∀ (this : 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₅ : ∀ (this : 0 = e₁ - e₂), e₁ = e₂
rwa₆ : ∀ (this : e₁ - e₂ = 0), e₁ = e₂
rwa₇ rwa₈ rwa₉ rwa₁₀ : ∀ (this : e₁ = e₂), e₁ = e₂
⊢ e₁ = e₂

Tactic:
rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this

Premises used: sub_eq_zero, pow_succ, MulZeroClass.zero_mul, two_mul, pow_add, 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
I : Type u_3
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
obtain :
  ∀ (e' : I → R) (h₁ : CompleteOrthogonalIdempotents e')
    (h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)), CompleteOrthogonalIdempotents e
⊢ CompleteOrthogonalIdempotents e

Tactic:
obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker f h he'' (fun _ ↦ ⟨_, rfl⟩)

Premises used: CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)
h₃ : ∀ (i : I), e i = e' i
⊢ e = e'

Tactic:
ext i
-- 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
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)
i : I
⊢ e i = e' i

Tactic:
eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
      (he _) (h₁.idem _) (h _ ?_) ((he' i).comm _)

Premises used: CompleteOrthogonalIdempotents.toOrthogonalIdempotents, OrthogonalIdempotents.idem, IsMulCentral.comm, eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
-- 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
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)
i : I
h₃ : Membership.mem (γ := Ideal R) (RingHom.ker f) (e i - e' i)
⊢ e i = e' i

Tactic:
refine eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
      (he _) (h₁.idem _) (h _ ?_) ((he' i).comm _)

Premises used: CompleteOrthogonalIdempotents.toOrthogonalIdempotents, OrthogonalIdempotents.idem, IsMulCentral.comm, eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
-- 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
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)
i : I
⊢ Membership.mem (γ := Ideal R) (RingHom.ker f) (e i - e' i)

Tactic:
simpa [RingHom.mem_ker, sub_eq_zero] using congr_fun h₂.symm i

Premises used: sub_eq_zero, RingHom.mem_ker, congr_fun, Eq.symm
-- 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
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)
⊢ CompleteOrthogonalIdempotents e

Tactic:
obtain rfl : e = e' := by
    ext i
    refine eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
      (he _) (h₁.idem _) (h _ ?_) ((he' i).comm _)
    simpa [RingHom.mem_ker, sub_eq_zero] using congr_fun h₂.symm i

Premises used: rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)
h₃ : CompleteOrthogonalIdempotents e
⊢ Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e) ((⇑f : (a : R) → S) ∘ e)

Tactic:
obtain rfl : e = e' := by
    ext i
    refine eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
      (he _) (h₁.idem _) (h _ ?_) ((he' i).comm _)
    simpa [RingHom.mem_ker, sub_eq_zero] using congr_fun h₂.symm i

Premises used: rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
h₁ : CompleteOrthogonalIdempotents e
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e) ((⇑f : (a : R) → S) ∘ e)
⊢ CompleteOrthogonalIdempotents e

Tactic:
h₁
-- 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
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
h₁ : CompleteOrthogonalIdempotents e
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e) ((⇑f : (a : R) → S) ∘ e)
⊢ CompleteOrthogonalIdempotents e

Tactic:
exact h₁
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
⊢ e₁ = e₂

Tactic:
eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute he₁ he₂ H (.all _ _)

Premises used: eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute, Commute.all
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : CommRing 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
obtain :
  ∀ (e' : R) (he₂ : IsIdempotentElem e')
    (he :
      Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f)
        ((f : (a : R) → S) e' : S))
    (he' : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)),
    ∃! e'_1 : R, IsIdempotentElem e'_1 ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S)
⊢ ∃! e' : R, IsIdempotentElem e' ∧ (f : (a : R) → S) e' = e

Tactic:
obtain ⟨e', he₂, rfl⟩ := exists_isIdempotentElem_eq_of_ker_isNilpotent f h e he he'

Premises used: exists_isIdempotentElem_eq_of_ker_isNilpotent, rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : CommRing 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'
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he' : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
x : R
h_1 :
  (fun (e'_1 : R) ↦
      IsIdempotentElem e'_1 ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S))
    x
hx : IsIdempotentElem x
hx' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) e' : S)
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x - e') : S) (0 : S)
rw₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) e' : S) = 0
rw₂ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e' : S) = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := S) 0 0
⊢ Membership.mem (γ := Ideal R) (RingHom.ker f) (x - e')

Tactic:
rw [RingHom.mem_ker, map_sub, hx', sub_self]

Premises used: map_sub, sub_self, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : CommRing 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'
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he' : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
⊢ ∃! e'_1 : R, IsIdempotentElem e'_1 ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S)

Tactic:
exact ⟨e', ⟨he₂, rfl⟩, fun x ⟨hx, hx'⟩ ↦
    eq_of_isNilpotent_sub_of_isIdempotentElem hx he₂
      (h _ (by rw [RingHom.mem_ker, map_sub, hx', sub_self]))⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})
obtain :
  ∀ (x : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i})),
    ∃ (a : R),
      Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
        ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
                Ideal.Quotient.mk (Ideal.span {1 - e i}) :
              (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
            a :
          (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
        ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
              (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
            x :
          (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
⊢ ∃ (a : R),
    (Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
            Ideal.Quotient.mk (Ideal.span {1 - e i}) :
          (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
        a =
      x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.quotientInfToPiQuotient_surj this x

Premises used: Ideal.quotientInfToPiQuotient_surj, rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i})
obtain :
  ∀ (x : R),
    ∃ (a : R),
      Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
        ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
                Ideal.Quotient.mk (Ideal.span {1 - e i}) :
              (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
            a :
          (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
        ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
              (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
            ((Ideal.Quotient.mk (⨅ (i : I), Ideal.span {1 - e i}) : (a : R) → R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) x :
              HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i})) :
          (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
⊢ ∃ (a : R),
    Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
              Ideal.Quotient.mk (Ideal.span {1 - e i}) :
            (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
          a :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
            (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
          x :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
h :
  ∀ (i : I),
    Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
              Ideal.Quotient.mk (Ideal.span {1 - e i}) :
            (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
          x i :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
            (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
          ((Ideal.Quotient.mk (⨅ (i : I), Ideal.span {1 - e i}) : (a : R) → R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) x :
            HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i}))
          i :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
⊢ Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
            Ideal.Quotient.mk (Ideal.span {1 - e i}) :
          (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
        x :
      (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
          (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
        ((Ideal.Quotient.mk (⨅ (i : I), Ideal.span {1 - e i}) : (a : R) → R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) x :
          HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i})) :
      (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))

Tactic:
ext i
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
i : I
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
            Ideal.Quotient.mk (Ideal.span {1 - e i}) :
          (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
        x i :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
          (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
        ((Ideal.Quotient.mk (⨅ (i : I), Ideal.span {1 - e i}) : (a : R) → R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) x :
          HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i}))
        i :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))

Tactic:
simp [Ideal.quotientInfToPiQuotient]

Premises used: Ideal.quotientInfToPiQuotient
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
⊢ ∃ (a : R),
    Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
              Ideal.Quotient.mk (Ideal.span {1 - e i}) :
            (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
          a :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
            (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
          ((Ideal.Quotient.mk (⨅ (i : I), Ideal.span {1 - e i}) : (a : R) → R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) x :
            HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i})) :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))

Tactic:
exact ⟨x, by ext i; simp [Ideal.quotientInfToPiQuotient]⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
suffices : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
⊢ Function.Surjective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {1 - e i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})

Tactic:
suffices Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j}) by
    intro x
    obtain ⟨x, rfl⟩ := Ideal.quotientInfToPiQuotient_surj this x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact ⟨x, by ext i; simp [Ideal.quotientInfToPiQuotient]⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
rw : IsCoprime (1 - e i) (1 - e j)
⊢ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})

Tactic:
rw [Ideal.isCoprime_span_singleton_iff]

Premises used: Ideal.isCoprime_span_singleton_iff
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ 1 * (1 - e i) + e i * (1 - e j) = 1

Tactic:
simp [mul_sub, he.ortho hij]

Premises used: mul_sub, OrthogonalIdempotents.ortho
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (1 - e i) (1 - e j)

Tactic:
exact ⟨1, e i, by simp [mul_sub, he.ortho hij]⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
⊢ ∏ i ∈ ∅, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ ∅, e i)

Tactic:
simp
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
a : I
s : Finset I
has : a ∉ s
ih : ∏ i ∈ s, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ s, e i)
⊢ ∏ i ∈ Finset.cons a s has, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ Finset.cons a s has, e i)

Tactic:
simp [ih, sub_mul, mul_sub, he.mul_sum_of_notMem has, sub_sub]

Premises used: mul_sub, OrthogonalIdempotents.mul_sum_of_notMem, sub_mul, sub_sub
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
empty : ∏ i ∈ ∅, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ ∅, e i)
cons :
  ∀ (a : I) (s : Finset I) (has : a ∉ s) (ih : ∏ i ∈ s, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ s, e i)),
    ∏ i ∈ Finset.cons a s has, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ Finset.cons a s has, e i)
⊢ ∏ i ∈ s, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ s, e i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s has ih =>
    simp [ih, sub_mul, mul_sub, he.mul_sum_of_notMem has, sub_sub]

Premises used: mul_sub, sub_mul, sub_sub
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
f : R →+* S
I : Type u_3
inst_2 : Fintype I
e : I → R
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
⊢ CompleteOrthogonalIdempotents e

Tactic:
of_ker_isNilpotent_of_isMulCentral f h he
    (fun _ ↦ Semigroup.mem_center_iff.mpr (mul_comm · _)) he'

Premises used: Iff.mpr, Semigroup.mem_center_iff, mul_comm, CompleteOrthogonalIdempotents.of_ker_isNilpotent_of_isMulCentral
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
rw : HSub.hSub (α := R) 1 (∑ i : I, e i) = 0
rw₁ : HSub.hSub (α := R) 1 1 = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (∏ i : I, (1 - e i)) 0

Tactic:
rw [he.1.prod_one_sub, he.complete, sub_self]

Premises used: sub_self, OrthogonalIdempotents.prod_one_sub, CompleteOrthogonalIdempotents.toOrthogonalIdempotents, CompleteOrthogonalIdempotents.complete
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : OrthogonalIdempotents e
he' : Eq.{u_1 + 1} (α := R) (∏ i : I, (1 - e i)) 0
rwa : ∀ (he' : HSub.hSub (α := R) 1 (∑ i : I, e i) = 0), Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
rwa₁ : ∀ (he' : Eq.{u_1 + 1} (α := R) 1 (∑ i : I, e i)), Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (he' : Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1), Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1

Tactic:
rwa [he.prod_one_sub, sub_eq_zero, eq_comm] at he'

Premises used: sub_eq_zero, OrthogonalIdempotents.prod_one_sub, eq_comm