-- 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₂) = ((coordChangeL 𝕜 e₁ e₁' b) v₁, (coordChangeL 𝕜 e₂ e₂' b) v₂)

Tactic:
rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']

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₂
⊢ (↑(e₁'.prod e₂') (↑(e₁.prod e₂).symm (b, v₁, v₂))).2 =
    ((↑e₁' { proj := b, snd := e₁.symm b v₁ }).2, (↑e₂' { proj := b, snd := e₂.symm b v₂ }).2)

case mk.hb
𝕜 : 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₂
⊢ b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet

case mk.hb
𝕜 : 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₂
⊢ b ∈ e₂.baseSet ∩ e₂'.baseSet

case mk.hb
𝕜 : 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₂
⊢ b ∈ e₁.baseSet ∩ e₁'.baseSet