Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL (ForML/ContinuousMultilinearMap.lean)

State before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
⊢ Continuous fun f => compContinuousLinearMapL f
Tactic:
have e := Fintype.equivFin ι
State after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun f => compContinuousLinearMapL f

State before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun f => compContinuousLinearMapL f
Tactic:
rw [continuous_congr (compContinuousLinearMapL_domDomCongr G e)]
State after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun x =>
    ContinuousLinearMap.comp
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 (fun i => E i) G e))))
      (ContinuousLinearMap.comp
        (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) x))
        ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 (fun i => E₁ i) G e)))

State before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun x =>
    ContinuousLinearMap.comp
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 (fun i => E i) G e))))
      (ContinuousLinearMap.comp
        (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) x))
        ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 (fun i => E₁ i) G e)))
Tactic:
refine .clm_comp continuous_const (.clm_comp ?_ continuous_const)
State after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun x => compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) x)

State before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun x => compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) x)
Tactic:
exact .comp (continuous_compContinuousLinearMapL_fin G) (LinearIsometryEquiv.continuous _)
State after:
no goals