Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hl.hl.fst
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₁
⊢ ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inl R M₁ M₂)
        x✝).1 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂) x✝).1

pp: case hl.hl.snd
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₁
⊢ ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inl R M₁ M₂)
        x✝).2 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂) x✝).2

pp: case hl.hr.fst
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₂
⊢ ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inr R M₁ M₂)
        x✝).1 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂) x✝).1

pp: case hl.hr.snd
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₂
⊢ ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inr R M₁ M₂)
        x✝).2 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂) x✝).2

pp: case hr.fst
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₃
⊢ (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).1 =
    (((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).1

pp: case hr.snd
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₃
⊢ (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).2 =
    (((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).2

Tactic:
<;>

Goal state after:
case hl.hl.fst
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₁
⊢ ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inl R M₁ M₂)
        x✝).1 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂) x✝).1

case hl.hl.snd
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₁
⊢ ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inl R M₁ M₂)
        x✝).2 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂) x✝).2

case hl.hr.fst
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₂
⊢ ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inr R M₁ M₂)
        x✝).1 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂) x✝).1

case hl.hr.snd
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₂
⊢ ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inr R M₁ M₂)
        x✝).2 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂) x✝).2

case hr.fst
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₃
⊢ (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).1 =
    (((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).1

case hr.snd
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₃
⊢ (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).2 =
    (((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).2