Theorem: ContinuousMultilinearMap.compContinuousLinearMapL_domDomCongr (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
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ compContinuousLinearMapL f =
    ContinuousLinearMap.comp
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
      (ContinuousLinearMap.comp
        (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
        ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e)))
Tactic:
ext φ x
State after:
case h.H
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((compContinuousLinearMapL f) φ) x =
    ((ContinuousLinearMap.comp
          (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
          (ContinuousLinearMap.comp
            (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
            ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e))))
        φ)
      x

State before:
case h.H
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((compContinuousLinearMapL f) φ) x =
    ((ContinuousLinearMap.comp
          (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
          (ContinuousLinearMap.comp
            (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
            ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e))))
        φ)
      x
Tactic:
suffices : (e.piCongrLeft' E₁).symm (fun i' ↦ f (e.symm i') (x (e.symm i'))) = fun i ↦ f i (x i)
State after:
case h.H
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
this : ((Equiv.piCongrLeft' E₁ e).symm fun i' => (f (e.symm i')) (x (e.symm i'))) = fun i => (f i) (x i)
⊢ ((compContinuousLinearMapL f) φ) x =
    ((ContinuousLinearMap.comp
          (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
          (ContinuousLinearMap.comp
            (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
            ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e))))
        φ)
      x

case this
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((Equiv.piCongrLeft' E₁ e).symm fun i' => (f (e.symm i')) (x (e.symm i'))) = fun i => (f i) (x i)

State before:
case this
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((Equiv.piCongrLeft' E₁ e).symm fun i' => (f (e.symm i')) (x (e.symm i'))) = fun i => (f i) (x i)
Tactic:
refine funext ?_
State after:
case this
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ∀ (x_1 : ι), (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) x_1 = (f x_1) (x x_1)

State before:
case this
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ∀ (x_1 : ι), (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) x_1 = (f x_1) (x x_1)
Tactic:
rw [Equiv.forall_congr_left' e]
State after:
case this
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ∀ (y : ι'),
    (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) (e.symm y) =
      (f (e.symm y)) (x (e.symm y))

State before:
case this
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ∀ (y : ι'),
    (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) (e.symm y) =
      (f (e.symm y)) (x (e.symm y))
Tactic:
intro i'
State after:
case this
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
i' : ι'
⊢ (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) (e.symm i') =
    (f (e.symm i')) (x (e.symm i'))

State before:
case this
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
i' : ι'
⊢ (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) (e.symm i') =
    (f (e.symm i')) (x (e.symm i'))
Tactic:
simp only [Equiv.piCongrLeft'_symm_apply_apply]
State after:
no goals

State before:
case h.H
𝕜 : 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 : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
this : ((Equiv.piCongrLeft' E₁ e).symm fun i' => (f (e.symm i')) (x (e.symm i'))) = fun i => (f i) (x i)
⊢ ((compContinuousLinearMapL f) φ) x =
    ((ContinuousLinearMap.comp
          (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
          (ContinuousLinearMap.comp
            (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
            ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e))))
        φ)
      x
Tactic:
simp [coe_domDomCongrₗᵢ', coe_domDomCongrₗᵢ'_symm, this, -Equiv.piCongrLeft'_symm_apply]
State after:
no goals