awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_1 : (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'
refine_1₁ : (1 - e₂) * (e' * ((1 - e₂) * e')) = (1 - e₂) * e'
refine_1₂ : (1 - e₂) * (e' * (1 - e₂) * e') = (1 - e₂) * e'
refine_1₃ : (1 - e₂) * ((e' * 1 - e' * e₂) * e') = (1 - e₂) * e'
refine_1₄ : (1 - e₂) * ((e' - e' * e₂) * e') = (1 - e₂) * e'
refine_1₅ : (1 - e₂) * ((e' - 0) * e') = (1 - e₂) * e'
⊢ IsIdempotentElem ((1 - e₂) * e')
have refine_1₆ : (1 - e₂) * (e' * e') = (1 - e₂) * e'
Tactic: rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_1 : (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'
refine_1₁ : (1 - e₂) * (e' * ((1 - e₂) * e')) = (1 - e₂) * e'
refine_1₂ : (1 - e₂) * (e' * (1 - e₂) * e') = (1 - e₂) * e'
refine_1₃ : (1 - e₂) * ((e' * 1 - e' * e₂) * e') = (1 - e₂) * e'
refine_1₄ : (1 - e₂) * ((e' - e' * e₂) * e') = (1 - e₂) * e'
refine_1₅ : (1 - e₂) * ((e' - 0) * e') = (1 - e₂) * e'
refine_1₆ : (1 - e₂) * (e' * e') = (1 - e₂) * e'
⊢ IsIdempotentElem ((1 - e₂) * e')
have refine_1₇ : (1 - e₂) * e' = (1 - e₂) * e'
Tactic: rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)
have refine_2 : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (1 - e₂) : S) ((f : (a : R) → S) e' : S) = (f : (a : R) → S) e'
Tactic: rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_2 :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (1 - e₂) : S) ((f : (a : R) → S) e' : S) = (f : (a : R) → S) e'
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)
have refine_2₁ : HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) 1 : S) ((f : (a : R) → S) e₂ : S))
    ((f : (a : R) → S) e' : S) =
  (f : (a : R) → S) e'
Tactic: rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_2 :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (1 - e₂) : S) ((f : (a : R) → S) e' : S) = (f : (a : R) → S) e'
refine_2₁ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) 1 : S) ((f : (a : R) → S) e₂ : S))
      ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)
have refine_2₂ : HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) e₂ : S)) ((f : (a : R) → S) e' : S) =
  (f : (a : R) → S) e'
Tactic: rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_2 :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (1 - e₂) : S) ((f : (a : R) → S) e' : S) = (f : (a : R) → S) e'
refine_2₁ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) 1 : S) ((f : (a : R) → S) e₂ : S))
      ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₂ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) e₂ : S)) ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)
have refine_2₃ : HMul.hMul (α := S) (β := S) (1 : S) ((f : (a : R) → S) e' : S) -
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) =
  (f : (a : R) → S) e'
Tactic: rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_2 :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (1 - e₂) : S) ((f : (a : R) → S) e' : S) = (f : (a : R) → S) e'
refine_2₁ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) 1 : S) ((f : (a : R) → S) e₂ : S))
      ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₂ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) e₂ : S)) ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₃ :
  HMul.hMul (α := S) (β := S) (1 : S) ((f : (a : R) → S) e' : S) -
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)
have refine_2₄ : HSub.hSub (α := S) ((f : (a : R) → S) e' : S)
    (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S)) =
  (f : (a : R) → S) e'
Tactic: rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_2 :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (1 - e₂) : S) ((f : (a : R) → S) e' : S) = (f : (a : R) → S) e'
refine_2₁ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) 1 : S) ((f : (a : R) → S) e₂ : S))
      ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₂ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) e₂ : S)) ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₃ :
  HMul.hMul (α := S) (β := S) (1 : S) ((f : (a : R) → S) e' : S) -
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₄ :
  HSub.hSub (α := S) ((f : (a : R) → S) e' : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S)) =
    (f : (a : R) → S) e'
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)
have refine_2₅ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e' : S) (0 : S) = (f : (a : R) → S) e'
Tactic: rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_2 :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (1 - e₂) : S) ((f : (a : R) → S) e' : S) = (f : (a : R) → S) e'
refine_2₁ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) 1 : S) ((f : (a : R) → S) e₂ : S))
      ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₂ :
  HMul.hMul (β := S) (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) e₂ : S)) ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₃ :
  HMul.hMul (α := S) (β := S) (1 : S) ((f : (a : R) → S) e' : S) -
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) =
    (f : (a : R) → S) e'
refine_2₄ :
  HSub.hSub (α := S) ((f : (a : R) → S) e' : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S)) =
    (f : (a : R) → S) e'
refine_2₅ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e' : S) (0 : S) = (f : (a : R) → S) e'
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)
have refine_2₆ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e' : S)
Tactic: rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
⊢ (1 - e₂) * e' * e₂ = 0
have refine_3 : (1 - e₂) * (e' * e₂) = 0
Tactic: rw [mul_assoc, h₂, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_3 : (1 - e₂) * (e' * e₂) = 0
⊢ (1 - e₂) * e' * e₂ = 0
have refine_3₁ : (1 - e₂) * 0 = 0
Tactic: rw [mul_assoc, h₂, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_3 : (1 - e₂) * (e' * e₂) = 0
refine_3₁ : (1 - e₂) * 0 = 0
⊢ (1 - e₂) * e' * e₂ = 0
have refine_3₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [mul_assoc, h₂, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
⊢ e₂ * ((1 - e₂) * e') = 0
have refine_4 : e₂ * (1 - e₂) * e' = 0
Tactic: rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_4 : e₂ * (1 - e₂) * e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0
have refine_4₁ : (e₂ * 1 - e₂ * e₂) * e' = 0
Tactic: rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_4 : e₂ * (1 - e₂) * e' = 0
refine_4₁ : (e₂ * 1 - e₂ * e₂) * e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0
have refine_4₂ : (e₂ - e₂ * e₂) * e' = 0
Tactic: rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_4 : e₂ * (1 - e₂) * e' = 0
refine_4₁ : (e₂ * 1 - e₂ * e₂) * e' = 0
refine_4₂ : (e₂ - e₂ * e₂) * e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0
have refine_4₃ : (e₂ - e₂) * e' = 0
Tactic: rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_4 : e₂ * (1 - e₂) * e' = 0
refine_4₁ : (e₂ * 1 - e₂ * e₂) * e' = 0
refine_4₂ : (e₂ - e₂ * e₂) * e' = 0
refine_4₃ : (e₂ - e₂) * e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0
have refine_4₄ : 0 * e' = 0
Tactic: rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_4 : e₂ * (1 - e₂) * e' = 0
refine_4₁ : (e₂ * 1 - e₂ * e₂) * e' = 0
refine_4₂ : (e₂ - e₂ * e₂) * e' = 0
refine_4₃ : (e₂ - e₂) * e' = 0
refine_4₄ : 0 * e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0
have refine_4₅ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
⊢ ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have succ : ∀ (e' : Fin n → R) (h₁ : OrthogonalIdempotents e')
  (h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))),
  ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: obtain ⟨e', h₁, h₂⟩ := IH (he.embedding (Fin.succEmb n)) (fun i ↦ he' _)
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
⊢ ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
Tactic: have h₂' (i) : f (e' i) = e i.succ := congr_fun h₂ i
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S} (he : OrthogonalIdempotents e)
    (he' : ∀ (i : Fin n), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)),
    ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Fin.succEmb n) : (a : Fin n) → Fin (n + 1))
h₂' : ∀ (i : Fin n), (f : (a : R) → S) (e' i) = e i.succ
⊢ ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have succ : ∀ (e₀ : R) (h₃ : IsIdempotentElem e₀) (h₄ : (f : (a : R) → S) e₀ = e 0) (h₅ : e₀ * ∑ i : Fin n, e' i = 0)
  (h₆ : (∑ i : Fin n, e' i) * e₀ = 0), ∃ (e' : Fin (n + 1) → R), OrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: obtain ⟨e₀, h₃, h₄, h₅, h₆⟩ :=
      exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h _ (he' 0) (he.idem 0) _
      h₁.isIdempotentElem_sum
      (by simp [Finset.mul_sum, h₂', he.mul_eq, eq_comm])
      (by simp [Finset.sum_mul, h₂', he.mul_eq])