mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
h✝ : k + 1 ≤ n
⊢ ⇑({ toFun := fun f ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ } f) = fderiv ℝ ⇑f

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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
h✝ : ¬k + 1 ≤ n
⊢ ⇑({ toFun := fun f ↦ 0, map_add' := ⋯, map_smul' := ⋯ } f) = 0

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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
h✝ : k + 1 ≤ n
⊢ ⇑({ toFun := fun f ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ } f) = fderiv ℝ ⇑f

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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
h✝ : ¬k + 1 ≤ n
⊢ ⇑({ toFun := fun f ↦ 0, map_add' := ⋯, map_smul' := ⋯ } f) = 0
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 : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
h✝ : k + ↑i ≤ n
⊢ ⇑({ toFun := fun f ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ } f) =
    iteratedFDeriv ℝ i ⇑f

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 : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
h✝ : ¬k + ↑i ≤ n
⊢ ⇑({ toFun := fun f ↦ 0, map_add' := ⋯, map_smul' := ⋯ } f) = 0

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 : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
h✝ : k + ↑i ≤ n
⊢ ⇑({ toFun := fun f ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ } f) =
    iteratedFDeriv ℝ i ⇑f

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 : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
h✝ : ¬k + ↑i ≤ n
⊢ ⇑({ toFun := fun f ↦ 0, map_add' := ⋯, map_smul' := ⋯ } f) = 0
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst✝ : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ↑i ≤ n
⊢ Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ) ↔ ↑i ≤ n → Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)

pp: case neg
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst✝ : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ¬↑i ≤ n
⊢ Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ) ↔ ↑i ≤ n → Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)

Tactic:
<;>

Goal state after:
case pos
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst✝ : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ↑i ≤ n
⊢ Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ) ↔ ↑i ≤ n → Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)

case neg
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst✝ : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ¬↑i ≤ n
⊢ Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ) ↔ ↑i ≤ n → Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
x : α
⊢ ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ ↑2‖

Tactic:
Real.rpow_natCast

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
x : α
⊢ ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

Tactic:
by
  by_cases H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
  · simp (discharger := positivity) only [ContDiffMapSupportedIn.seminorm_le_iff, monoLM_apply, H,
      and_self, ↓reduceIte]
    intro hik _ _
    exact norm_iteratedFDeriv_apply_le_seminorm _ (hik.trans (mod_cast H.1))
  · simp [monoLM_eq_zero, H]

Goal state after:
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
⊢ Continuous ⇑(monoLM 𝕜)

Tactic:
refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms _ _ _ _ _)
      (ContDiffMapSupportedIn.withSeminorms _ _ _ _ _) _ (fun i ↦ ⟨{i}, 1, fun f ↦ ?_⟩)
    simpa using seminorm_monoLM_le 𝕜 f

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : Ring A
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : ContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : Algebra ℝ A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
⊢ spectrum 𝕜 (abs a) = (fun z ↦ ↑‖z‖) '' spectrum 𝕜 a

Tactic:
rw [abs_eq_cfcₙ_coe_norm 𝕜 a, cfcₙ_eq_cfc, cfc_map_spectrum ..]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs c) x = s.indicator (fun x ↦ c) x
hxs : x ∈ s
⊢ ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫ = s.indicator (fun x ↦ ⟪c, ↑↑f x⟫) x

pp: case neg
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs c) x = s.indicator (fun x ↦ c) x
hxs : x ∉ s
⊢ ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫ = s.indicator (fun x ↦ ⟪c, ↑↑f x⟫) x

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs c) x = s.indicator (fun x ↦ c) x
hxs : x ∈ s
⊢ ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫ = s.indicator (fun x ↦ ⟪c, ↑↑f x⟫) x

case neg
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs c) x = s.indicator (fun x ↦ c) x
hxs : x ∉ s
⊢ ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫ = s.indicator (fun x ↦ ⟪c, ↑↑f x⟫) x
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f : α → E),
    Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ MemLp f p μ ∧ HasCompactSupport f →
      AEStronglyMeasurable f μ

Tactic:
rintro f ⟨_f_cont, f_mem, _hf⟩

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f✝ : α → E
hf : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → E
_f_cont : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
f_mem : MemLp f p μ
_hf : HasCompactSupport f
⊢ AEStronglyMeasurable f μ
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
y : X
⊢ ↑(P (n + 1)) ((P n) y) = ↑(P n) y

Tactic:
by simp [ContinuousLinearMap.coe_coe, hcomp]

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: E : Type u_5
F : Type u_8
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : 𝓢(E, F)
x : E
⊢ (Δ f) x = Δ (⇑f) x

Tactic:
laplacian_eq_sum (stdOrthonormalBasis ℝ E)

Goal state after:
E : Type u_5
F : Type u_8
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : 𝓢(E, F)
x : E
⊢ (∑ i, ∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} f)) x = Δ (⇑f) x
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j) x = D.e j
h : i = j
⊢ D.e j = 1 • D.e i

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j) x = D.e j
h : ¬i = j
⊢ 0 = 0 • D.e i

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j) x = D.e j
h : i = j
⊢ D.e j = 1 • D.e i

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j) x = D.e j
h : ¬i = j
⊢ 0 = 0 • D.e i
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ hV.linearIsometry.range ≤ (⨆ i, (V i).range).topologicalClosure

Tactic:
rintro x ⟨f, rfl⟩

Goal state after:
case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : ↥(lp G 2)
⊢ hV.linearIsometry.toLinearMap f ∈ (⨆ i, (V i).range).topologicalClosure
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case false
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ CompleteSpace ↥(bif false then K else Kᗮ)

pp: case true
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ CompleteSpace ↥(bif true then K else Kᗮ)

Tactic:
<;>

Goal state after:
case false
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ CompleteSpace ↥(bif false then K else Kᗮ)

case true
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ CompleteSpace ↥(bif true then K else Kᗮ)
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ⟪b i, b j⟫ = if i = j then 1 else 0

Tactic:
← b.repr.inner_map_map (b i) (b j),

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ⟪b.repr (b i), b.repr (b j)⟫ = if i = j then 1 else 0
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
⊢ fourierCoeff ⇑(fourier n) = Pi.single n 1

Tactic:
by
  ext m
  rw [← fourierCoeff_congr_ae (coeFn_fourierLp 2 n), ← fourierBasis_repr,
    HilbertBasis.repr_apply_apply, coe_fourierBasis]
  obtain (rfl | hmn) := eq_or_ne m n
  · rw [inner_self_eq_norm_sq_to_K, (orthonormal_fourier (hT := hT)).1 m]; simp
  · rw [(orthonormal_fourier (hT := hT)).2 hmn]; simp [hmn]

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' ↦ (L v) w') (L v) w
⊢ HasFDerivAt (fun w ↦ ↑(𝐞 (-(L v) w))) ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM ∘SL L v) w

Tactic:
convert! (hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg using 1

Goal state after:
case e'_12
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' ↦ (L v) w') (L v) w
e_8✝ : addCommGroup = instNormedAddCommGroup.toAddCommGroup
e_9✝ : NormedSpace.complexToReal.toModule ≍ instInnerProductSpaceRealComplex.toModule
⊢ (-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM ∘SL L v =
    ContinuousLinearMap.toSpanSingleton ℝ (2 * ↑π * I * ↑(𝐞 (-(L v) w))) ∘SL (-L v)
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: case e_f
𝕜 : Type u_1
inst✝²³ : CommRing 𝕜
V : Type u_2
inst✝²² : AddCommGroup V
inst✝²¹ : Module 𝕜 V
inst✝²⁰ : MeasurableSpace V
W : Type u_3
inst✝¹⁹ : AddCommGroup W
inst✝¹⁸ : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopologyEither W V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst✝¹¹, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹¹] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
⊢ Integrable (fun x_1 ↦ e (-(-L.flip x_1) x) • g x_1) ν

Tactic:
have hLflip : Continuous fun (p : W × V) => (-L.flip p.1) p.2 :=
      (continuous_neg.comp hL).comp continuous_swap

Goal state after:
case e_f
𝕜 : Type u_1
inst✝²³ : CommRing 𝕜
V : Type u_2
inst✝²² : AddCommGroup V
inst✝²¹ : Module 𝕜 V
inst✝²⁰ : MeasurableSpace V
W : Type u_3
inst✝¹⁹ : AddCommGroup W
inst✝¹⁸ : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopologyEither W V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst✝¹¹, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹¹] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
hLflip : Continuous[instTopologicalSpaceProd, inst✝¹¹] fun p ↦ (-L.flip p.1) p.2
⊢ Integrable (fun x_1 ↦ e (-(-L.flip x_1) x) • g x_1) ν
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : 0 < a.re
c : ℝ
⊢ ∫ (x : ℝ) in Iic c, Complex.exp (a * ↑x) = Complex.exp (a * ↑c) / a

Tactic:
simpa [neg_mul, ← mul_neg, ← Complex.ofReal_neg,
    integral_comp_neg_Ioi (f := fun x : ℝ ↦ Complex.exp (a * x))]
    using integral_exp_mul_complex_Ioi (a := -a) (by simpa) (-c)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: case neg
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Tactic:
have : ¬ Integrable (fun x => f |x|) := by
      contrapose hf
      exact hf.integrableOn
    rw [← eq, integral_undef hf, integral_undef this, mul_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: case inl
s : ℝ
h : IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume
hs : s ≤ -1
this : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 1) volume
⊢ False

Tactic:
integrableOn_Ioo_rpow_iff zero_lt_one

Goal state after:
case inl
s : ℝ
h : IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume
hs : s ≤ -1
this : -1 < s
⊢ False
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), 𝐞 (-(v * w)) • f v

Tactic:
mul_comm _ w

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), 𝐞 (-(w * v)) • f v
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case right.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0

Tactic:
· exact Or.inr hxy

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case fst
r θ : ℝ
hr : (r, θ).1 ∈ Ioi 0
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 ^ 2 +
            ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 ^ 2),
        (Complex.equivRealProd.symm ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)).arg).1 =
    (r, θ).1

pp: case snd
r θ : ℝ
hr : (r, θ).1 ∈ Ioi 0
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 ^ 2 +
            ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 ^ 2),
        (Complex.equivRealProd.symm ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)).arg).2 =
    (r, θ).2

Tactic:
<;>

Goal state after:
case fst
r θ : ℝ
hr : (r, θ).1 ∈ Ioi 0
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 ^ 2 +
            ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 ^ 2),
        (Complex.equivRealProd.symm ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)).arg).1 =
    (r, θ).1

case snd
r θ : ℝ
hr : (r, θ).1 ∈ Ioi 0
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 ^ 2 +
            ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 ^ 2),
        (Complex.equivRealProd.symm ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)).arg).2 =
    (r, θ).2
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: p : ℝ × ℝ
⊢ (fderivPolarCoordSymm p).det = p.1

Tactic:
by
  conv_rhs => rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
  unfold fderivPolarCoordSymm
  simp only [neg_mul, LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin,
    Matrix.det_fin_two_of, sub_neg_eq_add]
  ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
⊢ Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)

Tactic:
| succ n n_ih =>

Goal state after: