awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
⊢ 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})
have suffices : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
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]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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 (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
have rw : IsCoprime (1 - e i) (1 - e j)
Tactic: rw [Ideal.isCoprime_span_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
⊢ ∏ i ∈ s, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ s, e i)
have empty : ∏ i ∈ ∅, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ ∅, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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)
⊢ ∏ i ∈ s, (1 - e i) = HSub.hSub (α := R) 1 (∑ i ∈ s, e i)
have 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)
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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Eq.{u_1 + 1} (α := R) (∏ i : I, (1 - e i)) 0
have rw : HSub.hSub (α := R) 1 (∑ i : I, e i) = 0
Tactic: rw [he.1.prod_one_sub, he.complete, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∏ i : I, (1 - e i)) 0
have rw₁ : HSub.hSub (α := R) 1 1 = 0
Tactic: rw [he.1.prod_one_sub, he.complete, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∏ i : I, (1 - e i)) 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [he.1.prod_one_sub, he.complete, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
have rwa : ∀ (he' : HSub.hSub (α := R) 1 (∑ i : I, e i) = 0), Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
Tactic: rwa [he.prod_one_sub, sub_eq_zero, eq_comm] at he'
Cleared hypotheses: he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
have rwa₁ : ∀ (he' : Eq.{u_1 + 1} (α := R) 1 (∑ i : I, e i)), Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
Tactic: rwa [he.prod_one_sub, sub_eq_zero, eq_comm] at he'
Cleared hypotheses: he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i : I, e i) 1
have rwa₂ : ∀ (he' : 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'
Cleared hypotheses: he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Bijective (α := 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})
have refine : Function.Injective (α := 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: refine ⟨?_, he.1.surjective_pi⟩
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Injective (α := 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})
have rw : ∀ (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}))
      (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx :
  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}))
    (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
⊢ x = 0
have hx₁ : ∀ (x_1 : I), 1 - e x_1 ∣ x
Tactic: simp only [funext_iff, Pi.ringHom_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ x = 0
have rw : (∏ i : I, (1 - e i)) * x = 0
Tactic: rw [← this Finset.univ, he.prod_one_sub, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
rw : (∏ i : I, (1 - e i)) * x = 0
⊢ x = 0
have rw₁ : 0 * x = 0
Tactic: rw [← this Finset.univ, he.prod_one_sub, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
rw : (∏ i : I, (1 - e i)) * x = 0
rw₁ : 0 * x = 0
⊢ x = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← this Finset.univ, he.prod_one_sub, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
⊢ x = 0
have suffices : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
Tactic: suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
⊢ ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
have refine : ∀ (s : Finset I) (a : I) (s : Finset I), a ∉ s → (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * x = x
Tactic: refine fun s ↦ Finset.induction_on s (by simp) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s_1 : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
⊢ (∏ i ∈ insert a s, (1 - e i)) * x = x
have suffices : (1 - e a) * x = x
Tactic: suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s_1 : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
⊢ (1 - e a) * x = x
have obtain : ∀ (c : R) (hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c) (e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c),
  (1 - e a) * ((1 - e a) * c) = (1 - e a) * c
Tactic: obtain ⟨c, rfl⟩ := hx a
Cleared hypotheses: x, hx, e'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
s_1 : Finset I
a : I
s : Finset I
has : a ∉ s
c : R
hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c
e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c
⊢ (1 - e a) * ((1 - e a) * c) = (1 - e a) * c
have rw : (1 - e a) * (1 - e a) * c = (1 - e a) * c
Tactic: rw [← mul_assoc, (he.idem a).one_sub.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
s_1 : Finset I
a : I
s : Finset I
has : a ∉ s
c : R
hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c
e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c
rw : (1 - e a) * (1 - e a) * c = (1 - e a) * c
⊢ (1 - e a) * ((1 - e a) * c) = (1 - e a) * c
have rw₁ : (1 - e a) * c = (1 - e a) * c
Tactic: rw [← mul_assoc, (he.idem a).one_sub.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Bijective (α := 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})
have refine : Function.Injective (α := 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: classical
  refine ⟨?_, he.1.surjective_pi⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  simp only [funext_iff, Pi.ringHom_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx
  suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
  refine fun s ↦ Finset.induction_on s (by simp) ?_
  intro a s has e'
  suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
  obtain ⟨c, rfl⟩ := hx a
  rw [← mul_assoc, (he.idem a).one_sub.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
refine :
  Function.Injective (α := 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})
⊢ Function.Bijective (α := 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})
have refine₁ : ∀ (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}))
      (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) →
    a = 0
Tactic: classical
  refine ⟨?_, he.1.surjective_pi⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  simp only [funext_iff, Pi.ringHom_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx
  suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
  refine fun s ↦ Finset.induction_on s (by simp) ?_
  intro a s has e'
  suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
  obtain ⟨c, rfl⟩ := hx a
  rw [← mul_assoc, (he.idem a).one_sub.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
refine :
  Function.Injective (α := 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})
refine₁ refine₂ :
  ∀ (x : R)
    (hx :
      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}))
        (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))),
    x = 0
⊢ Function.Bijective (α := 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})
have refine₃ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x), x = 0
Tactic: classical
  refine ⟨?_, he.1.surjective_pi⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  simp only [funext_iff, Pi.ringHom_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx
  suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
  refine fun s ↦ Finset.induction_on s (by simp) ?_
  intro a s has e'
  suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
  obtain ⟨c, rfl⟩ := hx a
  rw [← mul_assoc, (he.idem a).one_sub.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
refine :
  Function.Injective (α := 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})
refine₁ refine₂ :
  ∀ (x : R)
    (hx :
      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}))
        (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))),
    x = 0
refine₃ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x), x = 0
⊢ Function.Bijective (α := 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})
have refine₄ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x) (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
Tactic: classical
  refine ⟨?_, he.1.surjective_pi⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  simp only [funext_iff, Pi.ringHom_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx
  suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
  refine fun s ↦ Finset.induction_on s (by simp) ?_
  intro a s has e'
  suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
  obtain ⟨c, rfl⟩ := hx a
  rw [← mul_assoc, (he.idem a).one_sub.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
refine :
  Function.Injective (α := 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})
refine₁ refine₂ :
  ∀ (x : R)
    (hx :
      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}))
        (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))),
    x = 0
refine₃ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x), x = 0
refine₄ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x) (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ Function.Bijective (α := 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})
have refine₅ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x) (s : Finset I) (a : I) (s : Finset I),
  a ∉ s → (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * x = x
Tactic: classical
  refine ⟨?_, he.1.surjective_pi⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  simp only [funext_iff, Pi.ringHom_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx
  suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
  refine fun s ↦ Finset.induction_on s (by simp) ?_
  intro a s has e'
  suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
  obtain ⟨c, rfl⟩ := hx a
  rw [← mul_assoc, (he.idem a).one_sub.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
refine :
  Function.Injective (α := 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})
refine₁ refine₂ :
  ∀ (x : R)
    (hx :
      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}))
        (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))),
    x = 0
refine₃ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x), x = 0
refine₄ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x) (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
refine₅ refine₆ :
  ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x) (s : Finset I) (a : I) (s : Finset I) (has : a ∉ s)
    (e' : (∏ i ∈ s, (1 - e i)) * x = x), (∏ i ∈ insert a s, (1 - e i)) * x = x
⊢ Function.Bijective (α := 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})
have refine₇ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x) (s : Finset I) (a : I) (s : Finset I) (has : a ∉ s)
  (e' : (∏ i ∈ s, (1 - e i)) * x = x), (1 - e a) * x = x
Tactic: classical
  refine ⟨?_, he.1.surjective_pi⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  simp only [funext_iff, Pi.ringHom_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx
  suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
  refine fun s ↦ Finset.induction_on s (by simp) ?_
  intro a s has e'
  suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
  obtain ⟨c, rfl⟩ := hx a
  rw [← mul_assoc, (he.idem a).one_sub.eq]