mathlib-initiative/mathlib-tactics huggingface dataset:
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
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ (↑n.factorial)⁻¹ * ((↑n.succ - 1)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ)) =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
eq_div_iff_mul_eq h₃,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ (↑n.factorial)⁻¹ * ((↑n.succ - 1)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ)) * (↑n.factorial * ↑n) =
    ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
mul_mul_mul_comm,

Goal state after:
x y : ℂ
⊢ cos x * cos y + sin x * sin y * (I * I) = cos x * cos y - sin x * sin y
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
x₀ : E'
m : ℕ
h : 1 < m
⊢ (fun x ↦ ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x ↦ x - x₀

Tactic:
by
  simpa only [isLittleO_norm_right, pow_one] using isLittleO_pow_sub_pow_sub x₀ h

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

Goal state before:
pp: x : ℝ
⊢ sinh x - cosh x = -rexp (-x)

Tactic:
← neg_sub,

Goal state after:
x : ℝ
⊢ -(cosh x - sinh x) = -rexp (-x)
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)

Tactic:
rw [zpow_add' (by simp [em'])]

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ k * a ^ k
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ 1 + x + x ^ 2 < 1 / (1 - x)

Tactic:
lt_div_iff₀

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ (1 + x + x ^ 2) * (1 - x) < 1

x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ 0 < 1 - x
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:

Tactic:
(∑ i ∈ range K with max N M + 1 ≤ i,
          abv (f i) * abv ((∑ k ∈ range (K - i), g k) - ∑ k ∈ range K, g k)) ≤
        ∑ i ∈ range K with max N M + 1 ≤ i, abv (f i) * (2 * Q) := by
        gcongr
        rw [sub_eq_add_neg]
        grw [abv_add abv]
        rw [two_mul, abv_neg abv]
        gcongr <;> exact le_of_lt (hQ _)
    _ < ε / (4 * Q) * (2 * Q) := by
        rw [← sum_mul, ← sum_range_sub_sum_range (le_of_lt hNMK)]
        have := lt_of_le_of_lt (abv_nonneg _ _) (hQ 0)
        gcongr
        exact (le_abs_self _).trans_lt <|
          hM _ ((Nat.le_succ_of_le (le_max_right _ _)).trans hNMK.le) _ <|
            Nat.le_succ_of_le <| le_max_right _ _

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

Goal state before:
pp: a : ℝ
this : ∀ (a : ℂ), ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 a, dist ((cexp - 1) x) ((cexp - 1) a) < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
intro ε hε

Goal state after:
a : ℝ
this : ∀ (a : ℂ), ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 a, dist ((cexp - 1) x) ((cexp - 1) a) < ε
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
⊢ ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
intro x

Goal state after:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
⊢ x ∈ {x | x.re ≤ a} → ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: x : ℝ
⊢ rexp (x / 2) = √(rexp x)

Tactic:
rw [eq_comm, sqrt_eq_iff_eq_sq, sq, ← exp_add, add_halves] <;> exact (exp_pos _).le

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

Goal state before:
pp: ⊢ π / 2 ≤ 2

Tactic:
by
  rw [Real.pi, mul_div_cancel_left₀ _ two_ne_zero]
  exact (Classical.choose_spec exists_cos_eq_zero).1.2

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
this✝ : Nonempty ↑{m | ↑m = x}
this : Nonempty ↑{m | ↑m = y}
⊢ ∀ (i : ↑{m | ↑m = x}) (j : ↑{m | ↑m = y}), ⨅ y_1, dist 1 ↑y_1 ≤ dist 1 ↑i + dist 1 ↑j

Tactic:
rintro ⟨a, rfl⟩ ⟨b, rfl⟩

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
a : M
this✝ : Nonempty ↑{m | ↑m = ↑a}
b : M
this : Nonempty ↑{m | ↑m = ↑b}
⊢ ⨅ y, dist 1 ↑y ≤ dist 1 ↑⟨a, ⋯⟩ + dist 1 ↑⟨b, ⋯⟩
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded t ∨ IsBounded s

Tactic:
exact AntilipschitzWith.isBounded_of_image2_left _ (fun x => (isometry_mul_left x).antilipschitz)
    (by rwa [image2_swap])

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NontrivialTopology E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ x, ‖x‖ = c

Tactic:
use c • ‖x‖⁻¹ • x

Goal state after:
case h
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NontrivialTopology E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ‖c • ‖x‖⁻¹ • x‖ = c
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁷ : Field R✝
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
v w : AbsoluteValue R✝ S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
_i : OrderTopology S
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ ∀ (ξ : R), ‖ξ‖ < 1 → Summable fun n ↦ ξ ^ n

Tactic:
intro x

Goal state after:
α : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁷ : Field R✝
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
v w : AbsoluteValue R✝ S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
_i : OrderTopology S
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
⊢ ‖x‖ < 1 → Summable fun n ↦ x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c * c + cos (2 * θ) * s = 2 * s * c * c + (2 * c ^ 2 - 1) * s

Tactic:
rw [cos_two_mul]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < ↑r
this : ENNReal.ofReal δ < ↑r
⊢ δ < ↑r

Tactic:
ofReal_eq_coe_nnreal hδ.le

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < ↑r
this : ↑(NNReal.mk δ ⋯) < ↑r
⊢ δ < ↑r
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
⊢ ∀ (x : X), Continuous[inst✝², inst✝¹] fun y ↦ g (x, y)

Tactic:
intro x

Goal state after:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
x : X
⊢ Continuous[inst✝², inst✝¹] fun y ↦ g (x, y)
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ Injective ⇑toAddCircle

Tactic:
intro x

Goal state after:
N : ℕ
inst✝ : NeZero N
x : ZMod N
⊢ ∀ ⦃a₂ : ZMod N⦄, toAddCircle x = toAddCircle a₂ → x = a₂
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: ⊢ ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|

Tactic:
intro x

Goal state after:
x : ℝ
⊢ ‖↑x‖ = |x - ↑(round x)|
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ ∀ (x : ℝ) (h : x ∈ I), (γ.truncate t₀ t₁) ⟨x, h⟩ ∈ range ⇑γ.extend

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ x : ℝ
⊢ ∀ (h : x ∈ I), (γ.truncate t₀ t₁) ⟨x, h⟩ ∈ range ⇑γ.extend
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
arccos_of_le_neg_one hx₁.le,

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ sin π = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg = (↑(rexp z.re) * cexp (↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg

Tactic:
ofReal_exp,

Goal state after:
z : ℂ
⊢ (cexp z).arg = (cexp ↑z.re * cexp (↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg ∈ Ioc (-π) π

Tactic:
by
  have hπ : 0 < π := Real.pi_pos
  rcases eq_or_ne z 0 with (rfl | hz)
  · simp [hπ, hπ.le]
  rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩
  rw [two_mul, neg_add_cancel_left, ← two_mul, zsmul_eq_mul] at hN
  rw [← norm_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N, ← sin_add_int_mul_two_pi _ N]
  have := arg_mul_cos_add_sin_mul_I (norm_pos_iff.mpr hz) hN
  push_cast at this
  rwa [this]

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

Goal state before:
pp: x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x ≠ 0

Tactic:
← log_one,

Goal state after:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x ≠ log 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
h : log x ≠ 0
⊢ log x < x - 1

Tactic:
linarith [add_one_lt_exp h, exp_log hx1]

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

Goal state before:
pp: n : ℕ
⊢ (fun x ↦ log x ^ n) =o[atTop] id

Tactic:
rw [Asymptotics.isLittleO_iff_tendsto']

Goal state after:
n : ℕ
⊢ Tendsto (fun x ↦ log x ^ n / id x) atTop (𝓝 0)

n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case pos
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∃ w, cexp w = z
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
rcases h with ⟨w, rfl⟩
      simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.ofPred_exists]
      exact Set.countable_iUnion fun m => Set.countable_singleton _

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

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log e

Tactic:
NormNum.IsInt.neg_to_eq h rfl

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-↑n)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log e

Tactic:
NormNum.IsInt.neg_to_eq h rfl

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log (-↑n)
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:
← div_eq_mul_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:
← div_eq_mul_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:
← div_eq_mul_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:
← div_eq_mul_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.Pow.Asymptotics

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
⊢ EqOn ((rexp ∘ fun x ↦ a * (x / (b * rexp x + c))) ∘ log) (fun x ↦ x ^ (a / (b * x + c))) (Set.Ioi 0)

Tactic:
intro x

Goal state after:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
⊢ x ∈ Set.Ioi 0 → ((rexp ∘ fun x ↦ a * (x / (b * rexp x + c))) ∘ log) x = (fun x ↦ x ^ (a / (b * x + c))) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y z : ℝ
hx : 0 ≤ x
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
exact rpow_add' hx (ne_of_gt <| add_pos_of_pos_of_nonneg hy hz)

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

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, ↑x < a ^ y

Tactic:
intro x

Goal state after:
y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, ↑x < a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
⊢ ∀ x < 0, -(log x * |x|) = log x * x

Tactic:
intro x

Goal state after:
h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
x : ℝ
⊢ x < 0 → -(log x * |x|) = log x * x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
⊢ y ^ z < x ^ z

Tactic:
by
  have := hx.trans hxy
  rw [← inv_lt_inv₀, ← rpow_neg, ← rpow_neg]
  on_goal 1 => refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)
  all_goals positivity

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

Goal state before:
pp: y : ℝ
h : 0 < y
⊢ ↑0 ^ y = ↑0

Tactic:
← ENNReal.some_eq_coe

Goal state after:
y : ℝ
h : 0 < y
⊢ some 0 ^ y = some 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
h : y < 0
⊢ ↑0 ^ y = ∞

Tactic:
← ENNReal.some_eq_coe

Goal state after:
y : ℝ
h : y < 0
⊢ some 0 ^ y = ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
← ENNReal.some_eq_coe

Goal state after:
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ some (x ^ y) = ↑x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (0, y)

pp: case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)

Tactic:
· -- x = 0 : reduce to continuousAt_cpow_zero_of_re_pos
    have A : ContinuousAt (fun p => p.1 ^ p.2 : ℂ × ℂ → ℂ) ⟨↑(0 : ℝ), y⟩ := by
      rw [ofReal_zero]
      apply continuousAt_cpow_zero_of_re_pos
      tauto
    have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ := by fun_prop
    exact A.comp_of_eq B rfl

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

Goal state before:
pp: case top.inr.inl
y : ℝ
hy✝ : 0 ≤ y
hy : 0 < y
hz : 0 ≤ 0
⊢ ∞ ^ (y + 0) = ∞ ^ y * ∞ ^ 0

Tactic:
rw [rpow_zero, mul_one, add_zero]

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

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ log x * y ≤ 0 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y

Tactic:
mul_nonpos_iff,

Goal state after:
x y : ℝ
hx : 0 < x
⊢ 0 ≤ log x ∧ y ≤ 0 ∨ log x ≤ 0 ∧ 0 ≤ y ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: z : ℝ
h : 0 < z
⊢ StrictMono fun x ↦ x ^ z

Tactic:
intro x

Goal state after:
z : ℝ
h : 0 < z
x : ℝ≥0∞
⊢ ∀ ⦃b : ℝ≥0∞⦄, x < b → (fun x ↦ x ^ z) x < (fun x ↦ x ^ z) b
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
⊢ ∀ {x y z : RayVector R M},
    SameRay R ↑((equiv R M) x) ↑((equiv R M) y) →
      SameRay R ↑((equiv R M) y) ↑((equiv R M) z) → SameRay R ↑((equiv R M) x) ↑((equiv R M) z)

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x : RayVector R M
⊢ ∀ {y z : RayVector R M},
    SameRay R ↑((equiv R M) x) ↑((equiv R M) y) →
      SameRay R ↑((equiv R M) y) ↑((equiv R M) z) → SameRay R ↑((equiv R M) x) ↑((equiv R M) z)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] V2
g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ f (v +ᵥ p) +ᵥ g (v +ᵥ p) = (f.linear + g.linear) v +ᵥ f p +ᵥ g p

Tactic:
by simp [vadd_vadd, add_right_comm]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddRightMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₀ ≤ p₁
⊢ Monotone ⇑(lineMap p₀ p₁)

Tactic:
intro x

Goal state after:
k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddRightMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₀ ≤ p₁
x : k
⊢ ∀ ⦃b : k⦄, x ≤ b → (lineMap p₀ p₁) x ≤ (lineMap p₀ p₁) b
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddLeftMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
⊢ Antitone ⇑(lineMap p₀ p₁)

Tactic:
intro x

Goal state after:
k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddLeftMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x : k
⊢ ∀ ⦃b : k⦄, x ≤ b → (lineMap p₀ p₁) b ≤ (lineMap p₀ p₁) x
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h✝ : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ r₂⁻¹ • r₂ • y = y

Tactic:
inv_smul_smul₀ hr₂.ne'

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h✝ : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ y = y
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : 0 ≤ 0
hab : a + 0 = 1
⊢ a • x + 0 • y ∈ s

Tactic:
rw [add_zero] at hab
    rwa [hab, zero_smul, one_smul, add_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ b • (y - x) + a • (-x + z) = 0

Tactic:
← neg_sub,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ b • -(x - y) + a • (-x + z) = 0
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 : Set P
p : P
v : V
hp : p ∈ spanPoints k s
hv : v ∈ vectorSpan k s
⊢ v +ᵥ p ∈ spanPoints k s

Tactic:
rcases hp with ⟨p₂, ⟨hp₂, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩

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 : Set P
p : P
v : V
hv : v ∈ vectorSpan k s
p₂ : P
hp₂ : p₂ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p = v₂ +ᵥ p₂
⊢ v +ᵥ p ∈ spanPoints k s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Tactic:
rw [hab, one_mul, zero_mul, add_zero] at hz

Goal state after:
case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : x ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ((fun x ↦ z + x) ⁻¹' s)

Tactic:
intro x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
⊢ x ∈ (fun x ↦ z + x) ⁻¹' s → StarConvex 𝕜 x ((fun x ↦ z + x) ⁻¹' s)