Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁶ : Semiring R
inst✝³⁵ : Semiring R₂
inst✝³⁴ : Semiring R₃
inst✝³³ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³² : RingHomInvPair σ₁₂ σ₂₁
inst✝³¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁰ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁹ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁸ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁷ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁶ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁵ : RingHomInvPair σ₄₁ σ₁₄
inst✝²⁴ : RingHomInvPair σ₂₄ σ₄₂
inst✝²³ : RingHomInvPair σ₄₂ σ₂₄
inst✝²² : RingHomInvPair σ₃₄ σ₄₃
inst✝²¹ : RingHomInvPair σ₄₃ σ₃₄
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁵ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹⁴ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup E₂
inst✝¹⁰ : SeminormedAddCommGroup E₃
inst✝⁹ : SeminormedAddCommGroup E₄
inst✝⁸ : Module R E
inst✝⁷ : Module R₂ E₂
inst✝⁶ : Module R₃ E₃
inst✝⁵ : Module R₄ E₄
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝² : TopologicalSpace α
inst✝¹ : Module R E₂
inst✝ : Module R E₃
⊢ ∀ (x : (E × E₂) × E₃), ‖(LinearEquiv.prodAssoc R E E₂ E₃) x‖ = ‖x‖

Tactic:
rintro ⟨⟨e, f⟩, g⟩

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁶ : Semiring R
inst✝³⁵ : Semiring R₂
inst✝³⁴ : Semiring R₃
inst✝³³ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³² : RingHomInvPair σ₁₂ σ₂₁
inst✝³¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁰ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁹ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁸ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁷ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁶ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁵ : RingHomInvPair σ₄₁ σ₁₄
inst✝²⁴ : RingHomInvPair σ₂₄ σ₄₂
inst✝²³ : RingHomInvPair σ₄₂ σ₂₄
inst✝²² : RingHomInvPair σ₃₄ σ₄₃
inst✝²¹ : RingHomInvPair σ₄₃ σ₃₄
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁵ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹⁴ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup E₂
inst✝¹⁰ : SeminormedAddCommGroup E₃
inst✝⁹ : SeminormedAddCommGroup E₄
inst✝⁸ : Module R E
inst✝⁷ : Module R₂ E₂
inst✝⁶ : Module R₃ E₃
inst✝⁵ : Module R₄ E₄
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module R F
e✝ : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝² : TopologicalSpace α
inst✝¹ : Module R E₂
inst✝ : Module R E₃
g : E₃
e : E
f : E₂
⊢ ‖(LinearEquiv.prodAssoc R E E₂ E₃) ((e, f), g)‖ = ‖((e, f), g)‖