awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
rw :
  Eq (α := α) ((T : (a : α) → α) (HMul.hMul (α := α) ((S : (a : α) → α) a : α) b) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
rw₁ :
  HMul.hMul (α := α) (β := α) ((S : (a : α) → α) a : α) ((T : (a : α) → α) b : α) =
    (S : (a : α) → α) ((T : (a : α) → α) (a * b) : α)
rw₂ :
  Eq (α := α) ((S : (a : α) → α) (HMul.hMul (β := α) a ((T : (a : α) → α) b : α)) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
⊢ Eq (α := α) ((T : (a : α) → α) ((S : (a : α) → α) (a * b) : α) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
have rw₃ : Eq (α := α) ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
  ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
Tactic: rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
⊢ Eq (α := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
    (Subsemiring.centralizer
      (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
have h : ∀ (T : AddMonoid.End α),
  Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T ↔
    Membership.mem (γ := Subsemiring (AddMonoid.End α))
      (Subsemiring.centralizer
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
      T
Tactic: ext T
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T ↔
    Membership.mem (γ := Subsemiring (AddMonoid.End α))
      (Subsemiring.centralizer
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
      T
have h : Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T →
  Membership.mem (γ := Subsemiring (AddMonoid.End α))
    (Subsemiring.centralizer
      (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
    T
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T →
    Membership.mem (γ := Subsemiring (AddMonoid.End α))
      (Subsemiring.centralizer
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
      T
⊢ Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T ↔
    Membership.mem (γ := Subsemiring (AddMonoid.End α))
      (Subsemiring.centralizer
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
      T
have h₁ : ∀
  (h :
    Membership.mem (γ := Subsemiring (AddMonoid.End α))
      (Subsemiring.centralizer
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
      T),
  Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (hypothesis)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  Membership.mem (γ := Subsemiring (AddMonoid.End α))
    (Subsemiring.centralizer
      (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
    T
⊢ Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T
have h₁ : ∀ (g : AddMonoid.End α),
  Membership.mem (γ := Set (AddMonoid.End α))
      (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
    g * T = T * g
Tactic: rw [Subsemiring.mem_centralizer_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  ∀ (g : AddMonoid.End α),
    Membership.mem (γ := Set (AddMonoid.End α))
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
      g * T = T * g
⊢ Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T
have h₁ : ∀ (a b : α), (↑T : ZeroHom α α).toFun (a * b) = a * (↑T : ZeroHom α α).toFun b
Tactic: refine ⟨⟨T, fun a b ↦ ?_, fun a b ↦ ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  ∀ (g : AddMonoid.End α),
    Membership.mem (γ := Set (AddMonoid.End α))
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
      g * T = T * g
h₁ : ∀ (a b : α), (↑T : ZeroHom α α).toFun (a * b) = a * (↑T : ZeroHom α α).toFun b
⊢ Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T
have h₂ : ∀ (a b : α), (↑T : ZeroHom α α).toFun (a * b) = (↑T : ZeroHom α α).toFun a * b
Tactic: refine ⟨⟨T, fun a b ↦ ?_, fun a b ↦ ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
⊢ Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α))
    { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ }
have rw : ∀ (g : CentroidHom α),
  g *
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := sorry, map_mul_right' := sorry :
        CentroidHom α } =
    { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := sorry, map_mul_right' := sorry } * g
Tactic: rw [Subsemiring.mem_center_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
g : CentroidHom α
⊢ g *
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
        CentroidHom α } =
    { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ } * g
have h : ∀ (a : α),
  Eq (α := α)
    ((g *
            { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := sorry, map_mul_right' := sorry :
              CentroidHom α } :
          (a : α) → α)
        a :
      α)
    (({ toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := sorry, map_mul_right' := sorry :
              CentroidHom α } *
            g :
          (a : α) → α)
        a :
      α)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
⊢ Eq.{u_5 + 1} (α := ↥(Subsemiring.center (CentroidHom α)))
    (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑0 : α);
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑0 : α), map_mul_left' := ⋯, map_mul_right' := ⋯ } ⋯)
    0
have simp : Eq.{u_5 + 1} (α := ↥(Subsemiring.center (CentroidHom α)))
  (Subtype.mk (p := fun (x : CentroidHom α) ↦
    Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
    { toAddMonoidHom := 0, map_mul_left' := sorry, map_mul_right' := sorry } sorry)
  0
Tactic: simp only [ZeroMemClass.coe_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
x x_1 : ↥(NonUnitalSubsemiring.center α)
⊢ (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑(x + x_1) : α);
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑(x + x_1) : α), map_mul_left' := ⋯, map_mul_right' := ⋯ }
      ⋯) =
    HAdd.hAdd (α := ↥(Subsemiring.center (CentroidHom α)))
      (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑x : α);
      Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
          CentroidHom α }
        ⋯)
      (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑x_1 : α);
      Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x_1 : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
          CentroidHom α }
        ⋯)
have dsimp : Subtype.mk (p := fun (x : CentroidHom α) ↦
    Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
    { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) ((↑x : α) + (↑x_1 : α)), map_mul_left' := sorry,
      map_mul_right' := sorry : CentroidHom α }
    sorry =
  Subtype.mk (p := fun (x : CentroidHom α) ↦
    Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
    (HAdd.hAdd (α := CentroidHom α)
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x : α), map_mul_left' := sorry, map_mul_right' := sorry }
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x_1 : α), map_mul_left' := sorry, map_mul_right' := sorry })
    sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
x x_1 : ↥(NonUnitalSubsemiring.center α)
⊢ Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) ((↑x : α) + (↑x_1 : α)), map_mul_left' := ⋯,
        map_mul_right' := ⋯ : CentroidHom α }
      ⋯ =
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      (HAdd.hAdd (α := CentroidHom α)
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x : α), map_mul_left' := ⋯, map_mul_right' := ⋯ }
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x_1 : α), map_mul_left' := ⋯, map_mul_right' := ⋯ })
      ⋯
have simp : Subtype.mk (p := fun (x : CentroidHom α) ↦
    Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
    {
      toAddMonoidHom :=
        HAdd.hAdd (α := AddMonoid.End α) (β := AddMonoid.End α)
          ((L : (a : α) → AddMonoid.End α) (↑x : α) : AddMonoid.End α)
          ((L : (a : α) → AddMonoid.End α) (↑x_1 : α) : AddMonoid.End α),
      map_mul_left' := sorry, map_mul_right' := sorry : CentroidHom α }
    sorry =
  Subtype.mk (p := fun (x : CentroidHom α) ↦
    Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
    (HAdd.hAdd (α := CentroidHom α)
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x : α), map_mul_left' := sorry, map_mul_right' := sorry }
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x_1 : α), map_mul_left' := sorry, map_mul_right' := sorry })
    sorry
Tactic: simp only [map_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
f g : ↥(Subsemiring.center (CentroidHom α))
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun) f)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun) g)
⊢ f = g
have mk : ∀ (val : CentroidHom α)
  (property : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val)
  (h :
    Eq.{u_5 + 1} (α := (a : α) → α)
      ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
        (Subtype.mk (p := fun (x : CentroidHom α) ↦
          Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
      ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
        g)),
  Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property =
    g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
g : ↥(Subsemiring.center (CentroidHom α))
val : CentroidHom α
property : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun) g)
⊢ Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property =
    g
have mk : ∀ (val_1 : CentroidHom α)
  (property_1 : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val_1)
  (h :
    Eq.{u_5 + 1} (α := (a : α) → α)
      ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
        (Subtype.mk (p := fun (x : CentroidHom α) ↦
          Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
      ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
        (Subtype.mk (p := fun (x : CentroidHom α) ↦
          Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1 property_1))),
  Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property =
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1 property_1
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
val : CentroidHom α
property : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val
val_1 : CentroidHom α
property_1 : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val_1
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1 property_1))
⊢ Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property =
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1 property_1
have mk : ∀ (x : α), Eq (α := α) ((val : (a : α) → α) x : α) ((val_1 : (a : α) → α) x : α)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a ↔
    Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
have mp : Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a →
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
      ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
    Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
      ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
mp :
  Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a →
    Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a ↔
    Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
have mpr : Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
      ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
    Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
      ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) →
  Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (hypothesis)
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 α)
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a
have e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
Tactic: have e1 (d : α) : T d = a * d := congr($hT d)
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (hypothesis)
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
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a
have e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
Tactic: have e2 (d : α) : T d = d * a := congr($(hT.trans hc.symm) d)