-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem iteratedPDeriv_succ_right {n : ℕ} (m : Fin (n + 1) → E) (f : 𝓢(E, F)) :
    iteratedPDeriv 𝕜 m f = iteratedPDeriv 𝕜 (Fin.init m) (pderivCLM 𝕜 (m (Fin.last n)) f)

Proof state:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
⊢ (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last (n + 1)))) f)

Tactic:
have hmzero : Fin.init m 0 = m 0 := by simp only [Fin.init_def, Fin.castSucc_zero]

Result:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
hmzero : Fin.init m 0 = m 0
⊢ (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last (n + 1)))) f)

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
hmzero : Fin.init m 0 = m 0
⊢ Fin.tail m (Fin.last n) = m (Fin.last n.succ)

Tactic:
simp only [Fin.tail_def, Fin.succ_last]

Result:
no goals

Proof state:
case h.e_6.h
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
hmzero : Fin.init m 0 = m 0
hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ)
⊢ (iteratedPDeriv 𝕜 (Fin.tail m)) f = (iteratedPDeriv 𝕜 ?m.1062770) ((pderivCLM 𝕜 ?m.1063971) f)

Tactic:
exact IH _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ
m : Fin (n + 1) → E
f : 𝓢(E, F)
⊢ (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)

Tactic:
induction n with
| zero =>
  rw [iteratedPDeriv_zero, iteratedPDeriv_one]
  rfl
| succ n IH =>
  have hmzero : Fin.init m 0 = m 0 := by simp only [Fin.init_def, Fin.castSucc_zero]
  have hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ) := by
    simp only [Fin.tail_def, Fin.succ_last]
  calc
    _ = pderivCLM 𝕜 (m 0) (iteratedPDeriv 𝕜 _ f) := iteratedPDeriv_succ_left _ _ _
    _ = pderivCLM 𝕜 (m 0) ((iteratedPDeriv 𝕜 _) ((pderivCLM 𝕜 _) f)) := by
      congr 1
      exact IH _
    _ = _ := by
      simp only [hmtail, iteratedPDeriv_succ_left, hmzero, Fin.tail_init_eq_init_tail]

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
hmzero : Fin.init m 0 = m 0
⊢ (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last (n + 1)))) f)

Tactic:
have hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ) := by
  simp only [Fin.tail_def, Fin.succ_last]

Result:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
hmzero : Fin.init m 0 = m 0
hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ)
⊢ (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last (n + 1)))) f)

Proof state:
case zero
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
m : Fin (0 + 1) → E
⊢ (pderivCLM 𝕜 (m 0)) f = (pderivCLM 𝕜 (m (Fin.last 0))) f

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
hmzero : Fin.init m 0 = m 0
hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ)
⊢ (pderivCLM 𝕜 (m 0)) ((iteratedPDeriv 𝕜 (Fin.tail m)) f) =
    (pderivCLM 𝕜 (m 0)) ((iteratedPDeriv 𝕜 ?m.1062770) ((pderivCLM 𝕜 ?m.1063971) f))

Tactic:
congr 1

Result:
case h.e_6.h
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
hmzero : Fin.init m 0 = m 0
hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ)
⊢ (iteratedPDeriv 𝕜 (Fin.tail m)) f = (iteratedPDeriv 𝕜 ?m.1062770) ((pderivCLM 𝕜 ?m.1063971) f)

Proof state:
case zero
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
m : Fin (0 + 1) → E
⊢ (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last 0))) f)

Tactic:
rw [iteratedPDeriv_zero, iteratedPDeriv_one]

Result:
case zero
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
m : Fin (0 + 1) → E
⊢ (pderivCLM 𝕜 (m 0)) f = (pderivCLM 𝕜 (m (Fin.last 0))) f

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
⊢ Fin.init m 0 = m 0

Tactic:
simp only [Fin.init_def, Fin.castSucc_zero]

Result:
no goals