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

Goal state before:
pp: n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M ∈ (convexHull ℝ) {x | ∃ σ, Equiv.Perm.permMatrix ℝ σ = x}
⊢ ‖M‖ ≤ 1

Tactic:
have ⟨_, ⟨σ, rfl⟩, hσ⟩ := convexOn_univ_norm.exists_ge_of_mem_convexHull (by simp) hM

Goal state after:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M ∈ (convexHull ℝ) {x | ∃ σ, Equiv.Perm.permMatrix ℝ σ = x}
σ : Equiv.Perm n
hσ : ‖M‖ ≤ ‖Equiv.Perm.permMatrix ℝ σ‖
⊢ ‖M‖ ≤ 1
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
C D : PointedCone R M
⊢ dual p ↑(C ⊔ D) = dual p (↑C ∪ ↑D)

Tactic:
by simp [← dual_hull]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
h : f x * (ε + ‖x - y‖) ≤ ε * f y + ‖x - y‖ * f z
⊢ ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x)

Tactic:
linear_combination h

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ) (extremePoints ℝ s))
l : StrongDual ℝ E
r : ℝ
hlr : ∀ a ∈ closure ((convexHull ℝ) (extremePoints ℝ s)), l a < r
hrx : r < l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ z ∈ s, l z ≤ l y}
z : E
hzA : z ∈ s
hz : IsMaxOn (⇑l) s z
⊢ False

Tactic:
obtain ⟨y, hy⟩ := (h.isCompact hscomp).extremePoints_nonempty ⟨z, hzA, hz⟩

Goal state after:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ) (extremePoints ℝ s))
l : StrongDual ℝ E
r : ℝ
hlr : ∀ a ∈ closure ((convexHull ℝ) (extremePoints ℝ s)), l a < r
hrx : r < l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ z ∈ s, l z ≤ l y}
z : E
hzA : z ∈ s
hz : IsMaxOn (⇑l) s z
y : E
hy : y ∈ extremePoints ℝ {y | y ∈ s ∧ ∀ z ∈ s, l z ≤ l y}
⊢ False
Module: Mathlib.Analysis.Convex.KreinMilman

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : w ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x | x ∈ s ∧ f x = w}
⊢ w ∈ ⇑f '' extremePoints ℝ s

Tactic:
have ht₀ : {x ∈ s | f x = w}.Nonempty := by simpa using! extremePoints_subset hw

Goal state after:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : w ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x | x ∈ s ∧ f x = w}
ht₀ : {x | x ∈ s ∧ f x = w}.Nonempty
⊢ w ∈ ⇑f '' extremePoints ℝ s
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  (∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f) →
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
⊢ ∃ K, ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t

Tactic:
by
    obtain ⟨r, hr⟩ := h hx
    obtain ⟨ε, hε, hεD⟩ := Metric.mem_nhds_iff.1 <| Filter.inter_mem (hC.mem_nhds hx) hr
    simp only [preimage_ofPred_eq, Pi.abs_apply, subset_inter_iff, hC.nhdsWithin_eq hx] at hεD ⊢
    obtain ⟨K, hK⟩ := exists_lipschitzOnWith_of_isBounded (hf.subset hεD.1 (convex_ball ..))
      (half_lt_self hε) <| isBounded_iff_forall_norm_le.2 ⟨r, by simpa using! hεD.2⟩
    exact ⟨K, _, ball_mem_nhds _ (by simpa), hK⟩

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
B : ℕ → Set E := fun n ↦ ball x (↑n + 1)
this : μ (⋃ n, frontier (s ∩ B n)) = 0
y : E
hy : y ∈ frontier s
⊢ y ∈ ⋃ n, frontier (s ∩ B n)

Tactic:
clear this

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
B : ℕ → Set E := fun n ↦ ball x (↑n + 1)
y : E
hy : y ∈ frontier s
⊢ y ∈ ⋃ n, frontier (s ∩ B n)
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i
i✝ : M
i : I
hi : i ∈ w.weights.support
⊢ w.weights i ≠ 0

Tactic:
by simpa using hi

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ s * s' + (s * t' + t) = 1

Tactic:
rw [← add_assoc, ← mul_add, h', mul_one, h]

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

Goal state before:
pp: case e'_4
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ |s - s'| * dist x y = iConvexComb f fun i ↦ dist (![x, x, y] i) (![x, y, y] i)

pp: case e'_3
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])

Tactic:
· simp [Finsupp.sum_fintype, Fin.sum_univ_succ, f, hss', iConvexComb_eq_sum]

Goal state after:
case e'_3
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r

Tactic:
grw [abs_sub_comm, ← le_abs_self] at hj'

Goal state after:
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)
⊢ ∃ t ∈ K.faces, s ⊂ t

Tactic:
push Not at hs'

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
hs' : s ∈ K.faces → ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t
⊢ ∃ t ∈ K.faces, s ⊂ t
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v✝ w✝ : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj \ y.Adj) v w
⊢ x.Adj w v ∧ ¬y.Adj w v

Tactic:
rwa [x.adj_comm, y.adj_comm]

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

Goal state before:
pp: V : Type u
G H : SimpleGraph V
h : Disjoint G.support H.support
⊢ Disjoint G H

Tactic:
by
  simp_rw [Set.disjoint_left, mem_support] at h
  rw [← disjoint_edgeSet, Set.disjoint_left, Sym2.forall]
  grind [mem_edgeSet]

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

Goal state before:
pp: V : Type u
v w : V
⊢ ⊤.commonNeighbors v w = Set.univ \ {v, w}

Tactic:
ext u
  simp [commonNeighbors, eq_comm, not_or]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ (G.neighborSet v).Nonempty ↔ ¬G.IsIsolated v

Tactic:
by
  simp [Set.nonempty_iff_ne_empty]

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

Goal state before:
pp: case mp
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
hs : s.WSameSide x y
ho : s.WOppSide y x
h : x ∉ s ∧ y ∉ s
⊢ False

Tactic:
exact h.1 (wOppSide_self_iff.1 (hs.trans_wOppSide ho h.2))

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ 0 + (1 - w i) / w i + 0 ≤ (1 - ε) / ε + (1 - w i) / w i + 1

Tactic:
by gcongr <;> positivity

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

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
h : (↑s).Nonempty
⊢ IsConnected {y | s.SOppSide x y}

Tactic:
obtain ⟨p, hp⟩ := h
  have : Nonempty s := ⟨⟨p, hp⟩⟩
  rw [setOfPred_sOppSide_eq_image2 hx hp, ← Set.image_prod]
  refine (isConnected_Iio.prod (isConnected_iff_connectedSpace.2 ?_)).image _
    ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
  convert! AddTorsor.connectedSpace s.direction s

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1

Tactic:
rw [le_sub_iff_add_le', neg_inv]
  exact (Real.le_rpow_inv_iff_of_neg (by positivity) ht (neg_lt_zero.mpr hr)).symm

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 : 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
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = 0

Tactic:
have : (fun t ↦ μ {a : α | t ≤ f a} * ENNReal.ofReal (g t))
        =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0 := by
          filter_upwards [H1] with t ht using by simp [ht]

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
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
this : (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =ᵐ[volume.restrict (Ioi 0)] 0
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = 0
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : E → F
hf : ContDiff ℝ ∞ f ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
hg : ContDiff ℝ ∞ g ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
⊢ ContDiff ℝ ∞ (f + g) ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n (f + g) =O[⊤] fun x ↦ (1 + ‖x‖) ^ k

Tactic:
refine ⟨hf.1.add hg.1, fun n ↦ ?_⟩

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : E → F
hf : ContDiff ℝ ∞ f ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
hg : ContDiff ℝ ∞ g ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
n : ℕ
⊢ ∃ k, iteratedFDeriv ℝ n (f + g) =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case hf
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
⊢ Differentiable ℝ fun x ↦ ‖x‖ ^ 2

Tactic:
exact .norm_sq ℝ differentiable_id

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
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
by
  by_cases hx : x = 0
  · simp [hx]
  simp [field, norm_smul, T.reApplyInnerSelf_smul]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : u ∈ closure[ContinuousLinearMap.topologicalSpace] {f | IsCompactOperator ⇑f}
⊢ u ∈ {f | IsCompactOperator ⇑f}

Tactic:
rw [mem_closure_iff_nhds_zero] at hu

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
⊢ u ∈ {f | IsCompactOperator ⇑f}
Module: Mathlib.Analysis.Distribution.TemperateGrowth

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

Tactic:
simp [div_eq_inv_mul, ← Real.rpow_neg_one, ← Real.rpow_mul]

Goal state after:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this : 0 ≤ C₂
⊢ 2 ^ l * (C₁ + C₂) * ((1 + x) ^ l) ^ (-1) = 2 ^ l * ((1 + x) ^ l) ^ (-1) * (C₁ + C₂)
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
⊢ HasEigenvalue T ↑(⨆ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)

Tactic:
have := FiniteDimensional.proper_rclike 𝕜 E

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
⊢ HasEigenvalue T ↑(⨆ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
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
⊢ HasEigenvalue T ↑(⨅ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)

Tactic:
have := FiniteDimensional.proper_rclike 𝕜 E

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
⊢ HasEigenvalue T ↑(⨅ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective ⇑S
hS_anti : Topology.IsClosedEmbedding ⇑S
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
⊢ ∃ f,
    (∀ (n : ℕ), 1 ≤ ‖f n‖) ∧
      (∀ (n : ℕ), ‖f n‖ ≤ R) ∧
        (∀ (n : ℕ), f n ∈ LinearMap.range (S ^ n)) ∧ ∀ (n : ℕ), ∀ y ∈ LinearMap.range (S ^ (n + 1)), 1 ≤ ‖f n - y‖

Tactic:
by
  -- Construct the sequence of submodules `V n := (S ^ n).range`, and show that they are closed.
  let V (n : ℕ) : Submodule 𝕜 X := S.iterateRange n
  have hV_succ (n : ℕ) : V (n + 1) = (V n).map (S : End 𝕜 X) := LinearMap.iterateRange_succ
  have hV_closed (n : ℕ) : IsClosed (V n : Set X) := by
    induction n with
    | zero => simp [V, Module.End.one_eq_id]
    | succ n ih =>
      rw [hV_succ]
      apply hS_anti.isClosedMap _ ih
  -- Apply Riesz's lemma repeatedly using the closed subspace `V (n+1)` inside `V n`.
  have x (n : ℕ) : ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖ := by
    have h₁ : IsClosed ((V (n + 1)).comap (V n).subtype : Set (V n)) := by
      simpa using! (hV_closed (n + 1)).preimage_val
    have h₂ : ∃ x : V n, x ∉ (V (n + 1)).comap (V n).subtype := by
      simpa [iterate_succ, V, (iterate_injective hS_anti.injective n).eq_iff,
        Function.Surjective] using! hS_not_surj
    obtain ⟨⟨x, hx⟩, hxn, hxy⟩ := riesz_lemma_of_norm_lt hc hR h₁ h₂
    simp only [Submodule.mem_comap, Submodule.subtype_apply, Subtype.forall] at hxn hxy
    exact ⟨x, hx, by simpa using! hxy 0, hxn,
      fun y hy ↦ hxy y (S.iterateRange.monotone (by simp) hy) hy⟩
  -- Use the existential claim to construct the sequence `f n`.
  choose x hxv hxn hxn' hxy using x
  exact ⟨x, hxn, hxn', hxv, hxy⟩

Goal state after:
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
⊢ A.charpoly.roots.card = A.charpoly.natDegree

Tactic:
simp [hA.roots_charpoly_eq_eigenvalues]

Goal state after:
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 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ A.PosSemidef ↔ 0 ≤ hA.eigenvalues

Tactic:
by
  conv_lhs => rw [hA.spectral_theorem]
  simp [isUnit_coe.posSemidef_star_right_conjugate_iff, posSemidef_diagonal_iff, Pi.le_def]

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

Goal state before:
pp: case pos
𝕜 : 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
μ : 𝕜
hμ : HasEigenvalue T μ
⊢ {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card = finrank 𝕜 ↥(eigenspace T μ)

Tactic:
convert!
      hT.direct_sum_isInternal.card_filter_subordinateOrthonormalBasisIndex_eq hn
        hT.orthogonalFamily_eigenspaces' ⟨μ, hμ⟩ with i
    unfold unsortedEigenvalues
    let ⟨x, hx⟩ := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
      hT.orthogonalFamily_eigenspaces'
    rw [Eigenvalues.val_mk, RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)]
    exact Subtype.mk_eq_mk.symm

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
x : E
⊢ ‖f x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0) f

Tactic:
← norm_iteratedFDeriv_zero (𝕜 := ℝ) (f := f) (x := x)

Goal state after:
𝕜 : 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
f : 𝓓^{n}_{K}(E, F)
x : E
⊢ ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0) f