-- Mathlib/Algebra/Ring/CentroidHom.lean
lemma centroid_eq_centralizer_mulLeftRight :
    RingHom.rangeS (toEndRingHom α) = Subsemiring.centralizer (Set.range L ∪ Set.range R)

Proof state:
case h.refine_1.intro.inl.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
a : α
⊢ L a * (toEndRingHom α) f = (toEndRingHom α) f * L a

Tactic:
exact AddMonoidHom.ext fun b ↦ (map_mul_left f a b).symm

Result:
no goals

Proof state:
case h.refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS → T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

Tactic:
rintro ⟨f, rfl⟩ S (⟨a, rfl⟩ | ⟨b, rfl⟩)

Result:
case h.refine_1.intro.inl.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
a : α
⊢ L a * (toEndRingHom α) f = (toEndRingHom α) f * L a

case h.refine_1.intro.inr.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ R b * (toEndRingHom α) f = (toEndRingHom α) f * R b

Proof state:
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ (toEndRingHom α).rangeS = Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

Tactic:
ext T

Result:
case h
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS ↔ T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

Proof state:
case h.refine_2.refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = a * (↑T).toFun b

Tactic:
exact congr($(h (L a) (.inl ⟨a, rfl⟩)) b).symm

Result:
no goals

Proof state:
case h.refine_1.intro.inr.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ R b * (toEndRingHom α) f = (toEndRingHom α) f * R b

Tactic:
exact AddMonoidHom.ext fun a ↦ (map_mul_right f a b).symm

Result:
no goals

Proof state:
case h.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)
⊢ T ∈ (toEndRingHom α).rangeS

Tactic:
rw [Subsemiring.mem_centralizer_iff] at h

Result:
case h.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
⊢ T ∈ (toEndRingHom α).rangeS

Proof state:
case h.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
⊢ T ∈ (toEndRingHom α).rangeS

Tactic:
refine ⟨⟨T, fun a b ↦ ?_, fun a b ↦ ?_⟩, rfl⟩

Result:
case h.refine_2.refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = a * (↑T).toFun b

case h.refine_2.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = (↑T).toFun a * b

Proof state:
case h.refine_2.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = (↑T).toFun a * b

Tactic:
exact congr($(h (R b) (.inr ⟨b, rfl⟩)) a).symm

Result:
no goals

Proof state:
case h
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS ↔ T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Result:
case h.refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS → T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

case h.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)
⊢ T ∈ (toEndRingHom α).rangeS