-- Mathlib/Topology/VectorBundle/Constructions.lean
theorem coordChangeL_prod [e₁.IsLinear 𝕜] [e₁'.IsLinear 𝕜] [e₂.IsLinear 𝕜] [e₂'.IsLinear 𝕜] ⦃b⦄
    (hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet) :
    ((e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b : F₁ × F₂ →L[𝕜] F₁ × F₂) =
      (e₁.coordChangeL 𝕜 e₁' b : F₁ →L[𝕜] F₁).prodMap (e₂.coordChangeL 𝕜 e₂' b)

Proof state:
case mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet
v₁ : F₁
v₂ : F₂
⊢ ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) (v₁, v₂) =
    Prod.map ⇑↑(coordChangeL 𝕜 e₁ e₁' b) ⇑↑(coordChangeL 𝕜 e₂ e₂' b) (v₁, v₂)

Tactic:
show
  (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) =
    (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)

Result:
case mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet
v₁ : F₁
v₂ : F₂
⊢ (coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) (v₁, v₂) = ((coordChangeL 𝕜 e₁ e₁' b) v₁, (coordChangeL 𝕜 e₂ e₂' b) v₂)

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet
⊢ ∀ (x : F₁ × F₂),
    ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) x =
      Prod.map (⇑↑(coordChangeL 𝕜 e₁ e₁' b)) (⇑↑(coordChangeL 𝕜 e₂ e₂' b)) x

Tactic:
rintro ⟨v₁, v₂⟩

Result:
case mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet
v₁ : F₁
v₂ : F₂
⊢ ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) (v₁, v₂) =
    Prod.map ⇑↑(coordChangeL 𝕜 e₁ e₁' b) ⇑↑(coordChangeL 𝕜 e₂ e₂' b) (v₁, v₂)

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet
⊢ ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) = (↑(coordChangeL 𝕜 e₁ e₁' b)).prodMap ↑(coordChangeL 𝕜 e₂ e₂' b)

Tactic:
rw [ContinuousLinearMap.ext_iff, ContinuousLinearMap.coe_prodMap']

Result:
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet
⊢ ∀ (x : F₁ × F₂),
    ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) x =
      Prod.map (⇑↑(coordChangeL 𝕜 e₁ e₁' b)) (⇑↑(coordChangeL 𝕜 e₂ e₂' b)) x