mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ PathConnectedSpace X ↔ IsPathConnected univ

Tactic:
by
  simp [pathConnectedSpace_iff, isPathConnected_iff, nonempty_iff_univ_nonempty]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
⊢ 0 < ‖w‖ ^ n

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ?m.62 ≤ ↑x.val / ↑N

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ 0 ≤ ↑y.val / ↑N

Tactic:
positivity

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

Goal state before:
pp: case inr.inr.refine_2
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)

Tactic:
exact ⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩

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

Goal state before:
pp: α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x‖ * ‖g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ 0 < ‖f x‖

Tactic:
positivity

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

Goal state before:
pp: ⊢ rexp (log 1) = rexp 0

Tactic:
rw [exp_log zero_lt_one, exp_zero]

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

Goal state before:
pp: x : ℝ
⊢ log (x / x) = 0

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0 <;> simp [*]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ (x / x).arg = 0

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0 <;> simp [*]

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

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ ∀ᶠ (x : K) in atTop, |↑⌊x⌋₊ - x| ≤ |1|

Tactic:
simpa using ⟨0, fun _ h ↦ mod_cast Nat.abs_floor_sub_le h⟩

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

Goal state before:
pp: n : ℕ
hn : n = 0
⊢ 0 ≤ log ↑n

Tactic:
simp [hn]

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) < 1 / x
⊢ |log x * x| < 1

Tactic:
rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff₀ h1] at this

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ |log x * x| < 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ 2 * x / (x + 2)

Tactic:
positivity

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

Goal state before:
pp: θ : ℝ
⊢ ↑(2 • (θ / 2)) = ↑θ

Tactic:
two_zsmul,

Goal state after:
θ : ℝ
⊢ ↑(θ / 2 + θ / 2) = ↑θ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < 2 * x / (x + 2)

Tactic:
positivity

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

Goal state before:
pp: ⊢ 2 • ↑(-π / 2) = ↑π

Tactic:
two_zsmul,

Goal state after:
⊢ ↑(-π / 2) + ↑(-π / 2) = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
two_zsmul,

Goal state after:
θ : Angle
⊢ θ + θ = 0 ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℤ
hn : x = ↑n * (2 * ↑π * I)
this : 0 ≤ ↑n * (2 * π)
⊢ 0 < 2 * π

Tactic:
positivity

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

Goal state before:
pp: θ : Angle
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
two_zsmul,

Goal state after:
θ : Angle
⊢ θ + θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x y : ℂ
h : cexp x = cexp y
n : ℤ
hn : x = y + ↑n * (2 * ↑π * I)
⊢ x.re = y.re

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case mp.refine_1
θ : ℝ
⊢ toIocMod ⋯ (-π) θ ∈ Ioc (-π) π

Tactic:
convert! toIocMod_mem_Ioc _ _ _

Goal state after:
case e'_4.e'_4
θ : ℝ
⊢ π = -π + 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
⊢ x = x ^ 2⁻¹ * x ^ 2⁻¹

Tactic:
by simp [← sq]

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.sin| = |ψ.sin|

Tactic:
rw [two_nsmul_eq_iff] at h

Goal state after:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.sin| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.sin| = |ψ.sin|

Tactic:
two_zsmul,

Goal state after:
θ ψ : Angle
h : θ + θ = ψ + ψ
⊢ |θ.sin| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.cos| = |ψ.cos|

Tactic:
rw [two_nsmul_eq_iff] at h

Goal state after:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.cos| = |ψ.cos|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.cos| = |ψ.cos|

Tactic:
two_zsmul,

Goal state after:
θ ψ : Angle
h : θ + θ = ψ + ψ
⊢ |θ.cos| = |ψ.cos|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)

Tactic:
two_zsmul,

Goal state after:
θ : Angle
⊢ (θ + θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
two_zsmul,

Goal state after:
θ : Angle
⊢ (θ + θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
two_zsmul,

Goal state after:
θ : Angle
⊢ (θ + θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ 0 < π / 2

Tactic:
positivity

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

Goal state before:
pp: θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
⊢ 2 • θ = 2 • ψ ↔ θ = ψ

Tactic:
two_zsmul,

Goal state after:
θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
⊢ θ + θ = ψ + ψ ↔ θ = ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
two_zsmul,

Goal state after:
θ ψ : Angle
h : θ + θ + (ψ + ψ) = ↑π
⊢ |θ.cos| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ IsOpen fun y ↦ y.re < 0 ∧ y.im < 0

Tactic:
exact
    IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_im continuous_zero)

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

Goal state before:
pp: ⊢ Real.tan π = 0

Tactic:
Real.tan_pi

Goal state after:
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ θ.tan = ψ.tan

Tactic:
rw [two_nsmul_eq_iff] at h

Goal state after:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ θ.tan = ψ.tan
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
ψ : Angle
⊢ (ψ + ↑π).tan = ψ.tan

Tactic:
exact tan_add_pi _

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ θ.tan = ψ.tan

Tactic:
two_zsmul,

Goal state after:
θ ψ : Angle
h : θ + θ = ψ + ψ
⊢ θ.tan = ψ.tan
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan x✝ = (Real.tan x✝¹)⁻¹

Tactic:
← tan_pi_div_two_sub,

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan x✝ = Real.tan (π / 2 - x✝¹)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
two_zsmul,

Goal state after:
θ ψ : Angle
h : θ + θ + (ψ + ψ) = ↑π
⊢ ψ.tan = θ.tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2

Tactic:
two_zsmul,

Goal state after:
θ : Angle
⊢ (θ + θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|

Tactic:
two_zsmul,

Goal state after:
θ : Angle
⊢ (θ + θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ 0 < b

Tactic:
positivity

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

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ 0 < b

Tactic:
positivity

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

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ 0 ≤ b

Tactic:
positivity

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

Goal state before:
pp: θ ψ : Angle
h : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
two_zsmul,

Goal state after:
θ ψ : Angle
h : θ + ψ + (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ |θ.toReal| + |ψ.toReal| = π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
· simp [rpow_add pos]

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

Goal state before:
pp: case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ ↑(rexp (↑y * log x).re) * (↑(Real.cos (↑y * log x).im) + ↑(Real.sin (↑y * log x).im) * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
re_ofReal_mul,

Goal state after:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ ↑(rexp (y * (log x).re)) * (↑(Real.cos (↑y * log x).im) + ↑(Real.sin (↑y * log x).im) * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case refine_1
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 < c ^ r⁻¹

Tactic:
positivity

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

Goal state before:
pp: case refine_2
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 ≤ c ^ r⁻¹

Tactic:
positivity

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

Goal state before:
pp: case refine_3
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 ≤ r

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
n : ℕ
⊢ 0 ≤ ↑n ^ r

Tactic:
positivity

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

Goal state before:
pp: k : ℕ
b : ℝ
hb : 0 < b
⊢ (fun x ↦ x ^ k) =o[atTop] fun x ↦ rexp (b * x)

Tactic:
by
  simpa using isLittleO_zpow_exp_pos_mul_atTop k hb

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

Goal state before:
pp: s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ 0 ≤ log x ^ r

Tactic:
positivity

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

Goal state before:
pp: case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

Tactic:
positivity

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

Goal state before:
pp: case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
positivity

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

Goal state before:
pp: a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ x ^ b = cexp (Complex.log x * b)

Tactic:
rw [cpow_def_of_ne_zero hx]

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

Goal state before:
pp: a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
simp only [rpow_def]
  refine Complex.continuous_re.continuousAt.comp ?_
  refine (continuousAt_const_cpow ?_).comp Complex.continuous_ofReal.continuousAt
  norm_cast

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

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map f l).prod ^ r

Tactic:
by
  rw [← list_prod_map_rpow, List.map_map]; rfl

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

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

Tactic:
positivity

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

Goal state before:
pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ y

Tactic:
positivity

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

Goal state before:
pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

Tactic:
positivity

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

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

Tactic:
positivity

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

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

Tactic:
positivity

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

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

Tactic:
positivity

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

Goal state before:
pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

Tactic:
positivity

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

Goal state before:
pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

Tactic:
positivity

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

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

Tactic:
positivity

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

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

Tactic:
positivity

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

Goal state before:
pp: case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ y

Tactic:
positivity

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

Goal state before:
pp: case hy
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ z ≠ 0

Tactic:
positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ y ^ z⁻¹

Tactic:
positivity

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

Goal state before:
pp: case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ x

Tactic:
positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ x ^ z⁻¹

Tactic:
positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ y

Tactic:
positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < y ^ z⁻¹

Tactic:
positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ x

Tactic:
positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < x ^ z⁻¹

Tactic:
positivity

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

Goal state before:
pp: case pos
y : ℝ
h✝ : 0 < y
⊢ 0 * 0 = 0

pp: case pos
y : ℝ
h✝¹ : ¬0 < y
h✝ : y = 0
⊢ 1 * 1 = 1

pp: case neg
y : ℝ
h✝¹ : ¬0 < y
h✝ : ¬y = 0
⊢ ∞ * ∞ = ∞

Tactic:
exacts [zero_mul _, one_mul _, top_mul_top]

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

Goal state before:
pp: x : ℝ
⊢ ↑1 ^ x = ↑1

Tactic:
← coe_rpow_of_ne_zero one_ne_zero

Goal state after:
x : ℝ
⊢ ↑(1 ^ x) = ↑1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
hy : 0 < y
⊢ x ^ y = 0 ↔ x = 0

Tactic:
simp [hy, hy.not_gt]

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

Goal state before:
pp: x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ 0 ≤ ↑p.1 ^ p.2

Tactic:
positivity

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

Goal state before:
pp: x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ 0 ≤ 1 / ↑n

Tactic:
positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ x ^ z⁻¹

Tactic:
positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ y ^ z⁻¹

Tactic:
positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
h : x ^ z ≤ y
⊢ 0 < x ^ z

Tactic:
positivity

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

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

Tactic:
positivity

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

Goal state before:
pp: x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
⊢ log x ≤ x ^ ε / ε

Tactic:
by
  rcases hx.eq_or_lt with rfl | h
  · rw [log_zero, zero_rpow hε.ne', zero_div]
  rw [le_div_iff₀' hε]
  exact (log_rpow h ε).symm.trans_le <| (log_le_sub_one_of_pos <| rpow_pos_of_pos h ε).trans
    (sub_one_lt _).le

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

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ 2 ^ (-s).re ≤ 2 ^ (-1)

Tactic:
exact Real.rpow_le_rpow_of_exponent_le one_le_two <| (neg_lt_neg hs).le

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

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx coe_lt_top)

Goal state after:
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : ↑x ≤ 1
⊢ ↑x ^ z ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < ↑(↑n ^ x)

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ ↑n ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑r

Tactic:
positivity

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

Goal state before:
pp: case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑m

Tactic:
positivity

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

Goal state before:
pp: case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : Semiring β
inst✝³ : PartialOrder β
inst✝² : Algebra α β
inst✝¹ : IsOrderedRing β
inst✝ : SMulPosMono α β
a : α
ha : 0 ≤ a
⊢ 0 ≤ (algebraMap α β) a

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : Semiring β
inst✝³ : PartialOrder β
inst✝² : Algebra α β
inst✝¹ : IsOrderedRing β
inst✝ : SMulPosMono α β
a : α
ha : 0 < a
⊢ 0 ≤ (algebraMap α β) a

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : Semiring β
inst✝³ : PartialOrder β
inst✝² : Algebra α β
inst✝¹ : IsStrictOrderedRing β
inst✝ : SMulPosStrictMono α β
a : α
ha : 0 < a
⊢ 0 < (algebraMap α β) a

Tactic:
positivity

Goal state after:
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
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
⊢ f y = 0

Tactic:
rw [hy, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inr.refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ 0 < ry * rz₁ + rx * rz₂

Tactic:
positivity

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
hc₂ : c₂ ≠ 0
hpos : 0 < c₁ * c₂
h₁ : c₁ < 0
h₂ : c₂ < 0
⊢ SameRay R (c₁ • v) (c₂ • v)

Tactic:
· exact Or.inr (Or.inr ⟨-c₂, -c₁, neg_pos.2 h₂, neg_pos.2 h₁, by module⟩)

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ p₀ -ᵥ (lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)

Tactic:
rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]

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

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c : P1
r₁ r₂ : k
⊢ homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂

Tactic:
by
  simp only [homothety_def, add_smul, vadd_vadd]

Goal state after: