mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (x * I) = cosh x

Tactic:
by rw [← cosh_mul_I]; ring_nf; simp

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
⊢ (fun x ↦ x ^ n) =o[𝓝 0] fun x ↦ x

Tactic:
convert! isLittleO_pow_pow h (𝕜 := 𝕜)
  simp only [pow_one]

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

Goal state before:
pp: x : ℝ
hx : 0 < cos x
⊢ (√(1 + tan x ^ 2))⁻¹ = cos x

Tactic:
← sqrt_sq hx.le,

Goal state after:
x : ℝ
hx : 0 < cos x
⊢ (√(1 + tan x ^ 2))⁻¹ = √(cos x ^ 2)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ x ^ 2

Tactic:
← sq_abs

Goal state after:
x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ |x| ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖2 * Real.sin (x / 2)‖

Tactic:
show ‖2 * Real.sin (x / 2)‖ = ‖2 * sin (x / 2)‖ by norm_cast,

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖2 * sin (↑x / 2)‖
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 - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
grw [abs_sub_le, h]
  subst e₁; rw [expNear_succ, expNear_sub, abs_mul]
  convert!
    mul_le_mul_of_nonneg_left (a := |x| ^ n / ↑(Nat.factorial n)) (le_sub_iff_add_le'.1 e) ?_
      using 1
  · simp [mul_add, pow_succ', div_eq_mul_inv, abs_mul, abs_inv, Nat.factorial]
    ac_rfl
  · simp [div_nonneg, abs_nonneg]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ / sInf (Norm.norm '' f '' s) * ‖f x‖

Tactic:
rw [mul_comm_div]

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' f '' s))
Module: Mathlib.Analysis.SpecialFunctions.Exp

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

Tactic:
intro b' c' 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.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin ((π + π) / 2) = 0

Tactic:
add_div,

Goal state after:
⊢ sin (π / 2 + π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 π
⊢ 0 ≤ sin x

Tactic:
← closure_Ioo pi_ne_zero.symm

Goal state after:
x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2) = 1 ∨ sin (π / 2) = -1

Tactic:
by
    simpa [sq, mul_self_eq_one_iff] using sin_sq_add_cos_sq (π / 2)

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

Goal state before:
pp: x : ℝ
hl : -π ≤ x
hr : x ≤ π
this : 0 ≤ cos (x / 2)
⊢ √(1 / 2 + cos (2 * (x / 2)) / 2) = √((1 + cos x) / 2)

Tactic:
add_div,

Goal state after:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
this : 0 ≤ cos (x / 2)
⊢ √(1 / 2 + cos (2 * (x / 2)) / 2) = √(1 / 2 + cos x / 2)
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
⊢ ‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
by
  cases (norm_nonneg f).eq_or_lt' with
  | inl h =>
    rcases mk_surjective x with ⟨x, rfl⟩
    simpa [h] using le_opNorm f x
  | inr h =>
    rw [← not_lt, ← lt_div_iff₀' h, norm_lt_iff]
    rintro ⟨x, rfl, hx⟩
    exact ((lt_div_iff₀' h).1 hx).not_ge (le_opNorm f x)

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
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖(mk I) a‖ < ε₁ ∧ ‖(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖(mk I) b‖ < ε₂ ∧ ‖(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖(mk I) a‖ * ‖(mk I) b‖ < ε ∧ ‖(mk I) a‖ * ‖(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖(mk I) b‖ - ‖b‖ < ε₂

Tactic:
by linarith [Ideal.Quotient.norm_mk_le I b]

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

Goal state before:
pp: n : ℕ
⊢ 1 - (2 + sqrtTwoAddSeries 0 n) / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

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

Tactic:
add_div,

Goal state after:
n : ℕ
⊢ 1 - (2 / 2 ^ 2 + sqrtTwoAddSeries 0 n / 2 ^ 2) = 1 / 2 - sqrtTwoAddSeries 0 n / 4

n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
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_nhdsGT (neg_lt_self pi_div_two_pos)] with x hx
    exact cos_pos_of_mem_Ioo hx

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
n : ℕ
⊢ ‖v n‖ ≤ C * r ^ n

Tactic:
simp only [v]

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
n : ℕ
⊢ ‖if n < N then 0 else u n‖ ≤ C * r ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x✝¹ : X
x✝ : x✝¹ ∈ pathComponentIn F x
γ : Path x x✝¹
hγ : ∀ (t : ↑I), γ t ∈ F
⊢ JoinedIn (pathComponentIn F x) x x✝¹

Tactic:
refine ⟨γ, fun t ↦
      ⟨(γ.truncateOfLE t.2.1).cast (γ.extend_zero.symm) (γ.extend_extends' t).symm, fun t' ↦ ?_⟩⟩
    dsimp [Path.truncateOfLE, Path.truncate]
    exact γ.extend_extends' ⟨min (max t'.1 0) t.1, by simp [t.2.1, t.2.2]⟩ ▸ hγ _

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
s : Set X
t : Set Y
hs : IsPathConnected s
ht : IsPathConnected t
x✝³ x✝² : X × Y
x₁ : X
y₁ : Y
x✝¹ : (x₁, y₁) ∈ s ×ˢ t
hx₁ : (x₁, y₁).1 ∈ s
hy₁ : (x₁, y₁).2 ∈ t
x₂ : X
y₂ : Y
x✝ : (x₂, y₂) ∈ s ×ˢ t
hx₂ : (x₂, y₂).1 ∈ s
hy₂ : (x₂, y₂).2 ∈ t
⊢ JoinedIn (s ×ˢ t) (x₁, y₁) (x₂, y₂)

Tactic:
exact hs.joinedIn x₁ hx₁ x₂ hx₂ |>.prod <| ht.joinedIn y₁ hy₁ y₂ hy₂

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n
⊢ ‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)

Tactic:
rw [norm_eq' p hp.out, this, abs_sub_round_div_natCast_eq]

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

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

Tactic:
Real.cos_add_pi,

Goal state after:
case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -Real.cos (Real.arcsin ((-x).im / ‖x‖)) = x.re / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
rw [Real.cos_add_pi, Real.cos_arcsin]
    field_simp
    simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
    field

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

Goal state before:
pp: x : ℝ
⊢ x ≤ rexp (log x)

Tactic:
by_cases h_zero : x = 0

Goal state after:
case pos
x : ℝ
h_zero : x = 0
⊢ x ≤ rexp (log x)

case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : z = 0
⊢ 1 = 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : ¬z = 0
⊢ 1 = 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : y * z = 0
h✝¹ : y = 0
h✝ : ¬1 = 0
⊢ 1 = cexp (log 1 * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : z = 0
⊢ 1 = 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : ¬z = 0
⊢ 1 = 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : y * z = 0
h✝¹ : ¬y = 0
h✝ : ¬0 = 0
⊢ 1 = cexp (log 0 * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : z = 0
⊢ 0 = 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : ¬z = 0
⊢ 0 = 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : ¬y * z = 0
h✝¹ : y = 0
h✝ : ¬1 = 0
⊢ 0 = cexp (log 1 * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : z = 0
⊢ 0 = 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : ¬z = 0
⊢ 0 = 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : ¬y * z = 0
h✝¹ : ¬y = 0
h✝ : ¬0 = 0
⊢ 0 = cexp (log 0 * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝² : ¬x = 0
h✝¹ : cexp (log x * y) = 0
h✝ : z = 0
⊢ cexp (log x * (y * z)) = 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝² : ¬x = 0
h✝¹ : cexp (log x * y) = 0
h✝ : ¬z = 0
⊢ cexp (log x * (y * z)) = 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝¹ : ¬x = 0
h✝ : ¬cexp (log x * y) = 0
⊢ cexp (log x * (y * z)) = cexp (log (cexp (log x * y)) * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

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

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

Tactic:
· simp only [hre, arg_of_re_nonneg hre, Real.arcsin_le_pi_div_two, true_or]

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

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ 2 * sin ((θ - ψ) / 2) * cos ((2 * ↑k * π + π) / 2) = 0

Tactic:
add_div,

Goal state after:
case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ 2 * sin ((θ - ψ) / 2) * cos (2 * ↑k * π / 2 + π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
⊢ θ.cos = ψ.cos ↔ θ = ψ ∨ θ = -ψ

Tactic:
induction ψ using Real.Angle.induction_on
  exact cos_eq_real_cos_iff_eq_or_eq_neg

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

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

Tactic:
inv_cpow_eq_ite,

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

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

Tactic:
inv_cpow_eq_ite,

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

Goal state before:
pp: θ : Angle
⊢ θ.toReal = toReal 0 ↔ θ = 0

Tactic:
exact toReal_inj

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

Goal state before:
pp: θ : Angle
h : θ ≠ ↑π
h' : θ.toReal ≠ π
⊢ -θ.toReal ≤ π

Tactic:
linarith [neg_pi_lt_toReal θ]

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

Goal state before:
pp: θ : ℝ
k : ℤ
⊢ (↑θ - k • 0).toReal = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)

Tactic:
← coe_two_pi,

Goal state after:
θ : ℝ
k : ℤ
⊢ (↑θ - k • ↑(2 * π)).toReal = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ rexp (b * x) / x ^ s) atTop atTop

Tactic:
refine ((tendsto_rpow_atTop hb).comp (tendsto_exp_div_rpow_atTop (s / b))).congr' ?_
  filter_upwards [eventually_ge_atTop (0 : ℝ)] with x hx₀
  simp [Real.div_rpow, (exp_pos x).le, rpow_nonneg, ← Real.rpow_mul, ← exp_mul,
    mul_comm x, hb.ne', *]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ ↑(x ^ (y * z)) = ↑(x ^ y) ^ ↑z

Tactic:
Complex.ofReal_cpow hx,

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

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

Tactic:
rw [rpow_zero]

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

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

Tactic:
rw [rpow_zero]

Goal state after:
x : ℝ≥0∞
⊢ 0 < 1
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ midpoint R p₁ p₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p₂) + ⅟2 • -(p -ᵥ p₂) + ⅟2 • (p₂ -ᵥ p)

Tactic:
neg_vsub_eq_vsub_rev,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ midpoint R p₁ p₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p₂) + ⅟2 • (p₂ -ᵥ p) + ⅟2 • (p₂ -ᵥ p)
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ ⅟2 • -(p₁ -ᵥ p) + ⅟2 • -(p₂ -ᵥ p) = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)

Tactic:
neg_vsub_eq_vsub_rev,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ ⅟2 • (p -ᵥ p₁) + ⅟2 • -(p₂ -ᵥ p) = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (midpoint R x y) + f (midpoint R x y) = f x + f y

Tactic:
by rw [hm, midpoint_add_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: 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₁ v₂ : M
h : v₁ ∈ MulAction.orbit (↥(Units.posSubgroup R)) v₂
⊢ SameRay R v₁ v₂

Tactic:
by
  rcases h with ⟨⟨r, hr : 0 < r.1⟩, rfl : r • v₂ = v₁⟩
  exact SameRay.sameRay_pos_smul_left _ hr

Goal state after:
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.linear = g.linear
p : P1
h₂ : f p = g p
⊢ f = g

Tactic:
ext q
  have hgl : g.linear (q -ᵥ p) = toFun g ((q -ᵥ p) +ᵥ q) -ᵥ toFun g q := by simp
  have := f.map_vadd' q (q -ᵥ p)
  rw [h₁, hgl, toFun_eq_coe, map_vadd, linearMap_vsub, h₂] at this
  simpa

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

Goal state before:
pp: k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
inhabited_h : Inhabited ι
⊢ f 0 = g 0

Tactic:
← Pi.single_zero default

Goal state after:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
inhabited_h : Inhabited ι
⊢ f (Pi.single default 0) = g (Pi.single default 0)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
by
  simp only [← segment_eq_Icc h, segment, mem_ofPred_eq, smul_eq_mul, exists_and_left]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : E
h : Convex 𝕜 (a +ᵥ s)
⊢ Convex 𝕜 s

Tactic:
simpa using h.vadd (-a)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : { t // 0 ≤ t }
⊢ [x -[{ t // 0 ≤ t }] y] = uIcc x y

Tactic:
rcases le_total x y with h | h
  · simp [h, Nonneg.segment_eq_Icc]
  · simp [h, segment_symm _ x y, Nonneg.segment_eq_Icc]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ affineSpan 𝕜 ((convexHull 𝕜) s) = affineSpan 𝕜 s

Tactic:
by
  refine le_antisymm ?_ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))
  rw [affineSpan_le]
  exact convexHull_subset_affineSpan s

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s t

Tactic:
← Set.biUnion_of_singleton t

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s (⋃ x ∈ t, {x})
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝⁶ : Monoid N
inst✝⁵ : SMul M N
inst✝⁴ : SMul M α
inst✝³ : MulAction N α
inst✝² : IsScalarTower M N α
inst✝¹ : Bornology M
inst✝ : Bornology N
s t : Set α
h : Absorbs N s t
hbdd : Tendsto (fun x ↦ x • 1) (cobounded M) (cobounded N)
x : M
hx : t ⊆ (x • 1) • s
⊢ t ⊆ x • s

Tactic:
smul_one_smul N x s

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
inst✝⁶ : Monoid N
inst✝⁵ : SMul M N
inst✝⁴ : SMul M α
inst✝³ : MulAction N α
inst✝² : IsScalarTower M N α
inst✝¹ : Bornology M
inst✝ : Bornology N
s t : Set α
h : Absorbs N s t
hbdd : Tendsto (fun x ↦ x • 1) (cobounded M) (cobounded N)
x : M
hx : t ⊆ x • s
⊢ t ⊆ x • s
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case e'_5
R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ a • u = c • u

Tactic:
← hc2,

Goal state after:
case e'_5
R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ (algebraMap R A) c • u = c • u