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 : 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
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
⊢ 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₈ : ∀ (s : 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
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.{u_1, u_3} (R := R) fun (x : I) ↦ 1 - e x
⊢ Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {e i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {e i})
have obtain : ∀ (e' : I → R)
  (h :
    Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i}))
      (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i})) fun (i : I) ↦
            Ideal.Quotient.mk (Ideal.span {e' i})) :
        (a : R) → (i : I) → R ⧸ Ideal.span {e' i}))
  (he : CompleteOrthogonalIdempotents.{u_1, u_3} (R := R) fun (x : I) ↦ 1 - e' x),
  Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {e' i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {e' i})
Tactic: obtain ⟨e', rfl, h⟩ : ∃ e' : I → R, (e' = e) ∧ Function.Bijective (Pi.ringHom fun i ↦
      Ideal.Quotient.mk (Ideal.span {e' i})) := ⟨_, funext (by simp), he.bijective_pi⟩
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
⊢ Function.Bijective (α := R) (β :=
    HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e}) × HasQuotient.Quotient R (B := Ideal R) (Ideal.span {f}))
    (⇑(RingHom.prod (Ideal.Quotient.mk (Ideal.span {e})) (Ideal.Quotient.mk (Ideal.span {f}))) :
      (a : R) → (R ⧸ Ideal.span {e}) × R ⧸ Ideal.span {f})
have change : Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
  HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o 0}) × HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o 1}))
  (Function.comp (β := (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
    (⇑(piFinTwoEquiv fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) :
      (a : (i : Fin 2) → R ⧸ Ideal.span {o i}) → (R ⧸ Ideal.span {o 0}) × R ⧸ Ideal.span {o 1})
    (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
          Ideal.Quotient.mk (Ideal.span {o i})) :
      (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i}))
Tactic: change Function.Bijective
    (piFinTwoEquiv _ ∘ Pi.ringHom (fun i : Fin 2 ↦ Ideal.Quotient.mk (Ideal.span {o i})))
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
    HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o 0}) × HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o 1}))
    (Function.comp (β := (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
      (⇑(piFinTwoEquiv fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) :
        (a : (i : Fin 2) → R ⧸ Ideal.span {o i}) → (R ⧸ Ideal.span {o 0}) × R ⧸ Ideal.span {o 1})
      (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
            Ideal.Quotient.mk (Ideal.span {o i})) :
        (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i}))
have rw : Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
  (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
  (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
        Ideal.Quotient.mk (Ideal.span {o i})) :
    (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i})
Tactic: rw [(Equiv.bijective _).of_comp_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
    (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
    (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
          Ideal.Quotient.mk (Ideal.span {o i})) :
      (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i})
have he₁ : ∀ (i : Fin 2), IsIdempotentElem (o i)
Tactic: apply pi_bijective_of_isIdempotentElem
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
he₁ : ∀ (i : Fin 2), IsIdempotentElem (o i)
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
    (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
    (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
          Ideal.Quotient.mk (Ideal.span {o i})) :
      (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i})
have he₂ : ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0
Tactic: apply pi_bijective_of_isIdempotentElem
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
he₁ : ∀ (i : Fin 2), IsIdempotentElem (o i)
he₂ : ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
    (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
    (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
          Ideal.Quotient.mk (Ideal.span {o i})) :
      (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i})
have he₃ : Eq.{u_1 + 1} (α := R) (∏ i : Fin 2, o i) 0
Tactic: apply pi_bijective_of_isIdempotentElem
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
i j : Fin 2
hij : i ≠ j
⊢ (1 - o i) * (1 - o j) = 0
have he₁ : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨0, sorry⟩ ≠ j), (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))) * (1 - o j) = 0
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
i j : Fin 2
hij : i ≠ j
he₁ : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j), (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o j) = 0
⊢ (1 - o i) * (1 - o j) = 0
have he₂ : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨1, sorry⟩ ≠ j), (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))) * (1 - o j) = 0
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o j) = 0
have he₁ : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))) = 0
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
he₁ :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) = 0
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o j) = 0
have he₂ : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))) = 0
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o j) = 0
have he₁ : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))) = 0
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
he₁ :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) = 0
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o j) = 0
have he₂ : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))) = 0
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) = 0
have he₁ : ∀ (hij : True), (1 - o 0) * (1 - o 1) = 0
Tactic: simp at hij ⊢
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) = 0
have he₁ : ∀ (hij : True), (1 - o 1) * (1 - o 0) = 0
Tactic: simp at hij ⊢
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
r : R
simp_rw simp_rw₁ : e * (e * r * e) = e * r * e ∧ e * r * e * e = e * r * e
⊢ e * (fun (x : R) ↦ e * x * e) r = (fun (x : R) ↦ e * x * e) r ∧
    (fun (x : R) ↦ e * x * e) r * e = (fun (x : R) ↦ e * x * e) r
have simp_rw₂ : e * e * r * e = e * r * e ∧ e * r * e * e = e * r * e
Tactic: simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
r : R
simp_rw simp_rw₁ : e * (e * r * e) = e * r * e ∧ e * r * e * e = e * r * e
simp_rw₂ : e * e * r * e = e * r * e ∧ e * r * e * e = e * r * e
⊢ e * (fun (x : R) ↦ e * x * e) r = (fun (x : R) ↦ e * x * e) r ∧
    (fun (x : R) ↦ e * x * e) r * e = (fun (x : R) ↦ e * x * e) r
have simp_rw₃ : True ∧ e * r * e * e = e * r * e
Tactic: simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
r : R
simp_rw simp_rw₁ : e * (e * r * e) = e * r * e ∧ e * r * e * e = e * r * e
simp_rw₂ : e * e * r * e = e * r * e ∧ e * r * e * e = e * r * e
simp_rw₃ : True ∧ e * r * e * e = e * r * e
⊢ e * (fun (x : R) ↦ e * x * e) r = (fun (x : R) ↦ e * x * e) r ∧
    (fun (x : R) ↦ e * x * e) r * e = (fun (x : R) ↦ e * x * e) r
have simp_rw₄ : True ∧ e * (r * (e * e)) = e * (r * e)
Tactic: simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
r : R
simp_rw simp_rw₁ : e * (e * r * e) = e * r * e ∧ e * r * e * e = e * r * e
simp_rw₂ : e * e * r * e = e * r * e ∧ e * r * e * e = e * r * e
simp_rw₃ : True ∧ e * r * e * e = e * r * e
simp_rw₄ : True ∧ e * (r * (e * e)) = e * (r * e)
⊢ e * (fun (x : R) ↦ e * x * e) r = (fun (x : R) ↦ e * x * e) r ∧
    (fun (x : R) ↦ e * x * e) r * e = (fun (x : R) ↦ e * x * e) r
have simp_rw₅ : True ∧ True
Tactic: simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ e * r = r
have rw : e * r = r → r * e = r
Tactic: rw [mem_corner_iff idem, and_iff_left_of_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ r * e = r
have rw : e * r = r ↔ r * e = r
Tactic: rw [mem_corner_iff_mul_left idem hc, hc.comm]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
rw : e * r = r ↔ r * e = r
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ r * e = r
have rw₁ : r * e = r ↔ r * e = r
Tactic: rw [mem_corner_iff_mul_left idem hc, hc.comm]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
have simp_rw : Membership.mem (γ := Subsemigroup R) { carrier := Set.range fun (x : R) ↦ e * x * e, mul_mem' := sorry } r ↔
  Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
Tactic: simp_rw [corner, mem_mk, Set.mem_range, ← (hc.comm _).eq, ← mul_assoc, idem.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
simp_rw :
  Membership.mem (γ := Subsemigroup R) { carrier := Set.range fun (x : R) ↦ e * x * e, mul_mem' := ⋯ } r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
have simp_rw₁ : Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x * e) r ↔
  Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
Tactic: simp_rw [corner, mem_mk, Set.mem_range, ← (hc.comm _).eq, ← mul_assoc, idem.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
simp_rw :
  Membership.mem (γ := Subsemigroup R) { carrier := Set.range fun (x : R) ↦ e * x * e, mul_mem' := ⋯ } r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
simp_rw₁ :
  Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x * e) r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
have simp_rw₂ : (∃ (y : R), e * y * e = r) ↔ ∃ (y : R), e * y = r
Tactic: simp_rw [corner, mem_mk, Set.mem_range, ← (hc.comm _).eq, ← mul_assoc, idem.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
simp_rw :
  Membership.mem (γ := Subsemigroup R) { carrier := Set.range fun (x : R) ↦ e * x * e, mul_mem' := ⋯ } r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
simp_rw₁ :
  Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x * e) r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
simp_rw₂ : (∃ (y : R), e * y * e = r) ↔ ∃ (y : R), e * y = r
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
have simp_rw₃ : (∃ (y : R), e * (e * y) = r) ↔ ∃ (y : R), e * y = r
Tactic: simp_rw [corner, mem_mk, Set.mem_range, ← (hc.comm _).eq, ← mul_assoc, idem.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
simp_rw :
  Membership.mem (γ := Subsemigroup R) { carrier := Set.range fun (x : R) ↦ e * x * e, mul_mem' := ⋯ } r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
simp_rw₁ :
  Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x * e) r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
simp_rw₂ : (∃ (y : R), e * y * e = r) ↔ ∃ (y : R), e * y = r
simp_rw₃ : (∃ (y : R), e * (e * y) = r) ↔ ∃ (y : R), e * y = r
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
have simp_rw₄ : (∃ (y : R), e * e * y = r) ↔ ∃ (y : R), e * y = r
Tactic: simp_rw [corner, mem_mk, Set.mem_range, ← (hc.comm _).eq, ← mul_assoc, idem.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ x * e) r
have simp_rw : Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r ↔
  Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ x * e) r
Tactic: simp_rw [mem_corner_iff_mem_range_mul_left idem hc, (hc.comm _).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : NonUnitalSemiring R
a b : R
simp_rw simp_rw₁ : e * (a + b) * e = e * a * e + e * b * e
⊢ (fun (x : R) ↦ e * x * e) (a + b) = HAdd.hAdd (α := R) ((fun (x : R) ↦ e * x * e) a) ((fun (x : R) ↦ e * x * e) b)
have simp_rw₂ : (e * a + e * b) * e = e * a * e + e * b * e
Tactic: simp_rw [mul_add, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : NonUnitalSemiring R
simp_rw simp_rw₁ : e * 0 * e = 0
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ e * x * e) 0) 0
have simp_rw₂ : 0 * e = 0
Tactic: simp_rw [mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e : R
inst : NonUnitalRing R
a : R
simp_rw simp_rw₁ : e * -a * e = -(e * a * e)
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ e * x * e) (-a)) (-(fun (x : R) ↦ e * x * e) a)
have simp_rw₂ : -(e * a) * e = -(e * a * e)
Tactic: simp_rw [mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
⊢ (fun (r : (i : I) → ⋯.Corner) ↦ (∑ i : I, (↑(r i) : R) : R))
      ((fun (r : R) (i : I) ↦
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subsemigroup R) (Subsemigroup.corner (e i)) x)
            ((fun (x : R) ↦ e i * x * e i) r) ⋯)
        r) =
    r
have simp_rw : ∑ x : I, e x * r * e x = r
Tactic: simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]