mathlib-initiative/mathlib-tactics huggingface dataset:
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 - ε) / ε + (1 - w i) / w i + 1

Tactic:
by positivity

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 - ε) / ε

Tactic:
by positivity

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

Goal state before:
pp: 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} μ

Tactic:
exact f_mble.nullMeasurable measurableSet_Ici

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 0 ≤ 1 + ‖x‖

Tactic:
by positivity

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
⊢ 0 < 1 + ‖x‖

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω ↦ (1 + ‖ω‖) ^ (-r)
x : E
⊢ 0 ≤ (1 + ‖x‖) ^ (-r)

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
x✝ : E
⊢ 0 ≤ 1 + ‖x✝‖

Tactic:
by positivity

Goal state after:
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 : E → F
n k : ℕ
C : ℝ
x : E
⊢ 0 ≤ 1 + ‖x‖

Tactic:
by positivity

Goal state after:
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 : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : ℕ → ℕ
hk : ∀ (n : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
x : E
⊢ 0 ≤ (1 + ‖x‖) ^ k n

Tactic:
by positivity

Goal state after:
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 : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : ℕ → ℕ
hk : ∀ (n : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
x : E
⊢ 0 ≤ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k

Tactic:
by positivity

Goal state after:
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
n k₁ : ℕ
h₁ : iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₁
k₂ : ℕ
h₂ : iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₂
a✝ : E
⊢ 0 ≤ ‖a✝‖

Tactic:
by positivity

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ∞
x : ℝ
⊢ 0 x ≤ (fun t ↦ μ.real {a | t < f a}) x

Tactic:
by positivity

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
x : H
⊢ 0 ≤ 1 ^ 2 + 2 * 1 * ‖x‖

Tactic:
by positivity

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
y : H
⊢ 0 ≤ ‖y‖ ^ 2

Tactic:
by positivity

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

Goal state before:
pp: 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
⊢ 0 ≤ ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖

Tactic:
by positivity

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

Goal state before:
pp: 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)
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.range (N + 1)
⊢ 0 ≤ ‖Polynomial.eval r (descPochhammer ℝ x✝¹)‖

Tactic:
by positivity

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
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : T = 0
⊢ t ^ 2 / (2 * t) > 0

Tactic:
by positivity

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
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
⊢ min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t)) > 0

Tactic:
by positivity

Goal state after:
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:
image_subset_iff,

Goal state after:
𝕜₁ : 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)))
⊢ S ⊆ ⇑f ⁻¹' (σ₁₂ c • K)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: 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
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
this : r - ↑n ≤ ↑k
⊢ 0 ≤ |x|

Tactic:
by positivity

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
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
x : E
hc : c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
hx : ¬x = 0
⊢ 0 ≤ c * ‖x‖

Tactic:
by positivity

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
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
x : E
hc : c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
hx : ¬x = 0
⊢ 0 ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖

Tactic:
by positivity

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
inst✝ : Nontrivial E
hT' : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
⊢ 0 < ‖T‖

Tactic:
by positivity

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:
by apply integrable_one_add_norm; norm_num

Goal state after:
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₂
⊢ 0 ≤ x ^ (k + l) * f

Tactic:
by positivity

Goal state after:
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₂
⊢ 0 ≤ 1 + x

Tactic:
by positivity

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

Goal state before:
pp: case e'_12
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
e_8✝ : Real.instAddCommGroup = Real.instRCLike.toDivisionRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ toInnerProductSpaceReal.toModule
y : F
⊢ 2 • ⟪x₀, T y⟫_ℝ = ⟪x₀, T y⟫_ℝ + ⟪(T y, y).1, (T x₀, x₀).2⟫_ℝ

Tactic:
real_inner_comm _ x₀,

Goal state after:
case e'_12
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
e_8✝ : Real.instAddCommGroup = Real.instRCLike.toDivisionRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ toInnerProductSpaceReal.toModule
y : F
⊢ 2 • ⟪T y, x₀⟫_ℝ = ⟪T y, x₀⟫_ℝ + ⟪(T y, y).1, (T x₀, x₀).2⟫_ℝ
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 ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ⇑f}
huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}
T : Set M₂
hT : T.Finite
hTv✝ : closure[inst✝⁴.toTopologicalSpace] (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V
hTv : ⇑v '' closedBall 0 1 ⊆ ⋃ y ∈ T, y +ᵥ V
⊢ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ T, y +ᵥ U

Tactic:
image_subset_iff,

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 : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ⇑f}
huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}
T : Set M₂
hT : T.Finite
hTv✝ : closure[inst✝⁴.toTopologicalSpace] (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V
hTv : closedBall 0 1 ⊆ ⇑v ⁻¹' ⋃ y ∈ T, y +ᵥ V
⊢ closedBall 0 1 ⊆ ⇑u ⁻¹' ⋃ y ∈ T, y +ᵥ U
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₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ 0 < x

Tactic:
by positivity

Goal state after:
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₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ 0 ≤ x ^ (k + l) * f

Tactic:
by positivity

Goal state after:
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₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ 0 ≤ ((1 + x) / 2) ^ (-↑l)

Tactic:
by positivity

Goal state after:
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₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ 0 < (1 + x) / 2

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
v : E
⊢ 0 v ≤ ‖v‖ ^ k * ‖f v‖

Tactic:
by positivity

Goal state after:
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
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
hK : ∀ K > 0, ∃ x, ‖(T - μ • 1) x‖ < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
⊢ ‖C‖⁻¹ > 0

Tactic:
by positivity

Goal state after:
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
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
hK : ∀ K > 0, ∃ x, ‖(T - μ • 1) x‖ < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
⊢ ε > 0

Tactic:
by positivity

Goal state after:
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
⊢ 0 ≤ (1 + ‖x‖) ^ (-↑k)

Tactic:
by positivity

Goal state after:
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
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
⊢ ‖μ‖ * c / 2 > 0

Tactic:
by positivity

Goal state after:
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
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 1 ⊆ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hy_lim : Tendsto (fun n ↦ (T - μ • 1) (y_ n)) atTop (𝓝 0)
d : ℝ
hd₀ : d > 0
hd : ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
hyK : 0 ∈ K
hψy : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, ‖(y_ ∘ ψ) x‖ < ε
hy_eigen' : (T - μ • 1) 0 = 0
⊢ d > 0

Tactic:
by positivity

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

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔ Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j

Tactic:
by
  rw [eq_sort_iff']
  refine ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => ?_⟩, fun h i j hij => ?_⟩
  · exact ((Prod.Lex.toLex_lt_toLex.1 <| h hij).resolve_left hfij.not_lt).2
  · obtain he | hl := (h.1 hij.le).eq_or_lt <;> apply Prod.Lex.toLex_lt_toLex.2
    exacts [Or.inr ⟨he, h.2 i j hij he⟩, Or.inl hl]

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype n
inst✝² : DecidableEq n
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
h : ∀ (x y : E), inner 𝕜 (((toLin b.toBasis b.toBasis) A) x) y = inner 𝕜 (((toLin b.toBasis b.toBasis) Aᴴ) x) y
⊢ A.IsHermitian

Tactic:
simpa using! (LinearMap.ext fun x ↦ ext_inner_right _ (h x)).symm

Goal state after:
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
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
this✝ : Std.Symm fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (S (f n) - S (f m) + μ • f n)
hu : μ • (f m - u) = T (f m) - T (f n)
this : u ∈ (↑S ^ (m + 1)).range
⊢ ‖μ‖ ≤ ‖T (f m) - T (f n)‖

Tactic:
grw [← hu, norm_smul, mul_comm, ← hf_far _ u this, one_mul]

Goal state after:
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
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
S : X →L[𝕜] X := T - μ • 1
K✝ : NNReal
hK✝ : AntilipschitzWith K✝ ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
hp : Pairwise fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 (‖c‖ + 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (((fun n ↦ ↑T (f n)) ∘ ψ) n) (((fun n ↦ ↑T (f n)) ∘ ψ) N) < ε
⊢ ‖μ‖ > 0

Tactic:
by positivity

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

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
inst✝ : Nontrivial (Matrix n n 𝕜)
a : Matrix n n 𝕜
ha : IsSelfAdjoint a
⊢ (spectrum ℝ a).Nonempty

Tactic:
obtain (h | h) := isEmpty_or_nonempty n
    · obtain ⟨x, y, hxy⟩ := exists_pair_ne (Matrix n n 𝕜)
      exact False.elim <| Matrix.of.symm.injective.ne hxy <| Subsingleton.elim _ _
    · exact spectrum_real_eq_range_eigenvalues ha ▸ Set.range_nonempty _

Goal state after: