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

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

Tactic:
rcases h.exists_pos with ⟨C, C₀, hC⟩
  rw [IsBigOWith_def, eventually_cofinite] at hC
  rcases (hC.toFinset.image fun x => ‖f x‖ / ‖g'' x‖).exists_le with ⟨C', hC'⟩
  have : ∀ x, C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C' := by simpa using hC'
  refine ⟨max C C', lt_max_iff.2 (Or.inl C₀), fun x h₀ => ?_⟩
  rw [max_mul_of_nonneg _ _ (norm_nonneg _), le_max_iff, or_iff_not_imp_left, not_le]
  exact fun hx => (div_le_iff₀ (norm_pos_iff.2 h₀)).1 (this _ hx)

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖
⊢ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖

case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
⊢ ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P)) < ε / (2 * P) * P

Tactic:
rw [← sum_mul, mul_comm]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
⊢ ε / (2 * P) * ∑ i ∈ range (max N M + 1), abv (f i) < ε / (2 * P) * P
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
h'' : rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
have t := sub_le_iff_le_add'.1 h''

Goal state after:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
h'' : rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
t : rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
⊢ ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P)) < ε / (2 * P) * P

Tactic:
rw [← sum_mul, mul_comm]; gcongr

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

Goal state before:
pp: case inr
n : ℕ
hn : 0 < n
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖

Tactic:
NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff

Goal state after:
case inr
n : ℕ
hn : 0 < n
⊢ ∃ i,
    0 < i ∧
      ∀ ⦃x : ℂ⦄, x ∈ {y | ‖y‖ < i} → ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded (image2 (fun a x ↦ x * a) t s)

Tactic:
by rwa [image2_swap]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
x y : Set E
⊢ ↑1 * ediam x + ↑1 * ediam y = ediam x + ediam y

Tactic:
by simp only [ENNReal.coe_one, one_mul]

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

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

Tactic:
sq_sqrt,

Goal state after:
n : ℕ
⊢ 1 - (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: x : ℝ
h0x : 0 ≤ x
hxp✝ : x ≤ π / 2
h✝ : 0 < x
hxp : x = π / 2
⊢ 0 ≤ tan x

Tactic:
simp [hxp, tan_eq_sin_div_cos]

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

Goal state before:
pp: ⊢ Function.Periodic tan π

Tactic:
by
  simpa only [Function.Periodic, tan_eq_sin_div_cos] using! sin_antiperiodic.div cos_antiperiodic

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 : ℕ → α := ⋯
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ ℝ

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 : ℕ → α := ⋯
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ ∀ (n : ℕ), ‖v n‖ ≤ ?m.115 * r ^ n

Tactic:
· exact C

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 : ℕ → α := ⋯
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ ∀ (n : ℕ), ‖v n‖ ≤ C * r ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case snoc
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin n → X
x : X
hp : ∀ (i : Fin (n + 1)), snoc p x i ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), snoc p x i ∈ range ⇑γ

Tactic:
simp only [forall_fin_succ', snoc_castSucc, snoc_last, Path.cast_coe,
    Path.target_mem_range, and_true] at hp ⊢

Goal state after:
case snoc
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin n → X
x : X
hp : (∀ (i : Fin n), p i ∈ s) ∧ x ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin n), p i ∈ range ⇑γ
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n‖ * ‖z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n

Tactic:
norm_pow,

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C * (‖z‖ / ‖w‖) ^ n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
| ‖f n‖ * ‖w ^ n‖ ≤ C

Tactic:
norm_pow,

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
| ‖f n‖ * ‖w‖ ^ n ≤ C
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x : ℝ
hp : p ≠ 0
⊢ ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|

Tactic:
intro p

Goal state after:
p✝ x : ℝ
hp : p✝ ≠ 0
p : ℝ
⊢ 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
upper : ∀ (k : ℕ), ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
lower : ∀ (k : ℕ), ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
I : ∀ (n : ℕ), 0 ≤ f n
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range n, (-1) ^ i * f i| ≤ f n

Tactic:
obtain (h | h) := even_or_odd n

Goal state after:
case inl
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
upper : ∀ (k : ℕ), ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
lower : ∀ (k : ℕ), ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
I : ∀ (n : ℕ), 0 ≤ f n
h : Even n
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range n, (-1) ^ i * f i| ≤ f n

case inr
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
upper : ∀ (k : ℕ), ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
lower : ∀ (k : ℕ), ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
I : ∀ (n : ℕ), 0 ≤ f n
h : Odd n
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range n, (-1) ^ i * f i| ≤ f n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case inr
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ i ∈ Finset.range (2 * (n + 1)), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Odd (2 * n + 1)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i| ≤ f (2 * n + 1)

Tactic:
rw [Nat.mul_add, Finset.sum_range_succ] at upper

