mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y ↦ ((fun z ↦ z * x) ⁻¹' s).indicator (fun x ↦ 1) y
this : ∀ (x y : G), s.indicator (fun x ↦ 1) (y * x) = ((fun z ↦ z * x) ⁻¹' s).indicator (fun b ↦ 1) y
⊢ ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun x ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ

Tactic:
simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator (measurable_mul_const _ sm),
    setLIntegral_one]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
⊢ f' a ≠ 0 → ↑(f a) * g a = ↑(f' a) * g' a

Tactic:
h_a_nonneg

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
⊢ ↑(f a) * g a = ↑(f' a) * g' a
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ ENNReal.ofReal (ε * 2⁻¹ ^ n) > 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b c : R
⊢ discrim (-a) (-b) (-c) = discrim a b c

Tactic:
simp [discrim]

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

Goal state before:
pp: case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ 0 ≤ 2⁻¹ ^ n

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ sqrt x ≤ 1 ↔ x ≤ 1

Tactic:
← sqrt_one,

Goal state after:
x : ℝ≥0
⊢ sqrt x ≤ sqrt 1 ↔ x ≤ sqrt 1
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ 1 ≤ sqrt x ↔ 1 ≤ x

Tactic:
← sqrt_one,

Goal state after:
x : ℝ≥0
⊢ sqrt 1 ≤ sqrt x ↔ sqrt 1 ≤ x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ 1 ≤ √x ↔ 1 ≤ x

Tactic:
← sqrt_one,

Goal state after:
x : ℝ
⊢ √1 ≤ √x ↔ √1 ≤ x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x ≤ 1 ↔ x ≤ 1

Tactic:
← sqrt_one,

Goal state after:
x : ℝ
⊢ √x ≤ √1 ↔ x ≤ √1
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ 0 ≤ √2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ 0 ≤ 3 / 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ι : Type u_2
s : Finset ι
f g : ι → ℝ
x✝¹ : ι
x✝ : x✝¹ ∈ s
⊢ 0 ≤ f x✝¹ ^ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ |z.re| ≤ ‖z‖

Tactic:
rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (Complex.norm_nonneg _), abs_mul_abs_self,
    norm_mul_self_eq_normSq]

Goal state after:
z : ℂ
⊢ z.re * z.re ≤ normSq z
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
⊢ 0 ≤ m

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ 0 ≤ m

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: case hx
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ 0 ≤ 2

Tactic:
positivity

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < ↑x

Tactic:
positivity

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ↑x

Tactic:
positivity

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ ↑x ≠ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f g : ι → α
inst✝ : PosSMulMono ℚ≥0 α
hfg : ∀ i ∈ s, f i ≤ g i
⊢ 0 ≤ (↑(#s))⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ 0 ≤ (↑(#s))⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (f i)
⊢ 0 ≤ (↑(#s))⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
R : Type u_3
n : ℕ
a : ℕ → ℚ
⊢ 0 ≤ 𝔼 j ∈ range n, a j ^ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
R : Type u_3
a : ULift.{2, 0} ℕ → ℚ
s : Finset (ULift.{2, 0} ℕ)
⊢ 0 ≤ 𝔼 j ∈ s, a j ^ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
R : Type u_3
n : ℕ
a : ℕ → ℚ
⊢ 0 ≤ 𝔼 j, 𝔼 i ∈ range n, (a ↑j ^ 2 + ↑i ^ 2)

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
R : Type u_3
n : ℕ
a : ℕ → ℚ
⊢ 0 < 𝔼 j, (a ↑j ^ 2 + 1)

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
R : Type u_3
a : ℕ → ℚ
⊢ 0 < 𝔼 j ∈ {1}, (a j ^ 2 + 1)

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
ι : Type u_5
s : Finset ι
f : ι → NormedAddGroupHom V₁ V₂
v : V₁
⊢ (∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v

Tactic:
simp only [coe_sum, Finset.sum_apply]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
⊢ 0 ≤ ‖g‖ * ‖f‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: case ofNat
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
a✝ : ℕ
⊢ ↑(U ^ Int.ofNat a✝) = ↑U ^ Int.ofNat a✝

pp: case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝

Tactic:
· simp [SubmonoidClass.coe_pow]

Goal state after:
case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
⊢ Quotient (orbitRel α β) → M

Tactic:
refine @Quotient.lift _ _ (_) (fun b ↦ ∑' (a : α), f (a • b)) ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
⊢ ∀ (a b : β), a ≈ b → ∑' (a_2 : α), f (a_2 • a) = ∑' (a : α), f (a • b)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ re (↑r * z) = re z * r

Tactic:
re_ofReal_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ r * re z = re z * r
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ 0 ≤
    ‖{ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
          invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
        x✝‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ 0 ≤ ‖x✝‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
⊢ re 1 * re 1 + im 1 * im 1 = 1

Tactic:
simp only [one_im, add_zero, mul_one, one_re, mul_zero]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re (↑(‖z‖ ^ 2)⁻¹ * (starRingEnd K) z) = re z / ‖z‖ ^ 2

Tactic:
re_ofReal_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (‖z‖ ^ 2)⁻¹ * re ((starRingEnd K) z) = re z / ‖z‖ ^ 2
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst✝¹] s
hse : s ⊆ e.source
⊢ IsOpen[inst✝] (↑e '' s)

Tactic:
rw [(image_eq_target_inter_inv_preimage (e := e) hse)]
  exact e.continuousOn_invFun.isOpen_inter_preimage e.open_target hs

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ c⁻¹ > 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ 0 < c

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ c⁻¹ > 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
x : α
hx : c⁻¹⁻¹ * ‖f x‖ ≤ ‖g x‖
⊢ 0 < c⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ 0 ≤ c * ‖g' x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ pa,
          (∀ᶠ (x : β) in l', pa x) ∧
            ∃ pb,
              (∀ᶠ (y : α) in l, pb y) ∧
                ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖

Tactic:
exact fun h _ hc ↦ ⟨fun _ ↦ True, eventually_true l', _, h hc, fun _ ↦ id⟩

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝³ : SeminormedRing R
S : Type u_17
inst✝² : NormedRing S
inst✝¹ : NormMulClass S
c c' : ℝ
l : Filter α
inst✝ : NormOneClass S
n : ℕ
f : α → S
g : α → R
h : IsBigOWith c l (f ^ n) (g ^ n)
hn : n ≠ 0
hc : c ≤ c' ^ n
hc' : 0 ≤ c'
x : α
hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖
⊢ 0 ≤ c' * ‖g x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ IsBigOWith c l (fun x ↦ (g x)⁻¹) fun x ↦ (f x)⁻¹

Tactic:
by
  refine IsBigOWith.of_bound (h.bound.mp (h₀.mono fun x h₀ hle => ?_))
  rcases eq_or_ne (f x) 0 with hx | hx
  · simp only [hx, h₀ hx, inv_zero, norm_zero, mul_zero, le_rfl]
  · have hc : 0 < c := pos_of_mul_pos_left ((norm_pos_iff.2 hx).trans_le hle) (norm_nonneg _)
    replace hle := inv_anti₀ (norm_pos_iff.2 hx) hle
    simpa only [norm_inv, mul_inv, ← div_eq_inv_mul, div_le_iff₀ hc] using! hle

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
x✝² : ℕ
x✝¹ : x✝² ∈ range j
x✝ : x✝² ∉ range n
⊢ 0 ≤ x ^ x✝² / ↑x✝²!

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n k : ℕ
x✝ : k ∈ range (n + 1)
⊢ 0 ≤ x ^ k / ↑k !

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 1 + x + x ^ 2 / 2 = ∑ i ∈ range 3, x ^ i / ↑i !

Tactic:
simp only [sum_range_succ, range_one, sum_singleton, _root_.pow_zero, factorial,
          pow_one, mul_one, Nat.mul_one,
          cast_succ]
        ring_nf

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh (2 * x) = 2 * sinh x * cosh x

Tactic:
rw [two_mul, sinh_add]

Goal state after:
x : ℂ
⊢ sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
⊢ ↑n.succ ≠ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
⊢ ↑n.factorial * ↑n ≠ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : ¬f x = 0
⊢ 0 < ‖f x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hab
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ 0 ≤ ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ 0 < ‖a‖⁻¹ + 1

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 0 ≤ ‖x‖ ^ k / (↑n + 1) ^ k

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
x : α
⊢ 0 ≤ C * ‖g' x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ 0 < Real.cosh x

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
simpa using zpow_eq_neg_zpow_iff₀ (α := α) one_ne_zero

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ 0 < x ^ 3

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case h
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ 0 < x ^ 3 * (5 / 36) + x ^ 4 * (3 / 32) + x ^ 5 * (17 / 576) + x ^ 6 * (7 / 1296) + x ^ 7 * (1 / 1296)

Tactic:
positivity

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

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
⊢ 0 < ε / (2 * Real.exp a)

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 0 ≤ abv x

Tactic:
positivity

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr.zero.hb
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = 0 + n.succ
⊢ r ^ n.succ ≠ 0

Tactic:
positivity

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

Goal state before:
pp: b c : ℝ
n : ℕ
hb : 0 < b
⊢ Tendsto (fun x ↦ (b * rexp x + c) / x ^ n) atTop atTop

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)
  · simp only [pow_zero, div_one]
    exact (tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds
  simp only [add_div, mul_div_assoc]
  exact
    ((tendsto_exp_div_pow_atTop n).const_mul_atTop hb).atTop_add
      (tendsto_const_nhds.div_atTop (tendsto_pow_atTop hn))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (2 * π) = 1

Tactic:
simp [two_mul, cos_add]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ cos (π / 2 - x) = sin x

Tactic:
← cos_neg,

Goal state after:
x : ℝ
⊢ cos (-(π / 2 - x)) = sin x
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
x✝ : ℕ
⊢ 0 ≤ rexp (c * f x✝)

Tactic:
positivity

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

Goal state before:
pp: c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
i : ℕ
⊢ rexp (c * f i) ≤ rexp (↑i * c)

Tactic:
refine Real.exp_monotone ?_

Goal state after:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
i : ℕ
⊢ c * f i ≤ ↑i * c
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inr
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
h0 : 0 < x
⊢ sin x ≠ 0

Tactic:
exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne'

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this✝ : 0 < sin ((y - x) / 2)
this : 0 < cos ((y + x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
fb : f.NormNoninc
x : M ⧸ S
⊢ ‖(lift S f hf) x‖ ≤ ‖x‖

Tactic:
by
  have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb
  simpa using le_of_opNorm_le _ (f.lift_norm_le _ _ fb') _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
⊢ 0 < π / 2 ^ (n + 1)

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case hy.refine_1
n : ℕ
⊢ 0 ≤ π / 2 ^ (n + 2)

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this✝ : Function.Surjective fun x ↦ c • x
this : ↑‖c‖₊ ≠ 0
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ y ∈ s, edist x y

Tactic:
simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: r : ℝ
k : ℕ
hk : k ≠ 0
⊢ Tendsto (fun n ↦ r / ↑n ^ k) atTop (𝓝 0)

Tactic:
simpa using Filter.Tendsto.const_div_atTop (tendsto_natCast_atTop_atTop (R := ℝ).comp
    (tendsto_pow_atTop hk)) r

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ 0 < 2 * 4

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ √2 / 2 > 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin ↑π = 0

Tactic:
by rw [← ofReal_sin, Real.sin_pi]; simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (2 * ↑π) = 1

Tactic:
simp [two_mul, cos_add]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℂ
⊢ cos (↑π / 2 - x) = sin x

Tactic:
← cos_neg,

Goal state after:
x : ℂ
⊢ cos (-(↑π / 2 - x)) = sin x
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ₁ γ₂ : Path x y
h : (fun γ ↦ ⇑γ.toContinuousMap) γ₁ = (fun γ ↦ ⇑γ.toContinuousMap) γ₂
⊢ γ₁ = γ₂

Tactic:
simp only [DFunLike.coe_fn_eq] at h
    cases γ₁; cases γ₂; congr

Goal state after: