-- Mathlib/Algebra/Ring/CentroidHom.lean
lemma _root_.NonUnitalNonAssocSemiring.mem_center_iff (a : α) :
    a ∈ NonUnitalSubsemiring.center α ↔ R a = L a ∧ (L a) ∈ RingHom.rangeS (toEndRingHom α)

Proof state:
case mpr.intro.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
⊢ a ∈ NonUnitalSubsemiring.center α

Tactic:
have e2 (d : α) : T d = d * a := congr($(hT.trans hc.symm) d)

Result:
case mpr.intro.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ a ∈ NonUnitalSubsemiring.center α

Proof state:
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS

Tactic:
constructor

Result:
case mp
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α → R a = L a ∧ L a ∈ (toEndRingHom α).rangeS

case mpr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS → a ∈ NonUnitalSubsemiring.center α

Proof state:
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 c : α), a_1 * a * c = a_1 * (a * c)

Tactic:
exact fun b c ↦ by simpa [e1 c, e2 b] using
(map_mul_right T b c).symm.trans <| map_mul_left T b c

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
⊢ a ∈ NonUnitalSubsemiring.center α

Tactic:
have e1 (d : α) : T d = a * d := congr($hT d)

Result:
case mpr.intro.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
⊢ a ∈ NonUnitalSubsemiring.center α

Proof state:
case mpr.intro.intro.mid_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 c : α), a_1 * a * c = a_1 * (a * c)

case mpr.intro.intro.right_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)

Tactic:
case mid_assoc => exact fun b c ↦ by simpa [e1 c, e2 b] using
  (map_mul_right T b c).symm.trans <| map_mul_left T b c

Result:
case mpr.intro.intro.right_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)

Proof state:
case mpr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS → a ∈ NonUnitalSubsemiring.center α

Tactic:
rintro ⟨hc, ⟨T, hT⟩⟩

Result:
case mpr.intro.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
⊢ a ∈ NonUnitalSubsemiring.center α

Proof state:
case mpr.intro.intro
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ a ∈ NonUnitalSubsemiring.center α

Tactic:
constructor

Result:
case mpr.intro.intro.comm
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 : α), a * a_1 = a_1 * a

case mpr.intro.intro.left_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (b c : α), a * (b * c) = a * b * c

case mpr.intro.intro.mid_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 c : α), a_1 * a * c = a_1 * (a * c)

case mpr.intro.intro.right_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)

Proof state:
case mp
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α → R a = L a ∧ L a ∈ (toEndRingHom α).rangeS

Tactic:
exact fun ha ↦ ⟨AddMonoidHom.ext <| fun _ => (IsMulCentral.comm ha _).symm,
  ⟨centerToCentroid ⟨a, ha⟩, rfl⟩⟩

Result:
no goals

Proof state:
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
b c : α
⊢ b * a * c = b * (a * c)

Tactic:
simpa [e1 c, e2 b] using
(map_mul_right T b c).symm.trans <| map_mul_left T b c

Result:
no goals