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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
⊢ j ∈ s → C j * ‖B j x‖ ≤ sSup (C '' ↑s) * ‖B j x‖

Tactic:
hj

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ C j * ‖B j x‖ ≤ sSup (C '' ↑s) * ‖B j x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ C j ≤ sSup (C '' ↑s)

Tactic:
← s.sup'_eq_csSup_image hs,

Goal state after:
case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ C j ≤ s.sup' hs C
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
⊢ cexp (x - y) = cexp x / cexp y

Tactic:
simp [sub_eq_add_neg, exp_add, exp_neg, div_eq_mul_inv]

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

Goal state before:
pp: x y : ℝ
⊢ rexp (x - y) = rexp x / rexp y

Tactic:
simp [sub_eq_add_neg, exp_add, exp_neg, div_eq_mul_inv]

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

Goal state before:
pp: x : ℂ
⊢ tanh (-x) = -tanh x

Tactic:
simp [tanh, neg_div]

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
⊢ f =O[l] g ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x / g x‖

Tactic:
refine ⟨div_isBoundedUnder_of_isBigO, fun h => ?_⟩
  obtain ⟨c, hc⟩ := h
  simp only [eventually_map, norm_div] at hc
  refine IsBigO.of_bound c (hc.mp <| hgf.mono fun x hx₁ hx₂ => ?_)
  by_cases hgx : g x = 0
  · simp [hx₁ hgx, hgx]
  · exact (div_le_iff₀ (norm_pos_iff.2 hgx)).mp hx₂

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Tactic:
rcases h.exists_pos with ⟨C, C₀, hC⟩

Goal state after:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : IsBigOWith C cofinite f g''
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (2 * x) = 2 * cos x ^ 2 - 1

Tactic:
cos_two_mul',

Goal state after:
x : ℂ
⊢ cos x ^ 2 - sin x ^ 2 = 2 * cos x ^ 2 - 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: n : ℕ
z : ℂ
⊢ (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I

Tactic:
by
  rw [← exp_mul_I, ← exp_mul_I, ← exp_nat_mul, mul_assoc]

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

Goal state before:
pp: x : ℂ
⊢ ‖cexp x‖ ≤ Real.exp ‖x‖

Tactic:
convert norm_exp_sub_sum_le_exp_norm_sub_sum x 0

Goal state after:
case e'_3
x : ℂ
⊢ cexp x = cexp x - ∑ m ∈ range 0, x ^ m / ↑m.factorial

case e'_4
x : ℂ
⊢ Real.exp ‖x‖ = Real.exp ‖x‖ - ∑ m ∈ range 0, ‖x‖ ^ m / ↑m.factorial
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
rw [← ofReal_inj]; simp [sinh_three_mul]

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.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
⊢ j ≥ i → |f j - f i| < ε

Tactic:
hj

Goal state after:
α : 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.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
⊢ |f j - f i| < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ⟨rexp x, ⋯⟩) atTop atTop

Tactic:
by rw [tendsto_Ioi_atTop]; simp only [tendsto_exp_atTop]

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

Goal state before:
pp: x : ℝ
hl : -(π / 2) ≤ x
hu : x ≤ π / 2
⊢ cos x = √(1 - sin x ^ 2)

Tactic:
by
  rw [← abs_cos_eq_sqrt_one_sub_sin_sq, abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨hl, hu⟩)]

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

Goal state before:
pp: ⊢ comap re (comap Real.exp atTop) = comap re atTop

Tactic:
by rw [Real.comap_exp_atTop]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ infDist 1 {m | ↑m = ↑x} = infDist x ↑S

Tactic:
← infDist_image (IsometryEquiv.divLeft x).isometry,

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ infDist ((IsometryEquiv.divLeft x) 1) (⇑(IsometryEquiv.divLeft x) '' {m | ↑m = ↑x}) = infDist x ↑S
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 : 𝕜
s : Set E
⊢ ediam (c • s) = ‖c‖₊ • ediam s

Tactic:
refine le_antisymm (ediam_smul_le c s) ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
⊢ (fun n ↦ ↑n ^ k) =o[atTop] fun n ↦ r ^ n

Tactic:
by
  have : Tendsto (fun x : ℝ ↦ x ^ k) (𝓝[>] 1) (𝓝 1) :=
    ((continuous_id.pow k).tendsto' (1 : ℝ) 1 (one_pow _)).mono_left inf_le_left
  obtain ⟨r' : ℝ, hr' : r' ^ k < r, h1 : 1 < r'⟩ :=
    ((this.eventually (gt_mem_nhds hr)).and self_mem_nhdsWithin).exists
  have h0 : 0 ≤ r' := zero_le_one.trans h1.le
  suffices (fun n ↦ (n : R) ^ k : ℕ → R) =O[atTop] fun n : ℕ ↦ (r' ^ k) ^ n from
    this.trans_isLittleO (isLittleO_pow_pow_of_lt_left (pow_nonneg h0 _) hr')
  conv in (r' ^ _) ^ _ => rw [← pow_mul, mul_comm, pow_mul]
  suffices ∀ n : ℕ, ‖(n : R)‖ ≤ (r' - 1)⁻¹ * ‖(1 : R)‖ * ‖r' ^ n‖ from
    (isBigO_of_le' _ this).pow _
  intro n
  rw [mul_right_comm]
  refine n.norm_cast_le.trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))
  simpa [_root_.div_eq_inv_mul, Real.norm_eq_abs, abs_of_nonneg h0] using n.cast_le_pow_div_sub h1

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

Goal state before:
pp: k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
n : ℕ
hn : 1 ≤ n
⊢ n ∈ {x | (fun x ↦ 0 = (fun n ↦ ↑n ^ k * r ^ n) x) x}

Tactic:
by simp [zero_lt_one.trans_le hn |>.ne', h0]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun x ↦
    Function.uncurry (fun x y ↦ Function.uncurry (fun x_1 y ↦ (x x_1) y) y) ((Homeomorph.prodAssoc C(X, C(Y, Z)) X Y) x)

Tactic:
exact (continuous_fst.fst.eval continuous_fst.snd).eval continuous_snd

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

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

Tactic:
refine ⟨le_of_forall_le fun r hr ↦ ?_, ?_⟩

Goal state after:
case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ |x - ↑(round x)|

case refine_2
x : ℝ
⊢ ∀ (m : ℝ), ↑m = ↑x → |x - ↑(round x)| ≤ |m|
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
f : Y → Path x y
g : Y → Path y z
⊢ Continuous[inst✝, _] f → Continuous[inst✝, _] g → Continuous[inst✝, _] fun t ↦ (f t).trans (g t)

Tactic:
intro hf

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
hf : Continuous[inst✝, _] f
⊢ Continuous[inst✝, _] g → Continuous[inst✝, _] fun t ↦ (f t).trans (g t)
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(1 / 2) ≤ p⁻¹ * x

Tactic:
le_inv_mul_iff₀ hp,

Goal state after:
case inr.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p * -(1 / 2) ≤ 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
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄ : t₀ ≤ t₁
⊢ t₁ < 0

Tactic:
simpa using h₂

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

Goal state before:
pp: case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ Real.cos (Real.arcsin (x.im / ‖x‖)) = x.re / ‖x‖

Tactic:
rw [Real.cos_arcsin]

Goal state after:
case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ √(1 - (x.im / ‖x‖) ^ 2) = x.re / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ ‖z‖ = 1 ↔ ∃ θ, cexp (↑θ * I) = z

Tactic:
refine ⟨fun hz => ⟨arg z, ?_⟩, ?_⟩
  · calc
      exp (arg z * I) = ‖z‖ * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
      _ = z := norm_mul_exp_arg_mul_I z
  · rintro ⟨θ, rfl⟩
    exact Complex.norm_exp_ofReal_mul_I θ

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < Real.cos (θ + π)

Tactic:
refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩

Goal state after:
case refine_1
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ -(π / 2) < θ + π

case refine_2
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ θ + π < π / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range n, (-1) ^ i * f i| ≤ f n

Tactic:
by
  obtain h := hfs.tendsto_alternating_series_tsum
  have upper := hfa.alternating_series_le_tendsto h
  have lower := hfa.tendsto_le_alternating_series h
  have I (n : ℕ) : 0 ≤ f n := by
    apply le_of_tendsto hfs.tendsto_atTop_zero
    filter_upwards [Ici_mem_atTop n] with m hm using hfa hm
  obtain (h | h) := even_or_odd n
  · obtain ⟨n, rfl⟩ := even_iff_exists_two_mul.mp h
    specialize upper n
    specialize lower n
    simp only [sum_range_succ, even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul] at lower
    rw [abs_sub_le_iff]
    constructor
    · rwa [sub_le_iff_le_add, add_comm]
    · rw [sub_le_iff_le_add, add_comm]
      exact upper.trans (le_add_of_nonneg_right (I (2 * n)))
  · obtain ⟨n, rfl⟩ := odd_iff_exists_bit1.mp h
    specialize upper (n + 1)
    specialize lower n
    rw [Nat.mul_add, Finset.sum_range_succ] at upper
    rw [abs_sub_le_iff]
    constructor
    · rw [sub_le_iff_le_add, add_comm]
      exact lower.trans (le_add_of_nonneg_right (I (2 * n + 1)))
    · simpa [Finset.sum_range_succ, add_comm, pow_add] using upper

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

Goal state before:
pp: θ : Angle
⊢ 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
← not_or,

Goal state after:
θ : Angle
⊢ 2 • θ ≠ 0 ↔ ¬(θ = 0 ∨ θ = ↑π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
← not_or,

Goal state after:
θ : Angle
⊢ θ ≠ -θ ↔ ¬(θ = 0 ∨ θ = ↑π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
← not_or,

Goal state after:
θ : Angle
⊢ -θ ≠ θ ↔ ¬(θ = 0 ∨ θ = ↑π)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]
  exact Real.log_neg_natCast_nonneg _

Goal state after:
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
⊢ 1 < ↑n / ↑d

Tactic:
simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h)

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

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
exact (Real.neg_pi_div_two_le_arcsin _).trans (le_add_of_nonneg_right Real.pi_pos.le)

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

Goal state before:
pp: θ : Angle
⊢ θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
← not_or,

Goal state after:
θ : Angle
⊢ θ.sin ≠ 0 ↔ ¬(θ = 0 ∨ θ = ↑π)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
x : ℂ
hi : x.im = 0
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re

Tactic:
rw [(ext rfl hi : x = x.re)]
    rcases lt_trichotomy x.re 0 with (hr | hr | hr)
    · rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
      simp [hr.not_gt, ← two_mul, Real.pi_ne_zero]
    · simp [hr, Real.pi_ne_zero.symm]
    · rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
      simp [hr]

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

Goal state before:
pp: case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

pp: case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

pp: case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Tactic:
· rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le, ←
        Real.Angle.coe_add, ← two_mul, Real.Angle.coe_two_pi, Real.Angle.coe_zero]

Goal state after:
case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
← not_or,

Goal state after:
θ : Angle
⊢ θ.sign ≠ 0 ↔ ¬(θ = 0 ∨ θ = ↑π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
sign_two_nsmul_eq_neg_sign_iff

Goal state after:
θ : Angle
⊢ θ = 0 ∨ π / 2 < |θ.toReal| ↔ θ = 0 ∨ π / 2 < |θ.toReal|
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
⊢ rexp 1 ^ n = rexp ↑n

Tactic:
← rpow_natCast,

Goal state after:
n : ℕ
⊢ rexp 1 ^ ↑n = rexp ↑n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
· rw [abs_of_neg hx, rpow_def_of_neg hx, rpow_def_of_pos (neg_pos.2 hx), log_neg_eq_log, abs_mul,
      abs_of_pos (exp_pos _)]
    exact mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _)

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

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

Tactic:
rw [zero_add, rpow_zero, one_mul]

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

Goal state before:
pp: case empty
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
h : ∀ x ∈ ∅, 0 ≤ f x
⊢ a ^ 0 = 1

Tactic:
rpow_zero

Goal state after:
case empty
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
h : ∀ x ∈ ∅, 0 ≤ f x
⊢ 1 = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ n) ^ y

Tactic:
← rpow_natCast,

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ (x ^ y) ^ ↑n = (x ^ ↑n) ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
⊢ 0 < x ^ 0

Tactic:
rpow_zero

Goal state after:
x : ℝ≥0
⊢ 0 < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℝ
⊢ x ^ y = rexp (y * log x)

Tactic:
← exp_log hx,

Goal state after:
x : ℝ
hx : 0 < x
y : ℝ
⊢ rexp (log x) ^ y = rexp (y * log (rexp (log x)))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
← rpow_natCast,

Goal state after:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ ↑n) ^ (↑n)⁻¹ = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
← rpow_natCast,

Goal state after:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ ↑n = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: p : ℝ × ℝ
hp : p.1 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p

Tactic:
by
  rw [ne_iff_lt_or_gt] at hp
  cases hp with
  | inl hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
    refine ContinuousAt.mul ?_ (by fun_prop)
    · refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
      exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt
  | inr hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
    refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
    refine (continuousAt_log ?_).comp continuous_fst.continuousAt
    exact hp.ne'

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

Goal state before:
pp: case inl
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (x, y)

Tactic:
exact continuousAt_rpow_of_ne (x, y) hx

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

Goal state before:
pp: case inr
x : ℝ
⊢ ContinuousAt (fun x ↦ x ^ 0) x

Tactic:
rpow_zero

Goal state after:
case inr
x : ℝ
⊢ ContinuousAt (fun x ↦ 1) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
⊢ 0 < x ^ 0

Tactic:
rpow_zero

Goal state after:
x : ℝ≥0∞
⊢ 0 < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1 ^ z

Tactic:
exact rpow_lt_rpow hx1 hx2 hz

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

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
by
  rw [sub_eq_add_neg, rpow_add _ _ hx h'x, rpow_neg, div_eq_mul_inv]

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

Goal state before:
pp: case e'_5
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ (fun a ↦ a ^ y) ∘ ofNNReal = ofNNReal ∘ fun z ↦ z ^ y

Tactic:
ext1 x

Goal state after:
case e'_5
y : ℝ
h : 0 < y
x✝ x : ℝ≥0
⊢ ((fun a ↦ a ^ y) ∘ ofNNReal) x = (ofNNReal ∘ fun z ↦ z ^ y) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x : ℝ
h : 0 ≤ x
⊢ x = (x ^ (1 / 2)) ^ 2

Tactic:
← rpow_natCast,

Goal state after:
case inl
x : ℝ
h : 0 ≤ x
⊢ x = (x ^ (1 / 2)) ^ ↑2
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
← rpow_natCast,

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ ↑n) ^ (↑n)⁻¹ = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
← rpow_natCast,

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ (↑n)⁻¹) ^ ↑n = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: 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
⊢ ↑k ^ (↑d)⁻¹ = ↑r

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:
← hr,

Goal state after:
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
⊢ ↑(r ^ d) ^ (↑d)⁻¹ = ↑r

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
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: 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
⊢ ↑k ^ (↑d)⁻¹ = ↑r

Tactic:
← hr,

Goal state after:
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
⊢ ↑(r ^ d) ^ (↑d)⁻¹ = ↑r
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✝² : ZeroLEOneClass β
inst✝¹ : Nontrivial β
inst✝ : SMulPosStrictMono α β
a : α
ha : 0 < a
⊢ 0 < (algebraMap α β) a

Tactic:
by
  simpa using algebraMap_strictMono β ha

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr
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
⊢ SameRay R (x + y) z

Tactic:
rcases eq_or_ne y 0 with (rfl | hy₀)

Goal state after:
case inr.inl
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 z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
⊢ SameRay R (x + 0) z

case inr.inr
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
⊢ SameRay R (x + y) z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ SameRay R (-x) y ↔ SameRay R x (-y)

Tactic:
by rw [← sameRay_neg_iff, neg_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0

Tactic:
refine h.resolve_left (ne_of_gt <| sub_pos.2 ?_)

Goal state after:
case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ r₂ * r < r₁