-- Mathlib/Algebra/Central/TensorProduct.lean
lemma Algebra.TensorProduct.includeRight_map_center_le :
    (Subalgebra.center K C).map includeRight ≤ Subalgebra.center K (B ⊗[K] C) := fun x hx ↦ by
  simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢
  obtain ⟨c, hc0, rfl⟩ := hx
  intro bc
  induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b c' => simp [hc0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]

Proof state:
case intro.intro.add
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
x✝ y✝ : B ⊗[K] C
a✝¹ : x✝ * includeRight c = includeRight c * x✝
a✝ : y✝ * includeRight c = includeRight c * y✝
⊢ (x✝ + y✝) * includeRight c = includeRight c * (x✝ + y✝)

Tactic:
simp_all [add_mul, mul_add]

Result:
no goals

Proof state:
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
x : B ⊗[K] C
hx : x ∈ Subalgebra.map includeRight (Subalgebra.center K C)
⊢ x ∈ Subalgebra.center K (B ⊗[K] C)

Tactic:
simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢

Result:
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
x : B ⊗[K] C
hx : ∃ x_1, (∀ (b : C), b * x_1 = x_1 * b) ∧ includeRight x_1 = x
⊢ ∀ (b : B ⊗[K] C), b * x = x * b

Proof state:
case intro.intro.zero
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
⊢ 0 * includeRight c = includeRight c * 0

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
bc : B ⊗[K] C
⊢ bc * includeRight c = includeRight c * bc

Tactic:
induction bc using TensorProduct.induction_on with
| zero => simp
| tmul b c' => simp [hc0]
| add _ _ _ _ => simp_all [add_mul, mul_add]

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
⊢ ∀ (b : B ⊗[K] C), b * includeRight c = includeRight c * b

Tactic:
intro bc

Result:
case intro.intro
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
bc : B ⊗[K] C
⊢ bc * includeRight c = includeRight c * bc

Proof state:
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
x : B ⊗[K] C
hx : ∃ x_1, (∀ (b : C), b * x_1 = x_1 * b) ∧ includeRight x_1 = x
⊢ ∀ (b : B ⊗[K] C), b * x = x * b

Tactic:
obtain ⟨c, hc0, rfl⟩ := hx

Result:
case intro.intro
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
⊢ ∀ (b : B ⊗[K] C), b * includeRight c = includeRight c * b

Proof state:
case intro.intro.tmul
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
b : B
c' : C
⊢ b ⊗ₜ[K] c' * includeRight c = includeRight c * b ⊗ₜ[K] c'

Tactic:
simp [hc0]

Result:
no goals