mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ (if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    (if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) +
      if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0

Tactic:
by
    split_ifs with hk
    · have hk' : 0 < (n : ℕ∞ω) := mod_cast (add_pos_of_right zero_lt_one k).trans_le hk
      ext
      simp [fderiv_add (f.contDiff.differentiable hk'.ne').differentiableAt
                       (g.contDiff.differentiable hk'.ne').differentiableAt, FunLike.coe_add]
    · simp

Goal state after:
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ = (RingHom.id 𝕜) c • ContDiffMapSupportedIn.of_support_subset ⋯ ⋯

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hk : ¬k + 1 ≤ n
⊢ 0 = (RingHom.id 𝕜) c • 0

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ = (RingHom.id 𝕜) c • ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hk : ¬k + 1 ≤ n
⊢ 0 = (RingHom.id 𝕜) c • 0

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hk : ¬k + 1 ≤ n
⊢ 0 = (RingHom.id 𝕜) c • 0
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : k + ↑i ≤ n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : ¬k + ↑i ≤ n
⊢ 0 = 0 + 0

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : k + ↑i ≤ n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : ¬k + ↑i ≤ n
⊢ 0 = 0 + 0

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : ¬k + ↑i ≤ n
⊢ 0 = 0 + 0
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : k + ↑i ≤ n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ = (RingHom.id 𝕜) c • ContDiffMapSupportedIn.of_support_subset ⋯ ⋯

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : ¬k + ↑i ≤ n
⊢ 0 = (RingHom.id 𝕜) c • 0

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : k + ↑i ≤ n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ = (RingHom.id 𝕜) c • ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : ¬k + ↑i ≤ n
⊢ 0 = (RingHom.id 𝕜) c • 0

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : ¬k + ↑i ≤ n
⊢ 0 = (RingHom.id 𝕜) c • 0
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: case refine_1
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
h : A.PosSemidef
a : 𝕜
⊢ a ∈ spectrum 𝕜 A → a ∈ {a | 0 ≤ a}

pp: case refine_2
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
x✝ : A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a | 0 ≤ a}
h1 : A.IsHermitian
h2 : spectrum 𝕜 A ⊆ {a | 0 ≤ a}
⊢ A.PosSemidef

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
h : A.PosSemidef
a : 𝕜
⊢ a ∈ spectrum 𝕜 A → a ∈ {a | 0 ≤ a}
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: case refine_2
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
x✝ : A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a | 0 ≤ a}
h1 : A.IsHermitian
h2 : spectrum 𝕜 A ⊆ {a | 0 ≤ a}
⊢ A.PosSemidef

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
x✝ : A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a | 0 ≤ a}
h1 : A.IsHermitian
h2 : spectrum 𝕜 A ⊆ {a | 0 ≤ a}
⊢ A.PosSemidef
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
x : E
hx : x ∈ K
⊢ ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C ↔ x ∈ K → ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
x : E
hx : x ∉ K
⊢ ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C ↔ x ∈ K → ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
x : E
hx : x ∈ K
⊢ ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C ↔ x ∈ K → ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
x : E
hx : x ∉ K
⊢ ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C ↔ x ∈ K → ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
x : E
hx : x ∉ K
⊢ ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C ↔ x ∈ K → ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs : (A.submatrix Subtype.val Subtype.val).PosSemidef
hBs : (B.submatrix Subtype.val Subtype.val).PosSemidef
⊢ (A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val).IsHermitian ∧
    ∀ (x_1 : ↥x.support → 𝕜),
      0 ≤ star x_1 ⬝ᵥ A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val *ᵥ x_1

Tactic:
refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs : (A.submatrix Subtype.val Subtype.val).PosSemidef
hBs : (B.submatrix Subtype.val Subtype.val).PosSemidef
y : ↥x.support → 𝕜
⊢ 0 ≤ star y ⬝ᵥ A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val *ᵥ y
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: case inl
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
i : n
x : E
j k : n
hij : i ≠ j
⊢ gram 𝕜 (Pi.single i x) j k = single i i (⟪x, x⟫_𝕜) j k

pp: case inr
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
i : n
x : E
k : n
⊢ gram 𝕜 (Pi.single i x) i k = single i i (⟪x, x⟫_𝕜) i k

Tactic:
·

Goal state after:
case inl
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
i : n
x : E
j k : n
hij : i ≠ j
⊢ gram 𝕜 (Pi.single i x) j k = single i i (⟪x, x⟫_𝕜) j k
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: case inr.inl
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
i : n
x : E
k : n
hik : i ≠ k
⊢ gram 𝕜 (Pi.single i x) i k = single i i (⟪x, x⟫_𝕜) i k

pp: case inr.inr
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
i : n
x : E
⊢ gram 𝕜 (Pi.single i x) i i = single i i (⟪x, x⟫_𝕜) i i

Tactic:
·

Goal state after:
case inr.inl
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
i : n
x : E
k : n
hik : i ≠ k
⊢ gram 𝕜 (Pi.single i x) i k = single i i (⟪x, x⟫_𝕜) i k
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this : (∀ (x : E), ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
hi : ↑i ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this : (∀ (x : E), ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
hi : ¬↑i ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this : (∀ (x : E), ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
hi : ↑i ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y = ∑ i, ∑ j, (starRingEnd 𝕜) (x i) * y j * ⟪v i, v j⟫_𝕜

pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ ∑ i, ∑ j, (starRingEnd 𝕜) (x i) * y j * ⟪v i, v j⟫_𝕜 = ⟪∑ i, x i • v i, ∑ i, y i • v i⟫_𝕜

Tactic:
·

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y = ∑ i, ∑ j, (starRingEnd 𝕜) (x i) * y j * ⟪v i, v j⟫_𝕜
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this : (∀ (x : E), ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
hi : ¬↑i ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this : (∀ (x : E), ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
hi : ¬↑i ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ ∑ i, ∑ j, (starRingEnd 𝕜) (x i) * y j * ⟪v i, v j⟫_𝕜 = ⟪∑ i, x i • v i, ∑ i, y i • v i⟫_𝕜

Tactic:
·

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ ∑ i, ∑ j, (starRingEnd 𝕜) (x i) * y j * ⟪v i, v j⟫_𝕜 = ⟪∑ i, x i • v i, ∑ i, y i • v i⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y = ⟪∑ i, x i • v i, ∑ i, y i • v i⟫_𝕜

Tactic:
trans ∑ i, ∑ j, conj (x i) * y j * ⟪v i, v j⟫_𝕜
  · simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]
  · simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
A : 𝓓^{n₁}_{K₁}(E, F) → E → F'
hadd : ∀ (f g : 𝓓^{n₁}_{K₁}(E, F)) (x : E), A (f + g) x = A f x + A g x
hsmul : ∀ (c : 𝕜) (f : 𝓓^{n₁}_{K₁}(E, F)) (x : E), A (c • f) x = c • A f x
hsmooth : ∀ (f : 𝓓^{n₁}_{K₁}(E, F)), ContDiff ℝ (↑n₂) (A f)
hsupp : ∀ (f : 𝓓^{n₁}_{K₁}(E, F)), EqOn (A f) 0 (↑K₂)ᶜ
hbound :
  ∀ (i : ℕ),
    ↑i ≤ n₂ →
      ∃ s C,
        0 ≤ C ∧
          ∀ (f : 𝓓^{n₁}_{K₁}(E, F)),
            ∀ x ∈ K₂, ‖iteratedFDeriv ℝ i (A f) x‖ ≤ C * (s.sup fun j ↦ ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ j) f
Φ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F') :=
  { toFun := fun f ↦ { toFun := A f, contDiff' := ⋯, zero_on_compl' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
i : ℕ
hi : ¬↑i ≤ n₂
⊢ ∃ s C,
    ∀ (x : 𝓓^{n₁}_{K₁}(E, F)),
      (ContDiffMapSupportedIn.seminorm 𝕜 E F' n₂ K₂ i) (Φ x) ≤
        C * (s.sup (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁)) x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
A : 𝓓^{n₁}_{K₁}(E, F) → E → F'
hadd : ∀ (f g : 𝓓^{n₁}_{K₁}(E, F)) (x : E), A (f + g) x = A f x + A g x
hsmul : ∀ (c : 𝕜) (f : 𝓓^{n₁}_{K₁}(E, F)) (x : E), A (c • f) x = c • A f x
hsmooth : ∀ (f : 𝓓^{n₁}_{K₁}(E, F)), ContDiff ℝ (↑n₂) (A f)
hsupp : ∀ (f : 𝓓^{n₁}_{K₁}(E, F)), EqOn (A f) 0 (↑K₂)ᶜ
hbound :
  ∀ (i : ℕ),
    ↑i ≤ n₂ →
      ∃ s C,
        0 ≤ C ∧
          ∀ (f : 𝓓^{n₁}_{K₁}(E, F)),
            ∀ x ∈ K₂, ‖iteratedFDeriv ℝ i (A f) x‖ ≤ C * (s.sup fun j ↦ ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ j) f
Φ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F') :=
  { toFun := fun f ↦ { toFun := A f, contDiff' := ⋯, zero_on_compl' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
i : ℕ
hi : ¬↑i ≤ n₂
⊢ ∃ s C,
    ∀ (x : 𝓓^{n₁}_{K₁}(E, F)),
      (ContDiffMapSupportedIn.seminorm 𝕜 E F' n₂ K₂ i) (Φ x) ≤
        C * (s.sup (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁)) x