Goal state after:
case inr
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Odd (2 * n + 1)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i| ≤ f (2 * n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ π / 2 = π + arcsin x ↔ x ≤ -1

Tactic:
← sub_eq_iff_eq_add',

Goal state after:
x : ℝ
⊢ π / 2 - π = arcsin x ↔ x ≤ -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ tan (arccos x) = √(1 - x ^ 2) / x

Tactic:
rw [arccos, tan_pi_div_two_sub, tan_arcsin, inv_div]

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

Goal state before:
pp: x : ℝ
⊢ rexp 1 * x ≤ rexp x

Tactic:
by_cases hx0 : x ≤ 0

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

case neg
x : ℝ
hx0 : ¬x ≤ 0
⊢ rexp 1 * x ≤ rexp x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| (↑(r * ‖x‖) * (cos ↑x.arg + sin ↑x.arg * I)).arg

Tactic:
arg_mul_cos_add_sin_mul_I (mul_pos hr (norm_pos_iff.mpr hx)) x.arg_mem_Ioc

Goal state after:
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| x.arg
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁹ : NormedRing K
inst✝⁸ : NormedRing 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 n ↦ n • g n) atTop (𝓝 t)

Tactic:
simpa only [nsmul_eq_mul] using hg

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
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1

Tactic:
exact this

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

Goal state before:
pp: x : ↑{0}ᶜ
| log ↑x

Tactic:
log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)

Goal state after:
x : ↑{0}ᶜ
| expOrderIso.symm ⟨|↑x|, ⋯⟩
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case mp
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)

Tactic:
use -n

Goal state after:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ x = ↑(-n) * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_zero_iff]

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

Goal state before:
pp: case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0

Tactic:
intro p

Goal state after:
case inr.hg
n : ℕ
hn : n ≠ 0
p : ℕ
⊢ ↑(p ^ n.factorization p) = 0 → n.factorization p = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
have h₁' : 0 < (n : ℝ) / d := by
      simpa using (Rat.cast_pos (K := ℝ)).2 (of_decide_eq_true h₁)

Goal state after:
e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
rw [lt_iff_le_and_ne, neg_pi_div_two_le_arg_iff, ne_comm, Ne, arg_eq_neg_pi_div_two_iff]
  rcases lt_trichotomy z.re 0 with hre | hre | hre
  · simp [hre.ne, hre.not_ge, hre.not_gt]
  · simp [hre]
  · simp [hre, hre.le, hre.ne']

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

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

Tactic:
toReal_pi_div_two

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

Goal state before:
pp: case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬x = 0

Tactic:
exact ne_of_lt hx

Goal state after:
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 ..
  rw [← log_abs]
  obtain hx | hx := (abs_nonneg x).eq_or_lt'
  · simp [hx]
  · rw [rpow_def_of_pos hx]
    gcongr
    exact mul_inv_le_one

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

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ |(g x).im|
⊢ (fun x ↦ rexp ((f x).arg * (g x).im)) =Θ[l] fun x ↦ 1

Tactic:
by
  rcases hl with ⟨b, hb⟩
  refine Real.isTheta_exp_comp_one.2 ⟨π * b, ?_⟩
  rw [eventually_map] at hb ⊢
  refine hb.mono fun x hx => ?_
  rw [abs_mul]
  exact mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) Real.pi_pos.le

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑(↑x).arg * I) * y) = cexp ((↑(Real.log ‖-↑x‖) + ↑(-↑x).arg * I + ↑π * I) * y)

Tactic:
norm_neg,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑(↑x).arg * I) * y) = cexp ((↑(Real.log ‖↑x‖) + ↑(-↑x).arg * I + ↑π * I) * y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
⊢ ContinuousOn (sign ∘ f) s

Tactic:
by
  refine (continuousOn_of_forall_continuousAt fun θ hθ => ?_).comp hf (Set.mapsTo_image f s)
  obtain ⟨z, hz, rfl⟩ := hθ
  exact continuousAt_sign (hs _ hz).1 (hs _ hz).2

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

Goal state before:
pp: p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ ∀ {p : ℝ}, 0 < p → 0 < x ^ p

Tactic:
intro p

Goal state after:
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
⊢ 0 < p → 0 < x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z

Tactic:
repeat' rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]

Goal state after:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < rexp (log x * z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
simp [one_lt_rpow_iff_of_pos hx, hx]

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

Goal state before:
pp: x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
⊢ x ^ y ≤ x ^ z

Tactic:
rcases eq_or_lt_of_le hx0 with (rfl | hx0')
  · rcases eq_or_ne y 0 with rfl | hy0
    · rw [h rfl rfl]
    · rw [zero_rpow hy0]
      apply zero_rpow_nonneg
  · exact rpow_le_rpow_of_exponent_ge hx0' hx1 hyz

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ InjOn (fun y ↦ y ^ x) {y | 0 ≤ y}

Tactic:
rintro y hy z hz (hyz : y ^ x = z ^ x)
  rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]

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

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

Tactic:
← @mul_inv_cancel₀ _ _ z (ne_of_lt hz).symm

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

Goal state before:
pp: case top
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
    rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case top.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inr.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z