-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem one_add_le_sup_seminorm_apply {m : ℕ × ℕ} {k n : ℕ} (hk : k ≤ m.1) (hn : n ≤ m.2)
    (f : 𝓢(E, F)) (x : E) :
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤
      2 ^ m.1 * (Finset.Iic m).sup (fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Proof state:
case 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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i * ‖iteratedFDeriv ℝ n (⇑f) x‖ * ↑(k.choose i) ≤
    ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f * ↑(m.1.choose i)

Tactic:
gcongr

Result:
case h.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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

case h.h₂.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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ k.choose i ≤ m.1.choose i

Proof state:
case h.h₁.a
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ SchwartzMap.seminorm 𝕜 i n ≤ (Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2

Tactic:
exact Finset.le_sup_of_le (Finset.mem_Iic.2 <|
  Prod.mk_le_mk.2 ⟨Finset.mem_range_succ_iff.mp hi, hn⟩) le_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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
⊢ ∑ i ∈ Finset.range (m.1 + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
gcongr ∑ _i ∈ Finset.range (m.1 + 1), ?_ with i hi

Result:
case 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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ↑(m.1.choose i) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) 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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
x✝² : ℕ
x✝¹ : x✝² ∈ Finset.range (m.1 + 1)
x✝ : x✝² ∉ Finset.range (k + 1)
⊢ 0 ≤ ‖x‖ ^ x✝² * ↑(k.choose x✝²) * ‖iteratedFDeriv ℝ n (⇑f) x‖

Tactic:
positivity

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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ ∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
have hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1) := by
  rwa [Finset.range_subset, add_le_add_iff_right]

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
⊢ ∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Proof state:
case h.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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
apply (le_seminorm 𝕜 i n f x).trans

Result:
case h.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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ (SchwartzMap.seminorm 𝕜 i n) f ≤ ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Proof state:
case h.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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ (SchwartzMap.seminorm 𝕜 i n) f ≤ ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
apply Seminorm.le_def.1

Result:
case h.h₁.a
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ SchwartzMap.seminorm 𝕜 i n ≤ (Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2