mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

Tactic:
isBigO_iff'',

Goal state after:
G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ (∃ c > 0, ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ (∃ c, ∃ (_ : c > 0), ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔
    ∀ᶠ (n₀ : α) in atTop, ∃ c, ∃ (_ : c > 0), ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

Tactic:
Subtype.exists',

Goal state after:
G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ (∃ x, ∀ᶠ (x_1 : α) in atTop, ↑x * ‖f x_1‖ ≤ ‖g x_1‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ x, ∀ n ≥ n₀, ↑x * ‖f n‖ ≤ ‖g n‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ 2 * sin x * cos y = sin (x - y) + sin (x + y)

Tactic:
simp [sin_add, sin_sub]
  ring

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n ≤ f n.succ
⊢ ∀ n ≥ m, |(-f) n| ≤ a

Tactic:
simpa using ham

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

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(n % 2 + 2 * (n / 2)) * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
hn1,

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(1 + 2 * (n / 2)) * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball 1 δ / {x} = ball x⁻¹ δ

Tactic:
rw [ball_div_singleton, one_div]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ x • ball 1 δ = ball x δ

Tactic:
by
  rw [smul_ball, smul_eq_mul, mul_one]

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

Goal state before:
pp: case pos
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ ‖x ^ 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
simp only [_root_.pow_zero]

Goal state after:
case pos
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ ‖1 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (-(↑π / 2)) + sin (-(↑π / 2)) * I = -I

Tactic:
cos_neg,

Goal state after:
⊢ cos (↑π / 2) + sin (-(↑π / 2)) * I = -I
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
by
  simp_rw [sub_eq_add_neg, neg_ball, ball_add_ball hε hδ]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
h₁ : γ' 1 ⤳ y
⊢ JoinedIn F x y

Tactic:
have h : JoinedIn F (γ' 0) (γ' 1) := by
    refine ⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩
    simpa only [hf.continuous_iff, comp_def, hγ'] using map_continuous γ

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
h₁ : γ' 1 ⤳ y
h : JoinedIn F (γ' 0) (γ' 1)
⊢ JoinedIn F x y
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
γ' : Path y z
⊢ Continuous[_, inst✝¹] ((fun t ↦ if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ Subtype.val)

Tactic:
refine
      (Continuous.if_le ?_ ?_ continuous_id continuous_const (by simp)).comp
        continuous_subtype_val

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ γ : Path x y
γ' : Path y z
⊢ Continuous[_, inst✝¹] fun t ↦ γ.extend (2 * t)

case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ γ : Path x y
γ' : Path y z
⊢ Continuous[_, inst✝¹] fun t ↦ γ'.extend (2 * t - 1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i

Tactic:
by
  simp_rw [mul_comm]
  exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

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

Goal state before:
pp: f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i

Tactic:
by
  simp_rw [mul_comm]
  exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

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

Goal state before:
pp: x : ℝ
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
by_cases hx₁ : -1 ≤ x

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : x < -1
⊢ cos (-(π / 2)) = √(1 - x ^ 2)

Tactic:
cos_neg,

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ cos (π / 2) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

Tactic:
by_cases hx₁ : -1 ≤ x

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
by_cases hx₁ : -1 ≤ x

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
· rw [not_le] at hx₂
    rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]
    nlinarith

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case mp.inr.inl
h : log 0 = 0
⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = -1

pp: case mp.inr.inr
x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
· exact Or.inl rfl

Goal state after:
case mp.inr.inr
x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0

Tactic:
intro p hp

Goal state after:
case inr.hg
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ n.factorization p) = 0
⊢ n.factorization p = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ log ∘ rexp '' Iio (log a) = Iio (log a)

Tactic:
log_comp_exp,

Goal state after:
a : ℝ
ha : 0 < a
⊢ id '' Iio (log a) = Iio (log a)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ log ∘ rexp '' Iic (log a) = Iic (log a)

Tactic:
log_comp_exp,

Goal state after:
a : ℝ
ha : 0 < a
⊢ id '' Iic (log a) = Iic (log a)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log (↑n * ⅟↑d)

Tactic:
invOf_eq_inv,

Goal state after:
e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log (↑n * (↑d)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log (↑n * ⅟↑d)

Tactic:
invOf_eq_inv,

Goal state after:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log (↑n * (↑d)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log (↑n * ⅟↑d) ≠ 0

Tactic:
invOf_eq_inv,

Goal state after:
e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log (↑n * (↑d)⁻¹) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ Real.log (↑n * ⅟↑d) ≠ 0

Tactic:
invOf_eq_inv,

Goal state after:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ Real.log (↑n * (↑d)⁻¹) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))

Tactic:
convert!
    (Real.continuousAt_arcsin.comp_continuousWithinAt
          ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
            continuous_norm.continuousWithinAt _)).sub_const
      π using 1

Goal state after:
case e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun a ↦ ‖a‖)) z - π)

case convert_3
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.sign ≠ 0 ↔ ¬(θ = 0 ∨ θ = ↑π)

Tactic:
← sign_eq_zero_iff

Goal state after:
θ : Angle
⊢ θ.sign ≠ 0 ↔ ¬θ.sign = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ 0 < -x.re

Tactic:
neg_pos

Goal state after:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
obtain (h | h | h) := ψ.sign.trichotomy <;> obtain (h | h | h) := θ.sign.trichotomy

Goal state after:
case inl.inl.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = -1
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inl.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = -1
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inl.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = -1
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inr.inl.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 0
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inr.inl.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 0
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inr.inl.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 0
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inr.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 1
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inr.inr.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 1
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inr.inr.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 1
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) |(g a).im| b
x : α
hx : (fun x1 x2 ↦ x1 ≤ x2) |(g x).im| b
⊢ (fun x1 x2 ↦ x1 ≤ x2) (|(f x).arg| * |(g x).im|) (π * b)

