Theorem: ContinuousLinearMap.coprodL_apply (ForML/ContinuousLinearMapCo.lean)

State before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
⊢ (coprodL R M₁ M₂ F) f = coprod f.1 f.2
Tactic:
refine ContinuousLinearMap.ext ?_
State after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
⊢ ∀ (x : M₁ × M₂), ((coprodL R M₁ M₂ F) f) x = (coprod f.1 f.2) x

State before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
⊢ ∀ (x : M₁ × M₂), ((coprodL R M₁ M₂ F) f) x = (coprod f.1 f.2) x
Tactic:
intro x
State after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((coprodL R M₁ M₂ F) f) x = (coprod f.1 f.2) x

State before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((coprodL R M₁ M₂ F) f) x = (coprod f.1 f.2) x
Tactic:
simp [coprodL]
State after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((bilinearComp (flip (apply R F)) (fst R (M₁ →L[R] F) (M₂ →L[R] F)) (fst R M₁ M₂) +
          bilinearComp (flip (apply R F)) (snd R (M₁ →L[R] F) (M₂ →L[R] F)) (snd R M₁ M₂))
        f)
      x =
    f.1 x.1 + f.2 x.2

State before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((bilinearComp (flip (apply R F)) (fst R (M₁ →L[R] F) (M₂ →L[R] F)) (fst R M₁ M₂) +
          bilinearComp (flip (apply R F)) (snd R (M₁ →L[R] F) (M₂ →L[R] F)) (snd R M₁ M₂))
        f)
      x =
    f.1 x.1 + f.2 x.2
Tactic:
rw [add_apply, add_apply]
State after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((bilinearComp (flip (apply R F)) (fst R (M₁ →L[R] F) (M₂ →L[R] F)) (fst R M₁ M₂)) f) x +
      ((bilinearComp (flip (apply R F)) (snd R (M₁ →L[R] F) (M₂ →L[R] F)) (snd R M₁ M₂)) f) x =
    f.1 x.1 + f.2 x.2

State before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((bilinearComp (flip (apply R F)) (fst R (M₁ →L[R] F) (M₂ →L[R] F)) (fst R M₁ M₂)) f) x +
      ((bilinearComp (flip (apply R F)) (snd R (M₁ →L[R] F) (M₂ →L[R] F)) (snd R M₁ M₂)) f) x =
    f.1 x.1 + f.2 x.2
Tactic:
rw [bilinearComp_apply, bilinearComp_apply]
State after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((flip (apply R F)) ((fst R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((fst R M₁ M₂) x) +
      ((flip (apply R F)) ((snd R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((snd R M₁ M₂) x) =
    f.1 x.1 + f.2 x.2

State before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((flip (apply R F)) ((fst R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((fst R M₁ M₂) x) +
      ((flip (apply R F)) ((snd R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((snd R M₁ M₂) x) =
    f.1 x.1 + f.2 x.2
Tactic:
simp
State after:
no goals