-- Mathlib/RingTheory/TensorProduct/Pi.lean
@[simp]
lemma piRightHom_mul (x y : A ⊗[R] ∀ i, B i) :
    piRightHom R S A B (x * y) = piRightHom R S A B x * piRightHom R S A B y

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x y : A ⊗[R] ((i : ι) → B i)
⊢ (piRightHom R S A B) (x * y) = (piRightHom R S A B) x * (piRightHom R S A B) y

Tactic:
induction x

Result:
case zero
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y : A ⊗[R] ((i : ι) → B i)
⊢ (piRightHom R S A B) (0 * y) = (piRightHom R S A B) 0 * (piRightHom R S A B) y

case tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y : A ⊗[R] ((i : ι) → B i)
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝ * y) = (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝) * (piRightHom R S A B) y

case add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝ * y) = (piRightHom R S A B) x✝ * (piRightHom R S A B) y
a✝ : (piRightHom R S A B) (y✝ * y) = (piRightHom R S A B) y✝ * (piRightHom R S A B) y
⊢ (piRightHom R S A B) ((x✝ + y✝) * y) = (piRightHom R S A B) (x✝ + y✝) * (piRightHom R S A B) y

Proof state:
case tmul.zero
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝ * 0) = (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝) * (piRightHom R S A B) 0

Tactic:
simp

Result:
no goals

Proof state:
case tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)

Tactic:
ext j

Result:
case tmul.tmul.h
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
j : ι
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) j =
    ((piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)) j

Proof state:
case tmul.add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) x✝
a✝ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * y✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) y✝
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * (x✝ + y✝)) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ + y✝)

Tactic:
simp_all [mul_add]

Result:
no goals

Proof state:
case tmul.tmul.h
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
j : ι
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) j =
    ((piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)) j

Tactic:
simp

Result:
no goals

Proof state:
case add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝ * y) = (piRightHom R S A B) x✝ * (piRightHom R S A B) y
a✝ : (piRightHom R S A B) (y✝ * y) = (piRightHom R S A B) y✝ * (piRightHom R S A B) y
⊢ (piRightHom R S A B) ((x✝ + y✝) * y) = (piRightHom R S A B) (x✝ + y✝) * (piRightHom R S A B) y

Tactic:
simp_all [add_mul]

Result:
no goals

Proof state:
case zero
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y : A ⊗[R] ((i : ι) → B i)
⊢ (piRightHom R S A B) (0 * y) = (piRightHom R S A B) 0 * (piRightHom R S A B) y

Tactic:
simp

Result:
no goals