mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Piecewise

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : LinearOrder E
inst✝⁷ : IsOrderedAddMonoid E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : PosSMulMono 𝕜 E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
⊢ (Set.Iic e).piecewise f g (a • x + b • y) ≤ a • (Set.Iic e).piecewise f g x + b • (Set.Iic e).piecewise f g y

Tactic:
rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hx,
      Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hy)]
    obtain hc | hc := le_or_gt (a • x + b • y) e
    · rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hc]
      have hc' : a • x + b • e ≤ a • x + b • y := by gcongr
      trans a • f x + b • f e
      · exact (h_anti (hc'.trans hc) hc hc').trans (hf.2 hx Set.self_mem_Iic ha hb hab)
      · rw [h_eq]
        gcongr
        exact h_mono Set.self_mem_Ici hy.le hy.le
    · rw [Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hc)]
      have hc' : a • x + b • y ≤ a • e + b • y := by gcongr
      trans a • g e + b • g y
      · exact (h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 Set.self_mem_Ici hy.le ha hb hab)
      · rw [← h_eq]
        gcongr
        exact h_anti hx Set.self_mem_Iic hx

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ ∃ a,
    ∃ (h : (∀ (x y : V), a x y = a y x) ∧ ∀ (x : V), a x x = false),
      SimpleGraph.mk' ⟨a, ⋯⟩ = { Adj := Adj, symm := hs, loopless := hi }

Tactic:
refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩

Goal state after:
case refine_1
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ ∀ (x y : V), (fun v w ↦ decide (Adj v w)) x y = (fun v w ↦ decide (Adj v w)) y x

case refine_2
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ ∀ (x : V), (fun v w ↦ decide (Adj v w)) x x = false

case refine_3
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ SimpleGraph.mk' ⟨fun v w ↦ decide (Adj v w), ⋯⟩ = { Adj := Adj, symm := hs, loopless := hi }
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G = ⊤ ↔ ∀ (a b : V), a ≠ b → G.Adj a b

Tactic:
simp [← top_le_iff, le_iff_adj]

Goal state after:
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a -[ℝ] c -ᵥ a]

Tactic:
simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
      eq_comm]

Goal state after:
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
ι : Type u_4
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall 0 r
⊢ ‖∑ k ∈ t, w k • z k‖ < r

Tactic:
rw [← mem_ball_zero_iff]

Goal state after:
V : Type u_2
ι : Type u_4
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall 0 r
⊢ ∑ k ∈ t, w k • z k ∈ ball 0 r
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : MulActionWithZero 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ eLpNorm (↑↑(f • g)) r μ ≤ eLpNorm (↑↑f) p μ * eLpNorm (↑↑g) q μ

Tactic:
rw [eLpNorm_congr_ae (coeFn_lpSMul f g)]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : MulActionWithZero 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ eLpNorm (↑↑f • ↑↑g) r μ ≤ eLpNorm (↑↑f) p μ * eLpNorm (↑↑g) q μ
Module: Mathlib.Analysis.Convex.Visible

Goal state before:

Tactic:
Module.rank ℝ (span ℝ (-x +ᵥ s)) ≤
      Module.rank ℝ (span ℝ
        (-x +ᵥ affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V)) := by
      push_cast
      refine Submodule.rank_mono ?_
      gcongr
      exact (subset_convexHull ..).trans <| hs.convexHull_subset_affineSpan_isVisible hx
    _ = Module.rank ℝ (span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y})) := by
      suffices h :
        -x +ᵥ (affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V) =
          span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) by
        rw [AffineSubspace.coe_pointwise_vadd, h, span_span]
      simp [← AffineSubspace.coe_pointwise_vadd, AffineSubspace.pointwise_vadd_span,
        vadd_set_insert, affineSpan_insert_zero]
    _ ≤ #(-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) := rank_span_le _
    _ = #{y ∈ s | IsVisible ℝ (convexHull ℝ s) x y} := by simp

Goal state after:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case refine_2.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
x✝ : SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∧ w₁ i ≠ 0
hs : 0 < w₂ i
h0 : w₁ i ≠ 0
h' : w₁ i < 0
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)

Tactic:
exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₂ hw₁ hs h').symm

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ (1 + ‖x‖ ^ 2) ^ (-r / 2) = 2 ^ (r / 2) * ((√2 * √(1 + ‖x‖ ^ 2)) ^ r)⁻¹

Tactic:
rpow_div_two_eq_sqrt,

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ √(1 + ‖x‖ ^ 2) ^ (-r) = 2 ^ (r / 2) * ((√2 * √(1 + ‖x‖ ^ 2)) ^ r)⁻¹

case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ √(1 + ‖x‖ ^ 2) ^ (-r) = 2 ^ (r / 2) * ((√2 * √(1 + ‖x‖ ^ 2)) ^ r)⁻¹

pp: case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖ ^ 2

Tactic:
rpow_div_two_eq_sqrt,

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ √(1 + ‖x‖ ^ 2) ^ (-r) = √2 ^ r * ((√2 * √(1 + ‖x‖ ^ 2)) ^ r)⁻¹

case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 2

case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖ ^ 2
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
⊢ ∫⁻ (t : ℝ) in Ioc 0 s, ∞ * ENNReal.ofReal (g t) ≤ ∫⁻ (t : ℝ) in Ioc 0 s, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
apply setLIntegral_mono' measurableSet_Ioc (fun x hx ↦ ?_)
          rw [← h's]
          gcongr
          exact fun ha ↦ hx.2.trans (le_of_lt ha)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
⊢ ∃ F, Measurable F ∧ 0 ≤ F ∧ f =ᵐ[μ] F

Tactic:
refine ⟨fun ω ↦ max (f_mble.mk f ω) 0, f_mble.measurable_mk.max measurable_const,
        fun ω ↦ le_max_right _ _, ?_⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
⊢ f =ᵐ[μ] fun ω ↦ max (AEMeasurable.mk f f_mble ω) 0
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
ω : α
hω : f ω = AEMeasurable.mk f f_mble ω
⊢ 0 ω ≤ f ω → f ω = max (AEMeasurable.mk f f_mble ω) 0

Tactic:
h'ω

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
ω : α
hω : f ω = AEMeasurable.mk f f_mble ω
h'ω : 0 ω ≤ f ω
⊢ f ω = max (AEMeasurable.mk f f_mble ω) 0
Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty

Goal state before:
pp: E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Tendsto (⇑f) (cocompact E) (𝓝 0)
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero, tendsto_def] at h

Goal state after:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : ∀ s ∈ 𝓝 0, (fun x ↦ ‖f x‖) ⁻¹' s ∈ cocompact E
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h₁
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := ⋯
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
⊢ ‖Polynomial.eval r (descPochhammer ℝ n)‖ ≤ ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖

Tactic:
have : n ∈ Finset.range (N + 1) := by grind

Goal state after:
case h₁
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this✝ : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
this : n ∈ Finset.range (N + 1)
⊢ ‖Polynomial.eval r (descPochhammer ℝ n)‖ ≤ ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ∏ i, (Polynomial.X - Polynomial.C ↑(hA.eigenvalues i)) ≠ 0

Tactic:
simp [Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero]

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:
intro w

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 ∈ (eigenspace T μ)ᗮ
w : E
⊢ w ∈ eigenspace T μ → ⟪w, T v⟫ = 0
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)
⊢ EqOn (⇑f + ⇑g) 0 (↑K)ᶜ

Tactic:
← add_zero 0

Goal state after:
𝕜 : 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)
⊢ EqOn (⇑f + ⇑g) (0 + 0) (↑K)ᶜ
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
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
v : E
μ : Eigenvalues T
⊢ ∀ (w : PiLp 2 fun μ ↦ ↥(eigenspace T (↑T 1 μ))),
    T (hT.diagonalization.symm w) = hT.diagonalization.symm (toLp 2 fun μ ↦ ↑T 1 μ • w.ofLp μ)

Tactic:
intro w

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ ↦ ↥(eigenspace T (↑T 1 μ))
⊢ T (hT.diagonalization.symm w) = hT.diagonalization.symm (toLp 2 fun μ ↦ ↑T 1 μ • w.ofLp μ)
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
inst✝ : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
f g : 𝓓^{n}_{K}(E, F)
⊢ { toFun := ⇑T ∘ ⇑(f + g), contDiff' := ⋯, zero_on_compl' := ⋯ } =
    { toFun := ⇑T ∘ ⇑f, contDiff' := ⋯, zero_on_compl' := ⋯ } +
      { toFun := ⇑T ∘ ⇑g, contDiff' := ⋯, zero_on_compl' := ⋯ }

Tactic:
ext x; exact map_add T (f x) (g x)

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
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
⊢ ∀ (w : EuclideanSpace 𝕜 (Fin n)),
    T ((hT.eigenvectorBasis hn).repr.symm w) =
      (hT.eigenvectorBasis hn).repr.symm (toLp 2 fun i ↦ ↑(hT.eigenvalues hn i) * w.ofLp i)

Tactic:
intro w

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ T ((hT.eigenvectorBasis hn).repr.symm w) =
    (hT.eigenvectorBasis hn).repr.symm (toLp 2 fun i ↦ ↑(hT.eigenvalues hn i) * w.ofLp i)
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
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
⊢ ∏ i, (Polynomial.X - Polynomial.C ((RCLike.ofReal ∘ hT.eigenvalues hn) i)) ≠ 0

Tactic:
simp [Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero]

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
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' spectrum 𝕜 a)
⊢ cfc (fun x ↦ f ↑‖x‖) a = cfc f (cfc (fun z ↦ ↑‖z‖) a)

Tactic:
← cfc_comp' ..

Goal state after:
𝕜 : 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
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' spectrum 𝕜 a)
⊢ cfc (fun x ↦ f ↑‖x‖) a = cfc (fun x ↦ f ↑‖x‖) a
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
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ Module.finrank 𝕜 ↥(↑(b.proj A)).range = A.card

Tactic:
rw [range_proj_eq_span, Set.image_eq_range, finrank_span_eq_card]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ Fintype.card ↑↑A = A.card

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ LinearIndependent 𝕜 fun (x : ↑↑A) ↦ ↑b ↑x
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
b : SchauderBasis 𝕜 X
n : ℕ
x : X
⊢ (b.proj n) x = ∑ i ∈ Finset.range n, (b.coord i) x • ↑b i

Tactic:
rw [proj, GeneralSchauderBasis.proj_apply]

Goal state after:
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 α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g (↑p.toNNReal) μ
hg : eLpNorm (f - g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ ∃ g,
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧
        Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g (ENNReal.ofReal p) μ

Tactic:
refine ⟨g, g_support, ?_, g_cont, g_mem⟩

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g (↑p.toNNReal) μ
hg : eLpNorm (f - g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε
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
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
H : 0 < ENNReal.toReal 2
⊢ (fun s ↦ ∑ b ∈ s, (fun i ↦ ‖↑f i‖ ^ ENNReal.toReal 2) b) = fun a ↦
    ‖∑ b ∈ a, (fun i ↦ (V i) (↑f i)) b‖ ^ ENNReal.toReal 2

Tactic:
ext s

Goal state after:
ι : 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✝ hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
H : 0 < ENNReal.toReal 2
s : Finset ι
⊢ ∑ b ∈ s, (fun i ↦ ‖↑f i‖ ^ ENNReal.toReal 2) b = ‖∑ b ∈ s, (fun i ↦ (V i) (↑f i)) b‖ ^ ENNReal.toReal 2
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
⊢ Integrable (fun t ↦ (fourier n) t • f t) haarAddCircle

Tactic:
apply hf.bdd_smul 1
  · exact (map_continuous (fourier n)).aestronglyMeasurable
  · apply ae_of_all; intro t
    rw [fourier_apply, Circle.norm_coe]

Goal state after: