-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
@[simp]
lemma constFormalMultilinearSeries_zero [NontriviallyNormedField 𝕜] [NormedAddCommGroup E ]
    [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] :
    constFormalMultilinearSeries 𝕜 E (0 : F) = 0

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
⊢ constFormalMultilinearSeries 𝕜 E 0 = 0

Tactic:
ext n x

Result:
case h.H
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : Fin n → E
⊢ (constFormalMultilinearSeries 𝕜 E 0 n) x = (0 n) x

Proof state:
case h.H
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : Fin n → E
⊢ (constFormalMultilinearSeries 𝕜 E 0 n) x = (0 n) x

Tactic:
simp only [FormalMultilinearSeries.zero_apply, ContinuousMultilinearMap.zero_apply,
  constFormalMultilinearSeries]

Result:
case h.H
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : Fin n → E
⊢ (match n with
      | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
      | x => 0)
      x =
    0

Proof state:
case h.H.zero
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
x : Fin 0 → E
⊢ (match 0 with
      | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
      | x => 0)
      x =
    0

Tactic:
simp only [ContinuousMultilinearMap.uncurry0_apply]

Result:
no goals

Proof state:
case h.H
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : Fin n → E
⊢ (match n with
      | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
      | x => 0)
      x =
    0

Tactic:
induction n

Result:
case h.H.zero
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
x : Fin 0 → E
⊢ (match 0 with
      | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
      | x => 0)
      x =
    0

case h.H.succ
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
a✝ :
  ∀ (x : Fin n✝ → E),
    (match n✝ with
        | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
        | x => 0)
        x =
      0
x : Fin (n✝ + 1) → E
⊢ (match n✝ + 1 with
      | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
      | x => 0)
      x =
    0

Proof state:
case h.H.succ
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
a✝ :
  ∀ (x : Fin n✝ → E),
    (match n✝ with
        | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
        | x => 0)
        x =
      0
x : Fin (n✝ + 1) → E
⊢ (match n✝ + 1 with
      | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
      | x => 0)
      x =
    0

Tactic:
simp only [constFormalMultilinearSeries.match_1.eq_2, ContinuousMultilinearMap.zero_apply]

Result:
no goals