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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
⊢ ConvexIndependent 𝕜 Subtype.val

Tactic:
let fe : Set.range p ↪ ι := ⟨f, fun x₁ x₂ he => Subtype.ext (hf x₁ ▸ hf x₂ ▸ he ▸ rfl)⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }
⊢ ConvexIndependent 𝕜 Subtype.val
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
by
  have : ∀ {t}, μ t ≠ 0 → (⨍ x in t, f x ∂μ) ∈ s ∧ g (⨍ x in t, f x ∂μ) ≤ ⨍ x in t, g (f x) ∂μ :=
    fun ht =>
    hg.convexOn.set_average_mem_epigraph hgc hsc ht (by finiteness) (ae_restrict_of_ae hfs)
      hfi.integrableOn hgi.integrableOn
  refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_
  rintro ⟨t, hm, h₀, h₀', hne⟩
  rcases average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' (hfi.prodMk hgi) with
    ⟨a, b, ha, hb, hab, h_avg⟩
  rw [average_pair hfi hgi, average_pair hfi.integrableOn hgi.integrableOn,
    average_pair hfi.integrableOn hgi.integrableOn, Prod.smul_mk,
    Prod.smul_mk, Prod.mk_add_mk, Prod.mk_inj] at h_avg
  simp only [Function.comp] at h_avg
  rw [← h_avg.1, ← h_avg.2]
  calc
    g ((a • ⨍ x in t, f x ∂μ) + b • ⨍ x in tᶜ, f x ∂μ) <
        a * g (⨍ x in t, f x ∂μ) + b * g (⨍ x in tᶜ, f x ∂μ) :=
      hg.2 (this h₀).1 (this h₀').1 hne ha hb hab
    _ ≤ (a * ⨍ x in t, g (f x) ∂μ) + b * ⨍ x in tᶜ, g (f x) ∂μ := by
      gcongr
      exacts [(this h₀).2, (this h₀').2]

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

Goal state before:
pp: case inr.inl.inl
𝕜 : 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 : e < x
hy : y ≤ e
hc : a • x + b • y ≤ e
hc' : a • e + b • y ≤ a • x + b • y
⊢ f (a • x + b • y) ≤ a • g x + b • f y

Tactic:
trans a • f e + b • f y

Goal state after:
𝕜 : 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 : e < x
hy : y ≤ e
hc : a • x + b • y ≤ e
hc' : a • e + b • y ≤ a • x + b • y
⊢ f (a • x + b • y) ≤ a • f e + b • f y

𝕜 : 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 : e < x
hy : y ≤ e
hc : a • x + b • y ≤ e
hc' : a • e + b • y ≤ a • x + b • y
⊢ a • f e + b • f y ≤ a • g x + b • f y
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsStarConvexSet R (x + y) (s + t)

Tactic:
← Set.add_image_prod

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsStarConvexSet R (x + y) ((fun x ↦ x.1 + x.2) '' s ×ˢ t)
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
⊢ e.toFinset.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ⊆ e.toFinset → b.Nonempty → b ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
· constructor
      · exact Finset.nonempty_iff_ne_empty.mpr (Sym2.toFinset_ne_empty e)
      · intro b hb_sub hb_nonempty
        by_cases h : b.card = 1 <;>
          grind [Finset.card_eq_one, Finset.eq_of_subset_of_card_le hb_sub, Sym2.card_toFinset]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
⊢ (⋂ i, F i).Nonempty

Tactic:
rcases isEmpty_or_nonempty ι with _ | h_nonempty
  · simp only [iInter_of_empty, Set.univ_nonempty]
  /- By the finite version of theorem, every finite subfamily has an intersection. -/
  have h_fin (I : Finset ι) : (⋂ i ∈ I, F i).Nonempty := by
    apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])
    exact fun J _ hJ_card ↦ h_inter J hJ_card
  /- The following is a clumsy proof that family of compact sets with the finite intersection
  property has a nonempty intersection. -/
  have i0 : ι := Nonempty.some h_nonempty
  rw [show ⋂ i, F i = (F i0) ∩ ⋂ i, F i by simp [iInter_subset]]
  apply IsCompact.inter_iInter_nonempty
  · exact h_compact i0
  · intro i
    exact (h_compact i).isClosed
  · intro I
    simpa using h_fin ({i0} ∪ I)

Goal state after:
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: A : Type u_1
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace ℝ A
inst✝¹ : Nontrivial A
x : A
r : ℝ
inst✝ : StrictConvexSpace ℝ A
⊢ closedBall x r \ ball x r = sphere x r

Tactic:
closedBall_sdiff_ball

Goal state after:
A : Type u_1
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace ℝ A
inst✝¹ : Nontrivial A
x : A
r : ℝ
inst✝ : StrictConvexSpace ℝ A
⊢ sphere x r = sphere x r
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)

Tactic:
by
  rw [Set.disjoint_iff]
  rintro w ⟨h, h'⟩
  rw [mem_neighborSet, compl_adj] at h'
  exact h'.2 h

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

Goal state before:
pp: 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✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))

Tactic:
intro hx

Goal state after:
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✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
hx : x ∉ s
⊢ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: 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✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))

Tactic:
intro hx

Goal state after:
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✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
hx : x ∉ s
⊢ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜' : Type u_2
𝕜 : 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✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
x : α
⊢ ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(c • g) x = (c • ↑↑g) x → (c • ↑↑f • ↑↑g) x = (↑↑f • ↑↑(c • g)) x

Tactic:
hfx

