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

Goal state before:
pp: V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x y : V
hx : x ∉ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x y
⊢ y ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

Tactic:
by
  obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy
  rw [← Fintype.sum_subset (s := {i | w i ≠ 0})
    fun i hi ↦ mem_filter.2 ⟨mem_univ _, left_ne_zero_of_smul hi⟩]
  exact (convex_convexHull ..).sum_mem (fun i _ ↦ hw₀ _) (by rwa [sum_filter_ne_zero])
    fun i hi ↦ subset_convexHull _ _ ⟨ha _, IsVisible.of_convexHull_of_pos (fun _ _ ↦ hw₀ _) hw₁
      (by simpa) hx hxy (mem_univ _) <| (hw₀ _).lt_of_ne' (mem_filter.1 hi).2⟩

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

Goal state before:
pp: case inr.inr
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)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs : SignType.sign (w₁ i) = -SignType.sign (w₂ i)
h' : 0 < w₁ i
⊢ False

Tactic:
· rw [sign_pos h', eq_comm, neg_eq_iff_eq_neg, sign_eq_neg_one_iff] at hs
      exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg
        hw₁ hw₂ h' hs).wOppSide.not_sSameSide h

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
t : ℝ
ht : 0 ≤ t
h : 0 = t
⊢ IntervalIntegrable g volume 0 t

pp: case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
t : ℝ
ht : 0 ≤ t
h : 0 < t
⊢ IntervalIntegrable g volume 0 t

Tactic:
· simp [← h]

Goal state after:
case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
t : ℝ
ht : 0 ≤ t
h : 0 < t
⊢ IntervalIntegrable g volume 0 t
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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
⊢ g =ᵐ[volume.restrict (Ioo 0 M)] 0

Tactic:
obtain ⟨u, -, uM, ulim⟩ : ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < M) ∧ Tendsto u atTop (𝓝 M) :=
      exists_seq_strictMono_tendsto M

Goal state after:
α : 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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
⊢ g =ᵐ[volume.restrict (Ioo 0 M)] 0
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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
I : ν {a | f a ≤ M} = 0
H3 : ¬0 < ∫ (t : ℝ) in 0..u n, g t
⊢ False

Tactic:
not_lt,

Goal state after:
α : 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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
I : ν {a | f a ≤ M} = 0
H3 : ∫ (t : ℝ) in 0..u n, g t ≤ 0
⊢ False
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * ↑(k₂.choose k) * C₁ ^ k
x : D
i✝ : ℕ
hi✝ : i✝ ≤ n
i : ℕ
hi : i ∈ Finset.range (k₂ + 1)
⊢ C₂ * ((C₁ * (1 + ‖x‖) ^ k₁) ^ i * ↑(k₂.choose i)) ≤ C₂ * ↑(k₂.choose i) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂)

Tactic:
mul_pow,

Goal state after:
D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * ↑(k₂.choose k) * C₁ ^ k
x : D
i✝ : ℕ
hi✝ : i✝ ≤ n
i : ℕ
hi : i ∈ Finset.range (k₂ + 1)
⊢ C₂ * (C₁ ^ i * ((1 + ‖x‖) ^ k₁) ^ i * ↑(k₂.choose i)) ≤ C₂ * ↑(k₂.choose i) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * ↑(k₂.choose k) * C₁ ^ k
x : D
hg' : ∀ i ≤ n, ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
hf' : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
⊢ ↑n ! * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ n =
    ↑n ! * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)

Tactic:
mul_pow,

Goal state after:
D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * ↑(k₂.choose k) * C₁ ^ k
x : D
hg' : ∀ i ≤ n, ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
hf' : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
⊢ ↑n ! * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) ^ n * ((1 + ‖x‖) ^ k₁) ^ n) =
    ↑n ! * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)
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
f g : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport ⇑f ∪ tsupport ⇑g, isCompact' := ⋯ }
K_sub_Ω : ↑K ⊆ ↑Ω
f_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
⊢ toFun (f + g) = toFun f + toFun g

Tactic:
let g_K : 𝓓^{n}_{K}(E, F) :=
      .of_support_subset g.contDiff (subset_closure.trans subset_union_right)

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
f g : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport ⇑f ∪ tsupport ⇑g, isCompact' := ⋯ }
K_sub_Ω : ↑K ⊆ ↑Ω
f_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
g_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
⊢ toFun (f + g) = toFun f + toFun g
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ c • ⇑f ⁻¹' K
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))
⊢ ⇑f '' S ⊆ σ₁₂ c • K

Tactic:
by
    rw [image_subset_iff, this.isUnit.preimage_smul_setₛₗ σ₁₂]; exact hrS c hc.le

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

Goal state before:
pp: case right
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
j : Fin n
hy : (x, j) ∈ graph f
h✝ : i ≤ j
⊢ graph.proj ⟨(x, i), hx⟩ ≤ graph.proj ⟨(x, j), hy⟩

Tactic:
· simp [graph.proj]

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

Goal state before:
pp: n : ℕ
σ : Equiv.Perm (Fin n)
i✝ j✝ : Fin n
hij : i✝ < j✝
⊢ σ (σ⁻¹ i✝) = σ (σ⁻¹ j✝) → σ⁻¹ i✝ < σ⁻¹ j✝

Tactic:
h

Goal state after:
n : ℕ
σ : Equiv.Perm (Fin n)
i✝ j✝ : Fin n
hij : i✝ < j✝
h : σ (σ⁻¹ i✝) = σ (σ⁻¹ j✝)
⊢ σ⁻¹ i✝ < σ⁻¹ j✝
Module: Mathlib.Analysis.Matrix.Spectrum

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

Tactic:
h

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : hA.eigenvalues = hB.eigenvalues
⊢ ∏ i, (Polynomial.X - Polynomial.C ↑(hB.eigenvalues i)) = ∏ i, (Polynomial.X - Polynomial.C ↑(hB.eigenvalues i))
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : A.charpoly = B.charpoly
⊢ ((Multiset.map (⇑RCLike.re) A.charpoly.roots).sort fun x1 x2 ↦ x1 ≥ x2) =
    (Multiset.map (⇑RCLike.re) B.charpoly.roots).sort fun x1 x2 ↦ x1 ≥ x2

Tactic:
h

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
⊢ OrthogonalFamily 𝕜 (fun μ ↦ ↥(eigenspace T μ)) fun μ ↦ (eigenspace T μ).subtypeₗᵢ

Tactic:
by
  rintro μ ν hμν ⟨v, hv⟩ ⟨w, hw⟩
  by_cases hv' : v = 0
  · simp [hv']
  have H := hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector ⟨hv, hv'⟩)
  rw [mem_eigenspace_iff] at hv hw
  refine Or.resolve_left ?_ hμν.symm
  simpa [inner_smul_left, inner_smul_right, hv, hw, H] using (hT v w).symm

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
R : Type ?u.48
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass ℝ R F
inst✝ : ContinuousConstSMul R F
c : R
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (c • ⇑f) 0 (↑K)ᶜ

Tactic:
rw [← smul_zero c]

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
R : Type ?u.48
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass ℝ R F
inst✝ : ContinuousConstSMul R F
c : R
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (c • ⇑f) (c • 0) (↑K)ᶜ
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: case refine_2
𝕜 : 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
a✝ b✝ : Fin n
⊢ a✝ ≤ b✝ → Fin.revPerm b✝ ≤ Fin.revPerm a✝

Tactic:
h

Goal state after:
case refine_2
𝕜 : 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
a✝ b✝ : Fin n
h : a✝ ≤ b✝
⊢ Fin.revPerm b✝ ≤ Fin.revPerm a✝
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 : ℕ
E' : Type u_3
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace 𝕜 E'
inst✝ : FiniteDimensional 𝕜 E'
T' : E' →ₗ[𝕜] E'
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
hT' : T'.IsSymmetric
hn' : finrank 𝕜 E' = n
h : hT.eigenvalues hn = hT'.eigenvalues hn'
⊢ ∏ i, (Polynomial.X - Polynomial.C ↑(hT.eigenvalues hn i)) =
    ∏ i, (Polynomial.X - Polynomial.C ↑(hT'.eigenvalues hn' i))

Tactic:
h

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 : ℕ
E' : Type u_3
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace 𝕜 E'
inst✝ : FiniteDimensional 𝕜 E'
T' : E' →ₗ[𝕜] E'
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
hT' : T'.IsSymmetric
hn' : finrank 𝕜 E' = n
h : hT.eigenvalues hn = hT'.eigenvalues hn'
⊢ ∏ i, (Polynomial.X - Polynomial.C ↑(hT'.eigenvalues hn' i)) =
    ∏ i, (Polynomial.X - Polynomial.C ↑(hT'.eigenvalues hn' 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 : ℕ
E' : Type u_3
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace 𝕜 E'
inst✝ : FiniteDimensional 𝕜 E'
T' : E' →ₗ[𝕜] E'
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
hT' : T'.IsSymmetric
hn' : finrank 𝕜 E' = n
h : T.charpoly = T'.charpoly
⊢ ((Multiset.map (⇑RCLike.re) T.charpoly.roots).sort fun x1 x2 ↦ x1 ≥ x2) =
    (Multiset.map (⇑RCLike.re) T'.charpoly.roots).sort fun x1 x2 ↦ x1 ≥ x2

Tactic:
h

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 : ℕ
E' : Type u_3
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace 𝕜 E'
inst✝ : FiniteDimensional 𝕜 E'
T' : E' →ₗ[𝕜] E'
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
hT' : T'.IsSymmetric
hn' : finrank 𝕜 E' = n
h : T.charpoly = T'.charpoly
⊢ ((Multiset.map (⇑RCLike.re) T'.charpoly.roots).sort fun x1 x2 ↦ x1 ≥ x2) =
    (Multiset.map (⇑RCLike.re) T'.charpoly.roots).sort fun x1 x2 ↦ x1 ≥ x2
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✝ : Finite n
v : n → E
this : Fintype n
⊢ (gram 𝕜 v).PosSemidef

Tactic:
refine .of_dotProduct_mulVec_nonneg (isHermitian_gram _ _) fun x ↦ ?_

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
this : Fintype n
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ gram 𝕜 v *ᵥ x
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst✝ : μ.IsOpenPosMeasure
h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g
⊢ ↑↑((toLp p μ 𝕜) f) =ᵐ[μ] ↑↑((toLp p μ 𝕜) g)

Tactic:
h

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst✝ : μ.IsOpenPosMeasure
h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g
⊢ ↑↑((toLp p μ 𝕜) g) =ᵐ[μ] ↑↑((toLp p μ 𝕜) g)
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:
by
  rw [abs_eq_cfcₙ_coe_norm 𝕜 a, cfcₙ_eq_cfc, cfc_map_spectrum ..]

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 : (∫ (a : α), ‖(f - g) a‖ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (ENNReal.ofReal p).toReal⁻¹ ≤ ε ^ p⁻¹
⊢ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε

Tactic:
ENNReal.toReal_ofReal hp.le,

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 : (∫ (a : α), ‖(f - g) a‖ ^ p ∂μ) ^ p⁻¹ ≤ ε ^ p⁻¹
⊢ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε