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

Goal state before:
pp: n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1) / 2) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
cos_half,

Goal state after:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ √((1 + cos (π / 2 ^ (n + 1))) / 2) = sqrtTwoAddSeries 0 (n + 1) / 2

case hl
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ -π ≤ π / 2 ^ (n + 1)

case hr
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ π / 2 ^ (n + 1) ≤ π
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam (c⁻¹ • c • s) ≤ ‖c⁻¹‖₊ • ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)

Tactic:
inv_smul_smul₀ hc s,

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam s ≤ ‖c⁻¹‖₊ • ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : r < 0
⊢ interior (closedBall x r) = ball x r

Tactic:
closedBall_eq_empty.2 hr,

Goal state after:
case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : r < 0
⊢ interior ∅ = ball x r
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
⊢ [∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE

Tactic:
by
  have A : Ico 0 R ⊆ Ioo (-R) R :=
    fun x hx ↦ ⟨(neg_lt_zero.2 (hx.1.trans_lt hx.2)).trans_le hx.1, hx.2⟩
  have B : Ioo 0 R ⊆ Ioo (-R) R := Subset.trans Ioo_subset_Ico_self A
  -- First we prove that 1-4 are equivalent using 2 → 3 → 4, 1 → 3, and 2 → 1
  tfae_have 1 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
  tfae_have 2 → 1 := fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
  tfae_have 3 → 2
  | ⟨a, ha, H⟩ => by
    rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩
    exact ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
      H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩
  tfae_have 2 → 4 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
  tfae_have 4 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
  -- Add 5 and 6 using 4 → 6 → 5 → 3
  tfae_have 4 → 6
  | ⟨a, ha, H⟩ => by
    rcases bound_of_isBigO_nat_atTop H with ⟨C, hC₀, hC⟩
    refine ⟨a, ha, C, hC₀, fun n ↦ ?_⟩
    simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne')
  tfae_have 6 → 5 := fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩
  tfae_have 5 → 3
  | ⟨a, ha, C, h₀, H⟩ => by
    rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩)
    · obtain rfl : f = 0 := by
        ext n
        simpa using H n
      simp only [lt_irrefl, false_or] at h₀
      exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩
    exact ⟨a, A ⟨ha₀, ha⟩,
      isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩
  -- Add 7 and 8 using 2 → 8 → 7 → 3
  tfae_have 2 → 8
  | ⟨a, ha, H⟩ => by
    refine ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ ?_⟩
    rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn
  tfae_have 8 → 7 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩
  tfae_have 7 → 3
  | ⟨a, ha, H⟩ => by
    refine ⟨a, A ⟨?_, ha⟩, .of_norm_eventuallyLE H⟩
    exact nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans)
  tfae_finish

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (frontier (closedBall x r)) = ∅

Tactic:
interior_frontier isClosed_closedBall

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ ∅ = ∅
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (closedBall x r) = ball x r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)
  · rw [closedBall_zero, ball_zero, interior_singleton]
  · exact interior_closedBall x hr

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (frontier (closedBall x r)) = ∅

Tactic:
interior_frontier isClosed_closedBall

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ ∅ = ∅
Module: Mathlib.Topology.Hom.ContinuousEvalConst

Goal state before:
pp: F : Type u_1
α : Type u_2
X : Type u_3
inst✝⁵ : FunLike F α X
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace X
inst✝² : ContinuousEvalConst F α X
F' : Type u_5
inst✝¹ : FunLike F' α X
inst✝ : TopologicalSpace F'
f : F' → F
hc : Continuous[inst✝, inst✝⁴] f
hf : ∀ (g : F'), ⇑(f g) = ⇑g
x : α
⊢ Continuous[inst✝, inst✝³] fun f ↦ f x

Tactic:
simpa only [← hf] using! (continuous_eval_const x).comp hc

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
⊢ c • ball 0 1 = ball 0 ‖c‖

Tactic:
_root_.smul_ball hc,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
⊢ ball (c • 0) (‖c‖ * 1) = ball 0 ‖c‖
Module: Mathlib.Analysis.SpecificLimits.Normed

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

Tactic:
hn

Goal state after:
R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
n : ℕ
hn : 1 ≤ n
⊢ ‖x ^ n‖ = ‖x‖ ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 3 / 2) = √3 / 2

Tactic:
cos_half,

Goal state after:
⊢ √((1 + cos (π / 3)) / 2) = √3 / 2

case hl
⊢ -π ≤ π / 3

case hr
⊢ π / 3 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
this : 2 * c = 4 * c ^ 2 - 1
⊢ 4 * c ^ 2 - 2 * c - 1 = 0

Tactic:
by simp [this]

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
⊢ ↑n * π ≠ π / 5

Tactic:
hn

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : ↑n * π = π / 5
⊢ False
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
⊢ ‖r ^ n‖ ≤ ‖r‖ ^ n → ‖‖↑(u n) * r ^ n‖‖ ≤ ‖1‖ * ‖↑(u n) * ‖r‖ ^ n‖

Tactic:
hn

Goal state after:
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖‖↑(u n) * r ^ n‖‖ ≤ ‖1‖ * ‖↑(u n) * ‖r‖ ^ n‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Tendsto sin (𝓝[<] (π / 2)) (𝓝 1)

Tactic:
convert! continuous_sin.continuousWithinAt.tendsto

Goal state after:
case e'_5
⊢ 1 = sin (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)

Tactic:
have : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re) :=
    apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re

Goal state after:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ x * (1 - x)⁻¹ʳ ^ 2 = (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ

Tactic:
· symm
    calc (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ
    _ = (1 - x)⁻¹ʳ ^ 2 - ((1 - x) * (1 - x)⁻¹ʳ) * (1 - x)⁻¹ʳ := by
      simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)]
    _ = x * (1 - x)⁻¹ʳ ^ 2 := by noncomm_ring

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
n : ℕ
⊢ n ≥ N → u n = v n

Tactic:
hn

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
n : ℕ
hn : n ≥ N
⊢ u n = v n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
⊢ ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖ → ‖f a✝‖ ≤ 0

Tactic:
hn

Goal state after:
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
⊢ ‖f a✝‖ ≤ 0
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
⊢ 1 ≤ ‖f (a✝ + 1)‖ / ‖f a✝‖ → ‖f a✝‖ ≠ 0

Tactic:
hn

Goal state after:
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
hn : 1 ≤ ‖f (a✝ + 1)‖ / ‖f a✝‖
⊢ ‖f a✝‖ ≠ 0
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ range ⇑(γ.truncate t₀ t₁) ⊆ range ⇑γ

Tactic:
rw [← γ.extend_range]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ range ⇑(γ.truncate t₀ t₁) ⊆ range ⇑γ.extend
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:
norm_eq' p hp.out,

Goal state after:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n
⊢ p * |p⁻¹ * (↑m / ↑n * p) - ↑(round (p⁻¹ * (↑m / ↑n * p)))| = p * (↑(min (m % n) (n - m % n)) / ↑n)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
⊢ n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖

Tactic:
hn

Goal state after:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
x : ℝ
hx0 : x ≤ 0
⊢ rexp 1 * x ≤ rexp x

Tactic:
apply le_trans (mul_nonpos_of_nonneg_of_nonpos (exp_pos 1).le hx0) (exp_nonneg x)

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).re = (log ↑x).re

Tactic:
by rw [log_re, ofReal_re, Complex.norm_of_nonneg hx]

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 1 ≤ x⁻¹

Tactic:
← le_inv_comm₀ h1 zero_lt_one,

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

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

Tactic:
hn

Goal state after:
x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℕ
hn : x = ↑n * (2 * ↑π * I)
⊢ ↑n * (2 * ↑π * I) = ↑↑n * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
⊢ -1 < ↑n / ↑d

Tactic:
exact_mod_cast of_decide_eq_true h₂

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

Goal state before:
pp: case refine_1
n m : ℕ
z : ℂ
⊢ -π < ↑m * (↑n).arg

pp: case refine_2
n m : ℕ
z : ℂ
⊢ ↑m * (↑n).arg ≤ π

Tactic:
· simp only [natCast_arg, mul_zero, Left.neg_neg_iff, pi_pos]

Goal state after:
case refine_2
n m : ℕ
z : ℂ
⊢ ↑m * (↑n).arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
this : 1 % 2 = 0 % 2
⊢ ↑θ = ↑ψ

Tactic:
exact absurd this one_ne_zero

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

Goal state before:
pp: θ : Angle
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
sin_eq_iff_eq_or_add_eq_pi

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

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

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

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

Tactic:
· simp [hi, hi.ne, hi.not_gt, arg_neg_eq_arg_add_pi_of_im_neg, sub_eq_add_neg, ←
      add_eq_zero_iff_eq_neg, Real.pi_ne_zero]

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

case inr.inr
x : ℂ
hi : 0 < x.im
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
by
  rw [← toReal_inj, toReal_neg_pi_div_two]

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

Goal state before:
pp: θ : Angle
this : 0 < π / 2
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2

Tactic:
have := toReal_mem_Ioc θ

Goal state after:
θ : Angle
this✝ : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ x ^ (log x)⁻¹ ≤ rexp 1

Tactic:
calc
    _ ≤ |x ^ (log x)⁻¹| := le_abs_self _
    _ ≤ |x| ^ (log x)⁻¹ := abs_rpow_le_abs_rpow ..

Goal state after:
case calc.step
x : ℝ
⊢ |x| ^ (log x)⁻¹ ≤ rexp 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
s : ℂ
hs : s.re ≠ 0
⊢ ‖↑n ^ s‖ = ↑n ^ s.re

Tactic:
← ofReal_natCast,

Goal state after:
n : ℕ
s : ℂ
hs : s.re ≠ 0
⊢ ‖↑↑n ^ s‖ = ↑n ^ s.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℂ
⊢ ‖↑n ^ s‖ = ↑n ^ s.re

Tactic:
← ofReal_natCast,

Goal state after:
n : ℕ
hn : 0 < n
s : ℂ
⊢ ‖↑↑n ^ s‖ = ↑n ^ s.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)

Tactic:
suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y) by
      refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)
      exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm

Goal state after:
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p ↦ (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ 1 ↔ x ≤ y ^ z

Tactic:
← @mul_inv_cancel₀ _ _ z hz.ne.symm

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ √‖x‖ * Real.cos (x.arg / 2) = √((‖x‖ + x.re) / 2)

Tactic:
cos_half,

Goal state after:
x : ℂ
⊢ √‖x‖ * √((1 + Real.cos x.arg) / 2) = √((‖x‖ + x.re) / 2)

case hl
x : ℂ
⊢ -π ≤ x.arg

case hr
x : ℂ
⊢ x.arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
by
  lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx coe_lt_top)
  simp only [coe_le_one_iff] at hx
  simp [← coe_rpow_of_nonneg _ hz, NNReal.rpow_le_one hx hz]

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e : P₁ ≃ᵃ[k] P₂
p : P₂
v : V₂
⊢ v +ᵥ p = e.symm.symm (e.linear.symm v +ᵥ e.symm p)

Tactic:
by
      rw [Equiv.symm_symm, e.map_vadd' ((Equiv.symm e.toEquiv) p) ((LinearEquiv.symm e.linear) v),
        LinearEquiv.apply_symm_apply, Equiv.apply_symm_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
x y : E
⊢ [x -[R] y] ⊆ [x -[𝕜] y]

Tactic:
by
  rintro z ⟨a, b, ha, hb, hab, hxy⟩
  refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩
  all_goals exact zero_smul R (1 : 𝕜) ▸ smul_le_smul_of_nonneg_right ‹_› zero_le_one

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔ s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
refine convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h hx hy, ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) →
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
⊢ b • x ∈ s

Tactic:
rcases eq_or_ne a 0 with rfl | ha₀
  · simp_all
  · calc
      (a⁻¹ • b) • a • x ∈ s := by
        refine hs.smul_mem ?_ ha
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ hba (norm_nonneg _)
      (a⁻¹ • b) • a • x = b • x := by rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]

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

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s

Tactic:
rw [Real.norm_eq_abs, abs_le] at ha

Goal state after:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕜 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
n : ι
⊢ ε n ≠ 0 → ∃ x, ε n • ↑x ∉ V

Tactic:
hn

Goal state after:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕜 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
⊢ ∃ x, ε n • ↑x ∉ V
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ Subsingleton P

Tactic:
have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ s = univ

Tactic:
have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ s = univ
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : ∑ i ∈ s, w i = 1
i2 : ι
hi2 : i2 ∈ s
h : ¬i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0

Tactic:
· simp [hw0 i2 hi2 h]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : (s✝.sup' hs p).closedBall e r = s✝.inf' hs fun i ↦ (p i).closedBall e r
⊢ ((Finset.cons a✝ s✝ h✝).sup' ⋯ p).closedBall e r = (Finset.cons a✝ s✝ h✝).inf' ⋯ fun i ↦ (p i).closedBall e r

Tactic:
simp only [Finset.sup'_cons hs, Finset.inf'_cons hs, closedBall_sup, inf_eq_inter, ih]

Goal state after: