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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
l : Filter ι
ε : ι → 𝕜
f : ι → E
hε : Tendsto ε l (𝓝 0)
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f)
⊢ Tendsto (ε • f) l (𝓝 0)

Tactic:
← isLittleO_one_iff 𝕜

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
l : Filter ι
ε : ι → 𝕜
f : ι → E
hε : ε =o[l] fun _x ↦ 1
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f)
⊢ (ε • f) =o[l] fun _x ↦ 1
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case hab
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ≤ ↑⌈x⌉₊

Tactic:
exact Nat.le_ceil _

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

Goal state before:
pp: case e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
x : ℝ
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-(b * rexp x) + -c))

Tactic:
← neg_add (b * exp x) c,

Goal state after:
case e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
x : ℝ
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / -(b * rexp x + c))
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case e'_5
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ 𝓝 0 = 𝓝 (-0)

Tactic:
· rw [neg_zero]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖S.normedMk m‖ ≤ 1 * ‖m‖

Tactic:
by simp [norm_mk_le_norm]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ f m + f x = f m

Tactic:
(NormedAddGroupHom.mem_ker f x).mp hx,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ f m + 0 = f m
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2 ^ 2 - 2

pp: n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
· refine (sqrtTwoAddSeries_lt_two n).trans_le ?_
      norm_num

Goal state after:
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
h_add : Tendsto (fun x ↦ 1 + v a ^ x) atTop (𝓝 (1 + 0))
h_sub : Tendsto (fun x ↦ 1 - v a ^ x) atTop (𝓝 (1 - 0))
⊢ Tendsto ?m.137 atTop (𝓝 1)

Tactic:
by simpa using h_sub

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

Goal state before:
pp: x : ℝ
h0x : 0 ≤ x
hxp✝ : x ≤ π / 2
h✝ : 0 < x
hxp : x = π / 2
⊢ 0 ≤ tan x

Tactic:
by simp [hxp, tan_eq_sin_div_cos]

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
⊢ 0 < ↑r - δ

Tactic:
refine sub_pos_of_lt ?_

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
⊢ δ < ↑r
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } t ∈ F

Tactic:
simp only [Path.coe_mk_mk, piecewise]
    split_ifs <;> assumption

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
inst✝ : PathConnectedSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsPathConnected (f '' univ)

Tactic:
exact isPathConnected_univ.image hf

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

Goal state before:
pp: case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝ : PathConnectedSpace X
x : X
_x_in : x ∈ univ
hx : pathComponentIn univ x = univ
⊢ connectedComponent x = univ

Tactic:
rw [← univ_subset_iff]

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝ : PathConnectedSpace X
x : X
_x_in : x ∈ univ
hx : pathComponentIn univ x = univ
⊢ univ ⊆ connectedComponent x
Module: Mathlib.Topology.Instances.AddCircle.Real

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

Tactic:
intro x y hxy

Goal state after:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
⊢ x = y
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
⊢ ↑x.val / ↑N < 0 + 1

Tactic:
by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _

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
⊢ ↑y.val / ↑N < 0 + 1

Tactic:
by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _

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

Goal state before:
pp: case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = |p|⁻¹ * ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)

Goal state after:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inr.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ False

pp: case inr.inr.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ False

Tactic:
· have : ↑z * p ≤ -p := by nlinarith
        linarith [abs_eq_self.mpr hp.le]

Goal state after:
case inr.inr.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ log |x| = log x

Tactic:
by
  by_cases h : x = 0
  · simp [h]
  · rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]

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

Goal state before:
pp: case hf₁
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)
⊢ Tendsto (fun x ↦ ↑⌊x⌋₊) atTop (cobounded K)

pp: case hbdd
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)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖↑⌊x⌋₊ - x‖

Tactic:
· exact tendsto_natCast_atTop_cobounded.comp tendsto_nat_floor_atTop

Goal state after:
case hbdd
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)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖↑⌊x⌋₊ - x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑(↑n * (π * 2)) = 0

Tactic:
intCast_mul_eq_zsmul,

Goal state after:
case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ n • ↑(π * 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑(↑n * (π * 2)) + ↑ψ = ↑ψ

Tactic:
intCast_mul_eq_zsmul,

Goal state after:
case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ n • ↑(π * 2) + ↑ψ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
hx : ¬x = 0
⊢ (if x = 0 then if 1 = 0 then 1 else 0 else cexp (log x * 1)) = x

Tactic:
if_neg (one_ne_zero : (1 : ℂ) ≠ 0),

Goal state after:
x : ℂ
hx : ¬x = 0
⊢ (if x = 0 then 0 else cexp (log x * 1)) = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
· simp [hre, hre.le, hre.ne']

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

Goal state before:
pp: case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
· simp [hre, hre.le, hre.ne']

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

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1 else 0 else (cexp ((starRingEnd ℂ) (log x) * (starRingEnd ℂ) ((starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹

Tactic:
conj_conj

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else (cexp ((starRingEnd ℂ) (log x) * n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
⊢ (↑x✝ + ↑x✝¹).cos = (↑x✝).cos * (↑x✝¹).cos - (↑x✝).sin * (↑x✝¹).sin

Tactic:
exact Real.cos_add _ _

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

Goal state before:
pp: x n : ℂ
⊢ (x ^ n)⁻¹ =
    if x.arg = π then
      if x.arg = π then (x ^ (starRingEnd ℂ) ((starRingEnd ℂ) n))⁻¹ else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹
    else x⁻¹ ^ n

Tactic:
conj_conj

Goal state after:
x n : ℂ
⊢ (x ^ n)⁻¹ = if x.arg = π then if x.arg = π then (x ^ n)⁻¹ else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ ↑θ.toReal = θ

Tactic:
by
  induction θ using Real.Angle.induction_on
  exact coe_toIocMod _ _

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

Goal state before:
pp: x n : ℂ
hx : x.arg ≠ π
⊢ x ^ (starRingEnd ℂ) n = (starRingEnd ℂ) ((starRingEnd ℂ) (x ^ (starRingEnd ℂ) n))

Tactic:
conj_conj

Goal state after:
x n : ℂ
hx : x.arg ≠ π
⊢ x ^ (starRingEnd ℂ) n = x ^ (starRingEnd ℂ) n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
simp [hi, hi.ne.symm, hi.not_gt, arg_neg_eq_arg_sub_pi_of_im_pos, sub_eq_add_neg, ←
      add_eq_zero_iff_neg_eq, Real.pi_ne_zero]

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

Goal state before:
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_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr),
        Real.Angle.coe_zero, zero_add]

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (↑(rexp (log (-x) * y)) * (↑(cos (y * π)) + Complex.sin ↑(y * π) * Complex.I)).re = rexp (log x * y) * cos (y * π)

Tactic:
←
      Complex.ofReal_sin,

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (↑(rexp (log (-x) * y)) * (↑(cos (y * π)) + ↑(sin (y * π)) * Complex.I)).re = rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rcases two_nsmul_eq_zero_iff.mp h with h | h
  · simp_all [add_eq_zero_iff_eq_neg.mp h]
  rw [← coe_toReal θ, ← coe_toReal ψ, ← coe_add] at h
  suffices |θ.toReal + ψ.toReal| = π by grind [toReal_neg_iff_sign_neg, abs_add_eq_add_abs_iff]
  rw [abs_eq pi_nonneg]
  rcases angle_eq_iff_two_pi_dvd_sub.mp h with ⟨k, hk⟩
  rw [sub_eq_iff_eq_add] at hk
  have : k ∈ Finset.Icc (-1) 0 :=
    IsStrictOrderedRing.int_mem_Icc_of_mul_mem_Ioo two_pi_pos <| by grind [toReal_mem_Ioc]
  fin_cases this
  all_goals simp at hk; grind

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

Goal state before:
pp: x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ (log x)⁻¹ = rexp 1

Tactic:
rpow_def_of_pos hx₀,

Goal state after:
x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ rexp (log x * (log x)⁻¹) = rexp 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
· simp [rpow_add', ← H, h]

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

Goal state before:
pp: case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Tactic:
Real.zero_rpow hw,

Goal state after:
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 / rexp (arg 0 * w.im)
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'
⊢ (fun x ↦ ‖log x ^ r‖) ≤ᶠ[atTop] fun x ↦ log x ^ r'

Tactic:
filter_upwards [tendsto_log_atTop.eventually_ge_atTop 1] with x hx

Goal state after:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ ‖log x ^ r‖ ≤ log x ^ r'
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
simp_rw [← rpow_intCast, ← rpow_mul hx, mul_comm y]

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
⊢ x ^ (-z) < (y ^ z)⁻¹

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

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

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

Tactic:
← rpow_neg

Goal state after:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ x ^ (-z) < y ^ (-z)

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z
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
⊢ x ^ (-z) ≤ (y ^ z)⁻¹

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

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

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

Tactic:
← rpow_neg

Goal state after:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

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

case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case refine_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x ↦ ‖x.1‖ ^ x.2.re) (𝓝 (0, z)) (𝓝 0)

pp: case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 (0, z)) ((fun x ↦ ‖x‖) ∘ fun x ↦ rexp (-(x.1.arg * x.2.im)))

Tactic:
· convert!
    (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _)
      _ <;>
      simp [hz, Real.zero_rpow hz.ne']

Goal state after:
case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 (0, z)) ((fun x ↦ ‖x‖) ∘ fun x ↦ rexp (-(x.1.arg * x.2.im)))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x ↦ c * x ^ y) (𝓝 0) (𝓝 0)

Tactic:
convert! ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _
  · simp [hy]
  · exact Or.inr hc

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

Goal state before:
pp: case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
ih : ∏ i ∈ s✝, f i ^ r = (∏ i ∈ s✝, f i) ^ r
⊢ ∏ i ∈ insert a✝ s✝, f i ^ r = (∏ i ∈ insert a✝ s✝, f i) ^ r

Tactic:
simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

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

Goal state before:
pp: case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ x⁻¹ ^ y * x ^ y = 1

Tactic:
rw [← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0, ENNReal.inv_mul_cancel h0 h_top,
    one_rpow]

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

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

Tactic:
intro x y hxy

Goal state after:
z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x ↦ x ^ z) x < (fun x ↦ x ^ z) y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
log_rpow h1,

Goal state after:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |t * log x * x ^ t| < 1
⊢ |log x * x ^ t| * t < 1
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:
rw [← H, norm_one] at this

Goal state after:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : 1 ≤ 1 / 2
⊢ False
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
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y

Tactic:
exact zero_left _

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
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z

Tactic:
rcases eq_or_ne x 0 with (rfl | hx); · exact zero_left z
  rcases eq_or_ne z 0 with (rfl | hz); · exact zero_right x
  rcases eq_or_ne y 0 with (rfl | hy)
  · exact (hy rfl).elim (fun h => (hx h).elim) fun h => (hz h).elim
  rcases hxy.exists_pos hx hy with ⟨r₁, r₂, hr₁, hr₂, h₁⟩
  rcases hyz.exists_pos hy hz with ⟨r₃, r₄, hr₃, hr₄, h₂⟩
  refine Or.inr (Or.inr <| ⟨r₃ * r₁, r₂ * r₄, mul_pos hr₃ hr₁, mul_pos hr₂ hr₄, ?_⟩)
  rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: 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

Tactic:
rwa [add_zero]

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 d : k
⊢ (lineMap p₀ ((lineMap p₀ p₁) c)) d = (lineMap p₀ p₁) (d * c)

Tactic:
simp [lineMap_apply, mul_smul]

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 y hxy

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 y : k
hxy : x ≤ y
⊢ (lineMap p₀ p₁) x ≤ (lineMap p₀ p₁) y
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₁
x y : k
hxy : x ≤ y
⊢ (lineMap p₀ p₁) x ≤ (lineMap p₀ p₁) y

Tactic:
suffices x • (p₁ - p₀) ≤ y • (p₁ - p₀) by simpa [lineMap]

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 y : k
hxy : x ≤ y
⊢ x • (p₁ - p₀) ≤ y • (p₁ - p₀)
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 y hxy

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 y : k
hxy : x ≤ y
⊢ (lineMap p₀ p₁) y ≤ (lineMap p₀ p₁) x