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

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
⊢ (g x = 0 → f x = 0) → ‖f x‖ ≤ C * ‖g x‖

Tactic:
h

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h✝ : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
h : g x = 0 → f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by rw [← neg_sub, cosh_sub_sinh]

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

Goal state before:
pp: n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |rexp x - ?b✝| + |?b✝ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

pp: case b
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ ℝ

Tactic:
h

Goal state after:
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |x| ^ m / ↑m.factorial * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
rm : ℝ
er : ↑m = rm
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)
⊢ |rexp x - expNear n x a| ≤ |x| ^ n / ↑n.factorial * b

Tactic:
subst er
  exact exp_approx_succ _ e₁ _ _ (by simpa using e) (exp_approx_end _ _ _ e₁ h)

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

Goal state before:
pp: case inl
t : ℝ
ht' : t ≤ ↑0
⊢ t ≤ 0

Tactic:
Nat.cast_zero

Goal state after:
case inl
t : ℝ
ht' : t ≤ 0
⊢ t ≤ 0
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 • ε
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε

Tactic:
have h : ∃ l, ∀ n ≥ m, a - l • ε < f n :=
    ⟨k + k + 1, fun n hnm ↦
      lt_of_lt_of_le (show a - (k + (k + 1)) • ε < -|f n| from
          lt_neg.1 <| (ham n hnm).trans_lt
              (by
                rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
                exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))))
        (neg_le.2 <| abs_neg (f n) ▸ le_abs_self _)⟩

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
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
⊢ 0 < b' → Tendsto (fun x ↦ x ^ n / (b' * rexp x + c')) atTop (𝓝 0)

Tactic:
h

Goal state after:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Tendsto (fun x ↦ x ^ n / (b' * rexp x + c')) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
h₀ : 0 < 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
⊢ f = 0

Tactic:
by
        ext n
        simpa using H n

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

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

Tactic:
rw [← hn, cos_int_mul_two_pi_add_pi] at h

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ ↑S.topologicalClosure

Tactic:
h

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ univ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n = (sin (π / 2 ^ (n + 2)) * 2) ^ 2

pp: case hx
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

pp: case hy
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2

Tactic:
mul_pow,

Goal state after:
n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n = sin (π / 2 ^ (n + 2)) ^ 2 * 2 ^ 2

case hx
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

case hy
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: k : ℕ
r : ℝ
hr : |r| < 1
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)

Tactic:
by_cases h0 : r = 0

Goal state after:
case pos
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)

case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
n : ℕ
hn : 1 ≤ n
⊢ ‖x ^ n‖ = ‖x‖ ^ n

Tactic:
induction n, hn using Nat.le_induction with

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

Goal state before:
pp: case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ c < 0

Tactic:
h

Goal state after:
case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ (- -2 - 2 * √5) / (2 * 4) < 0
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1

Tactic:
geom_series_mul_shift x h,

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ i + ∑' (i : ℕ), x ^ (i + 1) = 2 * ∑' (i : ℕ), x ^ i - 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝[>] 0)

Tactic:
by
  apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
  · convert! continuous_cos.continuousWithinAt.tendsto
    simp
  · filter_upwards [Ioo_mem_nhdsLT (neg_lt_self pi_div_two_pos)] with x hx
    exact cos_pos_of_mem_Ioo hx

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

Goal state before:
pp: ⊢ sin ↑π = 0

Tactic:
← ofReal_sin,

Goal state after:
⊢ ↑(Real.sin π) = 0
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ↑((n + k).descFactorial k) * r ^ n

Tactic:
by
  convert! (summable_choose_mul_geometric_of_norm_lt_one k hr).mul_left (k.factorial : R) using
    2 with n
  simp [← mul_assoc, descFactorial_eq_factorial_mul_choose (n + k) k]

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ ‖∑ x ∈ Finset.range n, f x - a‖ ≤ C * r ^ n / (1 - r)

Tactic:
rw [← dist_eq_norm]
  apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf)
  exact ha.tendsto_sum_nat

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

Goal state before:
pp: M : Type u_4
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l l' : List M
h : List.Forall₂ Joined l l'
⊢ Joined l.prod l'.prod

Tactic:
induction h with

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

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

Tactic:
rw [← hf.specializes_iff, hγ', γ.source]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : R0Space Y
f g : C(X, Y)
h : f ⤳ g
⊢ g ⤳ f

Tactic:
rw [← specializes_coe] at h ⊢

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : R0Space Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
⊢ ⇑g ⤳ ⇑f
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inr.inr.inr.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 : p < 0
hz' : ↑z ≤ -1
⊢ False

Tactic:
have : -p ≤ ↑z * p := by nlinarith

Goal state after:
case inr.inr.inr.inr.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 : p < 0
hz' : ↑z ≤ -1
this : -p ≤ ↑z * p
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : √(1 - x ^ 2) = 0
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

Tactic:
h

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

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

Tactic:
h

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : √(1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Tactic:
have := arg_mul_cos_add_sin_mul_I (norm_pos_iff.mpr hz) hN

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
this : (↑‖z‖ * (cos ↑(z.arg + ↑N * (2 * π)) + sin ↑(z.arg + ↑N * (2 * π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ (↑‖z‖ * (cos ↑z.arg + sin ↑z.arg * I)).re ∧ (↑‖z‖ * (cos ↑z.arg + sin ↑z.arg * I)).im = 0

Tactic:
h

Goal state after:
case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).re ∧ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).im = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ (↑‖z‖ * (cos ↑z.arg + sin ↑z.arg * I)).re < 0 ∧ (↑‖z‖ * (cos ↑z.arg + sin ↑z.arg * I)).im = 0

Tactic:
h

Goal state after:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ (↑‖z‖ * (cos ↑π + sin ↑π * I)).re < 0 ∧ (↑‖z‖ * (cos ↑π + sin ↑π * I)).im = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ (↑‖z‖ * (cos ↑z.arg + sin ↑z.arg * I)).re = 0 ∧ 0 < (↑‖z‖ * (cos ↑z.arg + sin ↑z.arg * I)).im

Tactic:
h

Goal state after:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).re = 0 ∧ 0 < (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).im
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ cexp ↑(Real.log ‖x‖) * (cos ↑x.arg + sin ↑x.arg * I) = x

Tactic:
← ofReal_sin,

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ cexp ↑(Real.log ‖x‖) * (cos ↑x.arg + ↑(Real.sin x.arg) * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ (↑‖z‖ * (cos ↑z.arg + sin ↑z.arg * I)).re = 0 ∧ (↑‖z‖ * (cos ↑z.arg + sin ↑z.arg * I)).im < 0

Tactic:
h

Goal state after:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).re = 0 ∧ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).im < 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: ⊢ Continuous fun x ↦ expOrderIso.symm ⟨|↑x|, ⋯⟩

Tactic:
exact expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)

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

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

Tactic:
h

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

Goal state before:
pp: case inr
z : ℂ
hre : z.re < 0
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0

Tactic:
simp only [hre.not_ge, false_or]

Goal state after:
case inr
z : ℂ
hre : z.re < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

Tactic:
simp only [hre.not_ge, false_or]

Goal state after:
case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬z.arg = π / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
arg_eq_pi_div_two_iff

Goal state after:
z : ℂ
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re

Tactic:
abs_le,

Goal state after:
z : ℂ
⊢ -(π / 2) ≤ z.arg ∧ z.arg ≤ π / 2 ↔ 0 ≤ z.re
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 ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1⁻¹ else 0⁻¹ else (cexp (log x * n))⁻¹

Tactic:
inv_one,

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 ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) 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: θ ψ : Angle
⊢ θ.toReal = ψ.toReal → θ = ψ

Tactic:
h

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

Goal state before:
pp: ⊢ ↑π ≠ 0

Tactic:
rw [← toReal_injective.ne_iff, toReal_pi, toReal_zero]
  exact Real.pi_ne_zero

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

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

Tactic:
simp [hr, Real.pi_ne_zero.symm]

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

Goal state before:
pp: θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)

Tactic:
Set.mem_Ioc

Goal state after:
θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
Set.mem_Ioc

Goal state after:
θ : Angle
⊢ π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π ↔ π / 2 < θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
Set.mem_Ioc

Goal state after:
θ : Angle
⊢ -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π

Tactic:
Function.update_eq_iff

Goal state after:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ↑π = ↑(arg 0) + ↑π ∧ ∀ (x : ℂ), x ≠ 0 → ((Real.Angle.coe ∘ arg) ∘ Neg.neg) x = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ SignType.sign 1 = 1

Tactic:
sign_one

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

Goal state before:
pp: ⊢ -SignType.sign 1 = -1

Tactic:
sign_one

Goal state after:
⊢ -1 = -1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0

Tactic:
h

Goal state after:
w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ w ≠ 0
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)
a✝ : ℕ
⊢ a✝ ≠ 0 → ↑a✝ ^ r = 0 → ‖g a✝‖ = 0

Tactic:
h

Goal state after:
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
a✝ : ℕ
h : a✝ ≠ 0
⊢ ↑a✝ ^ r = 0 → ‖g a✝‖ = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case h
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0

Tactic:
h

Goal state after:
case h
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ w ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
refine squeeze_zero (fun _ => norm_nonneg _) (fun _ => norm_cpow_le _ _) ?_

Goal state after:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x ↦ ‖x.1‖ ^ x.2.re / rexp (x.1.arg * x.2.im)) (𝓝 (0, z)) (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
rw [rpow_def_of_pos hx, one_lt_exp_iff, mul_pos_iff, log_pos_iff hx.le, log_neg_iff hx]

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

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

Tactic:
nth_rw 2 [← ENNReal.rpow_one x]
  exact ENNReal.rpow_le_rpow_of_exponent_ge hx h_one_le

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

Goal state before:
pp: case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 < ↑x✝
⊢ ↑x✝ ^ z < 1

Tactic:
· simp only [one_lt_coe_iff] at hx
    simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)),
      NNReal.rpow_lt_one_of_one_lt_of_neg hx hz]

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
x✝ : ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ f (r₁ • x) = f (r₂ • y)

Tactic:
h

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
x y : M
f : M →ₗ[R] N
h✝ : SameRay R x y
x✝ : ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ f (r₂ • y) = f (r₂ • y)
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 : RayVector R M
⊢ ∀ {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:
z

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 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
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
f g : P1 →ᵃ[k] P2
h : f = g
⊢ f default = g default

Tactic:
h

Goal state after:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
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
f g : P1 →ᵃ[k] P2
h : f = g
⊢ g default = g default
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : x + x = y + y
⊢ x = y

Tactic:
← two_smul k x,

Goal state after:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : 2 • x = y + y
⊢ x = y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddRightMono 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : ZeroLEOneClass 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = z

Tactic:
h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddRightMono 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : ZeroLEOneClass 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = x