-- Mathlib/Algebra/Central/TensorProduct.lean
lemma Algebra.TensorProduct.includeLeft_map_center_le :
    (Subalgebra.center K B).map includeLeft ≤ Subalgebra.center K (B ⊗[K] C)

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
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
x✝ y✝ : B ⊗[K] C
a✝¹ : x✝ * includeLeft b = includeLeft b * x✝
a✝ : y✝ * includeLeft b = includeLeft b * y✝
⊢ (x✝ + y✝) * includeLeft b = includeLeft b * (x✝ + y✝)

Tactic:
simp_all [add_mul, mul_add]

Result:
no goals

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
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
⊢ 0 * includeLeft b = includeLeft b * 0

Tactic:
simp

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 includeLeft (Subalgebra.center K B)
⊢ 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 : B), b * x_1 = x_1 * b) ∧ includeLeft x_1 = x
⊢ ∀ (b : B ⊗[K] C), b * x = x * b

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
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
⊢ ∀ (b_1 : B ⊗[K] C), b_1 * includeLeft b = includeLeft b * b_1

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
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
bc : B ⊗[K] C
⊢ bc * includeLeft b = includeLeft b * bc

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
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
bc : B ⊗[K] C
⊢ bc * includeLeft b = includeLeft b * bc

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

Result:
no goals

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
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
b' : B
c : C
⊢ b' ⊗ₜ[K] c * includeLeft b = includeLeft b * b' ⊗ₜ[K] c

Tactic:
simp [hb0]

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
⊢ Subalgebra.map includeLeft (Subalgebra.center K B) ≤ Subalgebra.center K (B ⊗[K] C)

Tactic:
intro x 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 ∈ Subalgebra.map includeLeft (Subalgebra.center K B)
⊢ x ∈ Subalgebra.center K (B ⊗[K] C)

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 : B), b * x_1 = x_1 * b) ∧ includeLeft x_1 = x
⊢ ∀ (b : B ⊗[K] C), b * x = x * b

Tactic:
obtain ⟨b, hb0, 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
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
⊢ ∀ (b_1 : B ⊗[K] C), b_1 * includeLeft b = includeLeft b * b_1