Tactic:
exact mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) Real.pi_pos.le

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith c l (fun x ↦ f x ^ r) fun x ↦ g x ^ r

Tactic:
← rpow_inv_rpow hc.le hr.ne'

Goal state after:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith ((c ^ r⁻¹) ^ r) l (fun x ↦ f x ^ r) fun x ↦ g x ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
t : ℝ
⊢ 1 ≤ t → ‖t ^ a * t ^ b‖ ≤ t ^ c

Tactic:
ht

Goal state after:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ ‖t ^ a * t ^ b‖ ≤ t ^ c
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n ↦ ↑n ^ a
hg : g =O[atTop] fun n ↦ ↑n ^ b
h : a + b ≤ c
t : ℕ
⊢ 1 ≤ t → ‖↑t ^ a * ↑t ^ b‖ ≤ ↑t ^ c

Tactic:
ht

Goal state after:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n ↦ ↑n ^ a
hg : g =O[atTop] fun n ↦ ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ t
⊢ ‖↑t ^ a * ↑t ^ b‖ ≤ ↑t ^ c
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case hgf
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0

Tactic:
refine (eventually_gt_atTop 0).mono fun t ht h => ?_

Goal state after:
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t ^ b = 0
⊢ rexp (-a * t) = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: c : ℂ
t : ℝ
⊢ 0 < t → ‖↑t ^ c‖ = t ^ c.re

Tactic:
ht

Goal state after:
c : ℂ
t : ℝ
ht : 0 < t
⊢ ‖↑t ^ c‖ = t ^ c.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (x : ℝ × ℝ) in pure 0 ×ˢ 𝓝 y, x.1 ^ x.2 = 0

Tactic:
pure_prod,

Goal state after:
y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (x : ℝ × ℝ) in Filter.map (Prod.mk 0) (𝓝 y), x.1 ^ x.2 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 < x
⊢ x ^ y < x ^ z ↔ y < z

Tactic:
rw [lt_iff_not_ge, rpow_le_rpow_left_iff hx, lt_iff_not_ge]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ 0 < -(x, y).1

Tactic:
neg_pos

Goal state after:
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ (x, y).1 < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖↑p ^ (-s)‖ ≤ 1 / 2
⊢ False

Tactic:
← H,

Goal state after:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖1‖ ≤ 1 / 2
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
    rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
    simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Goal state after:
case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ False

case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ False

case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ -(midpoint R p₁ p₂ -ᵥ p) = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)

Tactic:
midpoint_vsub,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ -(⅟2 • (p₁ -ᵥ p) + ⅟2 • (p₂ -ᵥ p)) = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
u : Rˣ
v : Ray R M
⊢ 0 < -↑u ↔ ↑u < 0

Tactic:
neg_pos

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
u : Rˣ
v : Ray R M
⊢ ↑u < 0 ↔ ↑u < 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_2
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = (r₁ + r₂)⁻¹ • (r₂ • v₁ + r₂ • v₂)

Tactic:
← H,

Goal state after:
case inr.inr.refine_2
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = (r₁ + r₂)⁻¹ • (r₂ • v₁ + r₁ • v₁)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • 0 + b • x ∈ s
a : 𝕜
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ a • x ∈ s

Tactic:
simpa only [sub_add_cancel, eq_self_iff_true, forall_true_left, zero_add, smul_zero] using
      h (sub_nonneg_of_le ha₁) ha₀

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ ∀ (c : k) {x : V}, x ∈ ↑s -ᵥ ↑s → c • x ∈ ↑s -ᵥ ↑s

Tactic:
rintro c _ ⟨p₁, hp₁, p₂, hp₂, rfl⟩
    rw [← vadd_vsub (c • (p₁ -ᵥ p₂)) p₂]
    refine vsub_mem_vsub ?_ hp₂
    exact s.smul_vsub_vadd_mem c hp₁ hp₂ hp₂

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
h : v +ᵥ p ∈ s
⊢ p ∈ s

Tactic:
convert! vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) h

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
h : v +ᵥ p ∈ s
⊢ p = -v +ᵥ v +ᵥ p
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Tactic:
by
    apply h hy
    · positivity
    · positivity
    · rw [← add_div]
      exact div_self hab.ne'

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ ↑(affineSpan k s) -ᵥ ↑(affineSpan k s) ⊆ ↑(vectorSpan k s)

Tactic:
rintro v ⟨p₁, ⟨p₂, hp₂, v₁, hv₁, hp₁⟩, p₃, ⟨p₄, hp₄, v₂, hv₂, hp₃⟩, rfl⟩

Goal state after:
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ (fun x1 x2 ↦ x1 -ᵥ x2) p₁ p₃ ∈ ↑(vectorSpan k s)
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ∀ (x : E), (∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ a • i • s) → ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s

Tactic:
rintro x ⟨r, hr, hx⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ a • r • s
⊢ ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.ball 0 1
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
exact ((isVonNBounded_ball 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
hs : p1 -ᵥ p i0 = (s.weightedVSub p) w
s' : Finset ι := insert i0 s
w' : ι → k := (↑s).indicator w
h' : ∑ i ∈ s', w' i = 0
⊢ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

Tactic:
have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
      rw [hs]
      exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm

Goal state after:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
hs : p1 -ᵥ p i0 = (s.weightedVSub p) w
s' : Finset ι := insert i0 s
w' : ι → k := (↑s).indicator w
h' : ∑ i ∈ s', w' i = 0
hs' : (s'.weightedVSub p) w' = p1 -ᵥ p i0
⊢ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w