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

Goal state before:
pp: 𝕜 : Type u_1
𝕂 : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
F' : Type u_5
inst✝¹¹ : NormedAddCommGroup F'
inst✝¹⁰ : NormedSpace ℝ F'
inst✝⁹ : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → ↑K ⊆ ↑Ω → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : 𝓓^{n}_{K}(E, F)), toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f
toFun_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
c : 𝕜
f : 𝓓^{n}(Ω, F)
⊢ toFun (c • f) = c • toFun f

Tactic:
set K : Compacts E := ⟨tsupport f, f.hasCompactSupport⟩

Goal state after:
𝕜 : Type u_1
𝕂 : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
F' : Type u_5
inst✝¹¹ : NormedAddCommGroup F'
inst✝¹⁰ : NormedSpace ℝ F'
inst✝⁹ : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → ↑K ⊆ ↑Ω → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : 𝓓^{n}_{K}(E, F)), toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f
toFun_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
c : 𝕜
f : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport ⇑f, isCompact' := ⋯ }
⊢ toFun (c • f) = c • toFun f
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
𝕂 : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
F' : Type u_5
inst✝¹¹ : NormedAddCommGroup F'
inst✝¹⁰ : NormedSpace ℝ F'
inst✝⁹ : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → ↑K ⊆ ↑Ω → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : 𝓓^{n}_{K}(E, F)), toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f
toFun_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
c : 𝕜
f : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport ⇑f, isCompact' := ⋯ }
K_sub_Ω : ↑K ⊆ ↑Ω
⊢ toFun (c • f) = c • toFun f

Tactic:
let f_K : 𝓓^{n}_{K}(E, F) := .of_support_subset f.contDiff subset_closure

Goal state after:
𝕜 : Type u_1
𝕂 : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
F' : Type u_5
inst✝¹¹ : NormedAddCommGroup F'
inst✝¹⁰ : NormedSpace ℝ F'
inst✝⁹ : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → ↑K ⊆ ↑Ω → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : 𝓓^{n}_{K}(E, F)), toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f
toFun_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
c : 𝕜
f : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport ⇑f, isCompact' := ⋯ }
K_sub_Ω : ↑K ⊆ ↑Ω
f_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
⊢ toFun (c • f) = c • toFun f
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, μ.real {a | t < f a}

Tactic:
have key := lintegral_eq_lintegral_meas_lt μ f_nn f_intble.aemeasurable
  have lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞ := Integrable.lintegral_lt_top f_intble
  have rhs_finite : ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a} < ∞ := by simp only [← key, lhs_finite]
  have rhs_integrand_finite : ∀ (t : ℝ), t > 0 → μ {a | t < f a} < ∞ :=
    fun t ht ↦ measure_gt_lt_top f_intble ht
  convert! (ENNReal.toReal_eq_toReal_iff' lhs_finite.ne rhs_finite.ne).mpr key
  · exact integral_eq_lintegral_of_nonneg_ae f_nn f_intble.aestronglyMeasurable
  · have aux := @integral_eq_lintegral_of_nonneg_ae _ _ ((volume : Measure ℝ).restrict (Set.Ioi 0))
      (fun t ↦ μ.real {a : α | t < f a}) ?_ ?_
    · rw [aux]
      congr 1
      apply setLIntegral_congr_fun measurableSet_Ioi
      exact fun t t_pos ↦ ENNReal.ofReal_toReal (rhs_integrand_finite t t_pos).ne
    · exact Eventually.of_forall (fun x ↦ by positivity)
    · apply Measurable.aestronglyMeasurable
      refine Measurable.ennreal_toReal ?_
      exact Antitone.measurable (fun _ _ hst ↦ measure_mono (fun _ h ↦ lt_of_le_of_lt hst h))

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : ¬x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
· simp [hx]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : ¬x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
x : E
hx : x = 0
⊢ T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t))

pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
x : E
hx : ¬x = 0
⊢ T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t))

Tactic:
· simp [hx]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
x : E
hx : ¬x = 0
⊢ T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t))
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ U ∈ map (⇑f) (𝓝 0)

Tactic:
suffices (σ₁₂ <| c⁻¹) • K ⊆ U by
    grw [← this]
    have : IsUnit c⁻¹ := hcnz.isUnit.inv
    rwa [mem_map, this.preimage_smul_setₛₗ σ₁₂, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)]

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ σ₁₂ c⁻¹ • K ⊆ U
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
h : μ.HasTemperateGrowth
⊢ Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑μ.integrablePower)) μ

Tactic:
simpa [Measure.integrablePower, h] using h.exists_integrable.choose_spec

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

Goal state before:
pp: case h₁.hx2
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ (1 + x) / 2 ≤ 1

pp: case h₁.hz
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ -↑l ≤ 0

Tactic:
· linarith

Goal state after:
case h₁.hz
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ -↑l ≤ 0
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h₂
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ f ≤ C₁ + C₂

Tactic:
· linarith

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ σ⁻¹ = Equiv.refl (Fin n) ↔ σ⁻¹ = 1

Tactic:
one_def

Goal state after:
n : ℕ
σ : Perm (Fin n)
⊢ σ⁻¹ = Equiv.refl (Fin n) ↔ σ⁻¹ = Equiv.refl (Fin n)
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
x : ℝ
⊢ x ∈ spectrum ℝ A ↔ x ∈ Set.range hA.eigenvalues

Tactic:
conv_lhs => rw [hA.spectral_theorem, ← spectrum.algebraMap_mem_iff 𝕜]
  simp

Goal state after:
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) = A

Tactic:
conv_rhs => rw [hA.spectral_theorem]
  rfl

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
v : E
hv : v ∈ (⨆ μ, eigenspace T μ)ᗮ
⊢ T v ∈ (⨆ μ, eigenspace T μ)ᗮ

Tactic:
← Submodule.iInf_orthogonal

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
v : E
hv : v ∈ ⨅ i, (eigenspace T i)ᗮ
⊢ T v ∈ ⨅ i, (eigenspace T i)ᗮ
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:
· simp [hx]

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.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
h : ∀ᵐ (x : E) ∂μ.restrict ↑K, ‖(B (f x)) (φ x)‖ ≤ ‖φ x‖ * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f
⊢ ∫ (x : E) in ↑K, ‖φ x‖ * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f ∂μ ≤
    (∫ (x : E) in ↑K, ‖φ x‖ ∂μ) * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f

Tactic:
rw [integral_mul_const, integral_mul_const]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : ¬IntegrableOn φ (↑K) μ
⊢ ‖(integralAgainstBilinLM B μ φ) f‖ ≤
    (∫ (x : E) in ↑K, ‖φ x‖ ∂μ) * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f

Tactic:
· simp only [integralAgainstBilinLM, hφ, ↓reduceIte, LinearMap.coe_mk, AddHom.coe_mk, norm_zero]
    positivity

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

Goal state before:
pp: case pos.inr
α : 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✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs✝ : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hs : x ∈ s
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖

Tactic:
· simp [hgs hs, hs]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
x : X
A₀ : Finset β
hA₀ : ∀ (t : Finset β), Disjoint t A₀ → ‖∑ i ∈ t, (b.coord i) x • ↑b i‖ < 1
A : Finset β
hdecomp :
  (GeneralSchauderBasis.proj b A) x =
    (GeneralSchauderBasis.proj b (A ∩ A₀)) x + (GeneralSchauderBasis.proj b (A \ A₀)) x
⊢ ‖(GeneralSchauderBasis.proj b A) x‖ ≤
    (Finset.image (fun B ↦ ‖(GeneralSchauderBasis.proj b B) x‖) A₀.powerset).sup' ⋯ _root_.id + 1

Tactic:
hdecomp

Goal state after:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
x : X
A₀ : Finset β
hA₀ : ∀ (t : Finset β), Disjoint t A₀ → ‖∑ i ∈ t, (b.coord i) x • ↑b i‖ < 1
A : Finset β
hdecomp :
  (GeneralSchauderBasis.proj b A) x =
    (GeneralSchauderBasis.proj b (A ∩ A₀)) x + (GeneralSchauderBasis.proj b (A \ A₀)) x
⊢ ‖(GeneralSchauderBasis.proj b (A ∩ A₀)) x + (GeneralSchauderBasis.proj b (A \ A₀)) x‖ ≤
    (Finset.image (fun B ↦ ‖(GeneralSchauderBasis.proj b B) x‖) A₀.powerset).sup' ⋯ _root_.id + 1
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F✝ : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
v w : E
f : 𝓢(E, F)
x : E
⊢ (∂_{v + w} f) x = (∂_{v} f + ∂_{w} f) x

Tactic:
simp [lineDerivOp_apply_eq_fderiv]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F✝ : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
r : ℝ
y : E
f : 𝓢(E, F)
x : E
⊢ (∂_{r • y} f) x = (r • ∂_{y} f) x

Tactic:
simp [lineDerivOp_apply_eq_fderiv]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case refine_2.h
ι : 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)
⊢ ⨆ i, (V i).range ≤ hV.linearIsometry.range

pp: case refine_2.ht
ι : 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)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑hV.linearIsometry.range

Tactic:
· refine iSup_le ?_
      rintro i x ⟨x, rfl⟩
      use lp.single 2 i x
      exact hV.linearIsometry_apply_single x

Goal state after:
case refine_2.ht
ι : 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)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑hV.linearIsometry.range
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
⊢ adjoin ℂ (range fourier) ≤ star (adjoin ℂ (range fourier))

Tactic:
refine adjoin_le ?_

Goal state after:
T : ℝ
⊢ range fourier ⊆ ↑(star (adjoin ℂ (range fourier)))
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ ∫ (x : AddCircle T), (fourier j) x * (starRingEnd ℂ) ((fourier i) x) ∂haarAddCircle = if i = j then 1 else 0

Tactic:
← fourier_neg,

Goal state after:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ ∫ (x : AddCircle T), (fourier j) x * (fourier (-i)) x ∂haarAddCircle = if i = j then 1 else 0
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case neg
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ ∫ (x : AddCircle T), (fourier (j + -i)) x ∂haarAddCircle = 0

Tactic:
have hij : j + -i ≠ 0 := by
    exact sub_ne_zero.mpr (Ne.symm h)

Goal state after:
case neg
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
hij : j + -i ≠ 0
⊢ ∫ (x : AddCircle T), (fourier (j + -i)) x ∂haarAddCircle = 0
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
a✝ : AddCircle T
ht : ↑↑(fourierLp 2 i) a✝ = (fourier i) a✝
⊢ (starRingEnd ℂ) ((fourier i) a✝) * ↑↑f a✝ = (fourier (-i)) a✝ • ↑↑f a✝

Tactic:
← fourier_neg,

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
a✝ : AddCircle T
ht : ↑↑(fourierLp 2 i) a✝ = (fourier i) a✝
⊢ (fourier (-i)) a✝ * ↑↑f a✝ = (fourier (-i)) a✝ • ↑↑f a✝
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (x : AddCircle T), ‖↑↑f x‖ ^ 2 ∂haarAddCircle
⊢ HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle)

Tactic:
H₂,

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (x : AddCircle T), ‖↑↑f x‖ ^ 2 ∂haarAddCircle
⊢ HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2 =
    ∫ (t : AddCircle (b - a)), ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) t‖ ^ 2 ∂haarAddCircle

Tactic:
nth_rw 2 [← add_sub_cancel a b]

Goal state after:
case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in a..a + (b - a), ‖f x‖ ^ 2 =
    ∫ (t : AddCircle (b - a)), ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) t‖ ^ 2 ∂haarAddCircle