awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a
have constructor : ∀ (a_1 : α), Commute a a_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
constructor : ∀ (a_1 : α), Commute a a_1
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a
have constructor₁ : ∀ (b c : α), a * (b * c) = a * b * c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
constructor : ∀ (a_1 : α), Commute a a_1
constructor₁ : ∀ (b c : α), a * (b * c) = a * b * c
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a
have constructor₂ : ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocCommSemiring α
a : α
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a ↔
    ∀ (b : α),
      Commute (S := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) b : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
have rw : (Eq (α := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
      ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
    ∀ (g : AddMonoid.End α),
      Membership.mem (γ := Set (AddMonoid.End α)) (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α)) g →
        HMul.hMul (β := AddMonoid.End α) g ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) =
          HMul.hMul (α := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) g) ↔
  ∀ (b : α),
    Commute (S := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) b : AddMonoid.End α)
      ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
Tactic: rw [NonUnitalNonAssocSemiring.mem_center_iff, CentroidHom.centroid_eq_centralizer_mulLeftRight,
    Subsemiring.mem_centralizer_iff, AddMonoid.End.mulRight_eq_mulLeft, Set.union_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonAssocSemiring α
T : CentroidHom α
⊢ Membership.mem (α := α) (γ := Subsemiring α) (Subsemiring.center α) ((T : (a : α) → α) 1 : α)
have comm : ∀ (a : α), Commute ((T : (a : α) → α) 1) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonAssocSemiring α
T : CentroidHom α
comm : ∀ (a : α), Commute ((T : (a : α) → α) 1) a
⊢ Membership.mem (α := α) (γ := Subsemiring α) (Subsemiring.center α) ((T : (a : α) → α) 1 : α)
have left_assoc : ∀ (b c : α), HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) (b * c) = HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) b * c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonAssocSemiring α
T : CentroidHom α
comm : ∀ (a : α), Commute ((T : (a : α) → α) 1) a
left_assoc :
  ∀ (b c : α), HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) (b * c) = HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) b * c
⊢ Membership.mem (α := α) (γ := Subsemiring α) (Subsemiring.center α) ((T : (a : α) → α) 1 : α)
have right_assoc : ∀ (a b : α), HMul.hMul (β := α) (a * b) ((T : (a : α) → α) 1 : α) = a * HMul.hMul (β := α) b ((T : (a : α) → α) 1 : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonAssocSemiring α
T : CentroidHom α
x : α
⊢ Eq (α := α)
    ((MulHom.toFun (NonUnitalRingHom.toMulHom centerToCentroid)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
have rw : Eq (α := α)
  (((NonUnitalRingHom.toMulHom centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
          ((fun (T : CentroidHom α) ↦
              (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                  ((T : (a : α) → α) 1) sorry :
                ↥(Subsemiring.center α)))
            T) :
        (a : α) → α)
      x :
    α)
  ((T : (a : α) → α) x : α)
Tactic: rw [MulHom.toFun_eq_coe,
      NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, ← map_mul_right, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonAssocSemiring α
T : CentroidHom α
x : α
rw :
  Eq (α := α)
    (((NonUnitalRingHom.toMulHom centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((MulHom.toFun (NonUnitalRingHom.toMulHom centerToCentroid)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
have rw₁ : Eq (α := α)
  (((centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
          ((fun (T : CentroidHom α) ↦
              (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                  ((T : (a : α) → α) 1) sorry :
                ↥(Subsemiring.center α)))
            T) :
        (a : α) → α)
      x :
    α)
  ((T : (a : α) → α) x : α)
Tactic: rw [MulHom.toFun_eq_coe,
      NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, ← map_mul_right, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonAssocSemiring α
T : CentroidHom α
x : α
rw :
  Eq (α := α)
    (((NonUnitalRingHom.toMulHom centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
rw₁ :
  Eq (α := α)
    (((centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((MulHom.toFun (NonUnitalRingHom.toMulHom centerToCentroid)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
have rw₂ : (↑((fun (T : CentroidHom α) ↦
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                ((T : (a : α) → α) 1) sorry :
              ↥(Subsemiring.center α)))
          T) :
      α) *
    x =
  (T : (a : α) → α) x
Tactic: rw [MulHom.toFun_eq_coe,
      NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, ← map_mul_right, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonAssocSemiring α
T : CentroidHom α
x : α
rw :
  Eq (α := α)
    (((NonUnitalRingHom.toMulHom centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
rw₁ :
  Eq (α := α)
    (((centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
rw₂ :
  (↑((fun (T : CentroidHom α) ↦
              (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                  ((T : (a : α) → α) 1) ⋯ :
                ↥(Subsemiring.center α)))
            T) :
        α) *
      x =
    (T : (a : α) → α) x
⊢ Eq (α := α)
    ((MulHom.toFun (NonUnitalRingHom.toMulHom centerToCentroid)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
have rw₃ : Eq (α := α) ((T : (a : α) → α) (1 * x) : α) ((T : (a : α) → α) x : α)
Tactic: rw [MulHom.toFun_eq_coe,
      NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, ← map_mul_right, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonAssocSemiring α
T : CentroidHom α
x : α
rw :
  Eq (α := α)
    (((NonUnitalRingHom.toMulHom centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
rw₁ :
  Eq (α := α)
    (((centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
rw₂ :
  (↑((fun (T : CentroidHom α) ↦
              (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                  ((T : (a : α) → α) 1) ⋯ :
                ↥(Subsemiring.center α)))
            T) :
        α) *
      x =
    (T : (a : α) → α) x
rw₃ : Eq (α := α) ((T : (a : α) → α) (1 * x) : α) ((T : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((MulHom.toFun (NonUnitalRingHom.toMulHom centerToCentroid)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
have rw₄ : Eq (α := α) ((T : (a : α) → α) x : α) ((T : (a : α) → α) x : α)
Tactic: rw [MulHom.toFun_eq_coe,
      NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, ← map_mul_right, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
⊢ f * g = g * f
have h₁ : ∀ (a : α), Eq (α := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a : α
⊢ Eq (α := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)
have h₁ : ∀ (r : α),
  HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
      HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
    0
Tactic: refine sub_eq_zero.1 (or_self_iff.1 <| (h _ _) fun r ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a r : α
⊢ HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
      HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
    0
have h₁ : HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) *
    (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
  0
Tactic: rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
        comp_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a r : α
h₁ :
  HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) *
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
⊢ HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
      HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
    0
have h₂ : HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) -
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
  0
Tactic: rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
        comp_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a r : α
h₁ :
  HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) *
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₂ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) -
      HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
⊢ HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
      HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
    0
have h₃ : HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
    (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
  HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
    (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
Tactic: rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
        comp_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a r : α
h₁ :
  HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) *
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₂ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) -
      HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₃ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
⊢ HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
      HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
    0
have h₄ : (f * g : (a : α) → α)
    (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) =
  HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
    (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
Tactic: rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
        comp_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a r : α
h₁ :
  HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) *
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₂ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) -
      HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₃ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
h₄ :
  (f * g : (a : α) → α)
      (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) =
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
⊢ HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
      HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
    0
have h₅ : Eq (α := α)
  ((f * g : (a : α) → α)
      (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) :
    α)
  ((g * f : (a : α) → α)
      (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) :
    α)
Tactic: rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
        comp_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a r : α
h₁ :
  HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) *
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₂ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) -
      HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₃ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
h₄ :
  (f * g : (a : α) → α)
      (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) =
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
h₅ :
  Eq (α := α)
    ((f * g : (a : α) → α)
        (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) :
      α)
    ((g * f : (a : α) → α)
        (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) :
      α)
⊢ HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
      HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
    0
have h₆ : Eq (α := α)
  (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α)
      (a *
        (r *
          HSub.hSub (α := α) (β := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a : α)
            ((g * f : (a : α) → α) a : α))) :
    α)
  ((g * f : (a : α) → α)
      (a *
        (r *
          HSub.hSub (α := α) (β := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a : α)
            ((g * f : (a : α) → α) a : α))) :
    α)
Tactic: rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
        comp_mul_comm]