Goal state after:
α : Type u_1
𝕜' : Type u_2
𝕜 : 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✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
x : α
hfx : ↑↑(c • f) x = (c • ↑↑f) x
⊢ ↑↑(c • g) x = (c • ↑↑g) x → (c • ↑↑f • ↑↑g) x = (↑↑f • ↑↑(c • g)) x
Module: Mathlib.Analysis.Distribution.Distribution

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
hx_mem : x ∈ tsupport ⇑f
⊢ False

Tactic:
exact hx (f.tsupport_subset hx_mem)

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

Goal state before:
pp: α : 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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s) = fun x ↦
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f x)
⊢ ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * ∫⁻ (a : α), {a | s ≤ f a}.indicator (fun x ↦ 1) a ∂μ =
    (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

Tactic:
lintegral_indicator₀

Goal state after:
α : 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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s) = fun x ↦
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f x)
⊢ ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * ∫⁻ (a : α) in {a | s ≤ f a}, 1 ∂μ =
    (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

case hs
α : 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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s) = fun x ↦
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f x)
⊢ NullMeasurableSet {a | s ≤ f a} μ
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
ω : α
⊢ g =ᵐ[volume.restrict (Ioc 0 (f ω))] fun a ↦ 0

Tactic:
exact ae_restrict_of_ae_restrict_of_subset Ioc_subset_Ioi_self H1

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
R : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : BorelSpace E
μ : Measure E
h : μ.IsAddHaarMeasure
⊢ Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑(finrank ℝ E + 1))) μ

Tactic:
apply integrable_one_add_norm; norm_num

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
⊢ HasEigenvalue T ↑(⨆ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)

Tactic:
have : IsMaxOn T'.val.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀ := by simpa only [← hx₀] using hTx₀

Goal state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this✝ : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ HasEigenvalue T ↑(⨆ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-(↑k * ↑p))‖ₑ ∂μ < ∞
x : E
⊢ ‖(1 + ‖x‖) ^ (-(↑k * ↑p))‖ₑ = ‖(1 + ‖x‖) ^ (-↑k)‖ₑ ^ ↑p

Tactic:
← neg_mul,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-(↑k * ↑p))‖ₑ ∂μ < ∞
x : E
⊢ ‖(1 + ‖x‖) ^ (-↑k * ↑p)‖ₑ = ‖(1 + ‖x‖) ^ (-↑k)‖ₑ ^ ↑p
Module: Mathlib.Analysis.Matrix.Hermitian

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst✝ : RCLike 𝕜
h : A.IsHermitian
i : n
⊢ star (A i i) = A i i

Tactic:
← conjTranspose_apply,

Goal state after:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst✝ : RCLike 𝕜
h : A.IsHermitian
i : n
⊢ Aᴴ i i = A i i
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: n : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
| A.trace = 0

Tactic:
hA.1.spectral_theorem,

Goal state after:
n : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
| (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) ⋯.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ ⋯.eigenvalues))).trace = 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 : 𝓓^{n}_{K}(E, F)
⊢ EqOn (-⇑f) 0 (↑K)ᶜ

Tactic:
by
    rw [← neg_zero]
    exact f.zero_on_compl.comp_left

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

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

Tactic:
by
  refine ⟨fun h => ⟨h.isHermitian, fun a => ?_⟩, fun ⟨h1, h2⟩ => ?_⟩
  · simp only [h.isHermitian.spectrum_eq_image_range, Set.mem_image, Set.mem_range,
      exists_exists_eq_and, Set.mem_ofPred_eq, forall_exists_index]
    rintro i rfl
    exact_mod_cast h.eigenvalues_nonneg _
  · rw [h1.posSemidef_iff_eigenvalues_nonneg]
    intro i
    simpa [h1.spectrum_eq_image_range] using @h2 (h1.eigenvalues i)

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Finite n
m : Type u_3
inst✝ : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosSemidef
hy : y.PosSemidef
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y).PosSemidef

Tactic:
classical
  have := Fintype.ofFinite n; have := Fintype.ofFinite m
  obtain ⟨a, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg
  obtain ⟨b, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hy.nonneg
  simpa [mul_kronecker_mul, ← conjTranspose_kronecker, star_eq_conjTranspose] using
    posSemidef_conjTranspose_mul_self _

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

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ abs a = a

Tactic:
rw [abs, ha.star_eq, sqrt_mul_self a ha]

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

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ a⁺ + a⁻ = abs a

Tactic:
by
  rw [CFC.posPart_def, CFC.negPart_def, ← cfcₙ_add .., abs_eq_cfcₙ_norm a ha]
  exact cfcₙ_congr fun x hx ↦ posPart_add_negPart x

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

Goal state before:
pp: case e'_2.e'_7
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2

Tactic:
· rw [div_eq_mul_inv, ENNReal.mul_inv_cancel two_ne_zero ENNReal.ofNat_ne_top]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' quasispectrum 𝕜 a)
hf0 : f 0 = 0
⊢ cfcₙ (fun x ↦ f ↑‖x‖) a = cfcₙ f (abs a)

Tactic:
rw [cfcₙ_comp' f (‖·‖) a, ← abs_eq_cfcₙ_coe_norm _ a]

Goal state after:
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✝ : Fintype ι
b : HilbertBasis ι 𝕜 E
⊢ span 𝕜 (Set.range ⇑b) = ⊤

Tactic:
have := (span 𝕜 (Finset.univ.image b : Set E)).closed_of_finiteDimensional

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✝ : Fintype ι
b : HilbertBasis ι 𝕜 E
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(span 𝕜 ↑(Finset.image (⇑b) Finset.univ))
⊢ span 𝕜 (Set.range ⇑b) = ⊤
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
x₀ : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f

Tactic:
by
  have := SchwartzMap.le_seminorm 𝕜 0 n f x₀
  rwa [pow_zero, one_mul] at this

Goal state after: