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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖cexp x - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
Complex.exp,

Goal state after:
x : ℂ
n : ℕ
⊢ ‖(exp' x).lim - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case pos
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
hf : f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
simp [hf, hC_pos]

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖cexp x - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖

Tactic:
Complex.exp,

Goal state after:
x : ℂ
n : ℕ
⊢ ‖(exp' x).lim - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * Real.exp ‖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
this :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) +
      (∑ i ∈ range K, abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) -
        ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) <
    ε / (2 * P) * P + ε / (4 * Q) * (2 * Q)
⊢ ∑ i ∈ range K, abv (f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) < ε

Tactic:
by
    rw [hε] at this
    simpa [abv_mul abv] using this

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |x| ^ 4 * (5 / 96) + x ^ 2 / 2 ≤ 1 * (5 / 96) + 1 / 2

Tactic:
by
                  gcongr
                  · exact pow_le_one₀ (abs_nonneg _) hx
                  · rw [sq, ← abs_mul_self, abs_mul]
                    exact mul_le_one₀ hx (abs_nonneg _) hx

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

Goal state before:
pp: n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (-(t / ↑n)) ^ n = rexp (-t)

Tactic:
by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity

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

Goal state before:
pp: f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
n₀ : ℕ
⊢ (∀ (y : ℕ), n₀ ≤ y → 0 < g y) →
    (∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y) →
      (∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n) →
        ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
hn₀

Goal state after:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
n₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
⊢ (∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y) →
    (∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n) →
      ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ Subtype.val ∘ ⇑expOrderIso '' Set.Iio a = Set.Ioo 0 ((Subtype.val ∘ ⇑expOrderIso) a)

Tactic:
image_comp,

Goal state after:
a : ℝ
⊢ Subtype.val '' ⇑expOrderIso '' Set.Iio a = Set.Ioo 0 ((Subtype.val ∘ ⇑expOrderIso) a)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ Subtype.val ∘ ⇑expOrderIso '' Set.Iic a = Set.Ioc 0 ((Subtype.val ∘ ⇑expOrderIso) a)

Tactic:
image_comp,

Goal state after:
a : ℝ
⊢ Subtype.val '' ⇑expOrderIso '' Set.Iic a = Set.Ioc 0 ((Subtype.val ∘ ⇑expOrderIso) a)
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s : Set E
⊢ (∃ C, ∀ x ∈ s, ‖x‖ ≤ C) → ∃ C, ∀ x ∈ s, ‖x‖ ≤ C

Tactic:
exact id

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✝⁶ : Ring R
inst✝⁵ : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖mk a‖ - ‖a‖ < δ

Tactic:
by linarith [Submodule.Quotient.norm_mk_le S a]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ ‖c‖ • (ediam x).toReal = ‖c‖ * (ediam x).toReal

Tactic:
smul_eq_mul

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

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
⊢ c ∈ f ⁻¹' closedBall x (dist y x) → c ∈ Icc (-1) 1

Tactic:
hc

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ c ∈ Icc (-1) 1
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal

Tactic:
smul_eq_mul

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
⊢ Ioo a b • sphere 0 r = ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
have : EqOn (‖·‖) id (Ioo a b) := fun x hx ↦ abs_of_pos (ha.trans_lt hx.1)
  rw [set_smul_sphere_zero (by simp [ha.not_gt]), ← image_image (· * r), this.image_eq, image_id,
    image_mul_right_Ioo _ _ hr]
  ext x; simp [and_comm]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ ⨅ s, ⨅ (_ : f ∈ s ∧ s ∈ image2 (fun K U ↦ {f | MapsTo (⇑f) K U}) {K | IsCompact K} {t | IsOpen[inst✝] t}), 𝓟 s =
    ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen[inst✝] U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}

Tactic:
@and_comm (f ∈ _),

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ ⨅ s, ⨅ (_ : s ∈ image2 (fun K U ↦ {f | MapsTo (⇑f) K U}) {K | IsCompact K} {t | IsOpen[inst✝] t} ∧ f ∈ s), 𝓟 s =
    ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen[inst✝] U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ JoinedIn univ x y ↔ Joined x y

Tactic:
by
  simp [JoinedIn, Joined, exists_true_iff_nonempty]

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
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ IsPathConnected (f '' F)

Tactic:
use f x, mem_image_of_mem f x_in

Goal state after:
case right
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ ∀ ⦃y : Y⦄, y ∈ f '' F → JoinedIn (f '' F) (f x) y
Module: Mathlib.Topology.Connected.PathConnected

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

Tactic:
| elim0 =>

Goal state after:
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✝ : ℕ
hn : 1 ≤ ‖f (a✝ + 1)‖ / ‖f a✝‖
⊢ ‖f a✝‖ ≠ 0

Tactic:
hc

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✝‖
hc : ‖f a✝‖ = 0
⊢ False
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

Tactic:
· have ht : (t : ℝ) = 1 / 2 := by linarith
    norm_num [ht]

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

Tactic:
refine congr_arg _ (Subtype.ext ?_)
    simp only [coe_symm_eq]
    ring

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
⊢ IsPathConnected (range f)

Tactic:
exact isPathConnected_range hf'

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
⊢ PathConnectedSpace Y

Tactic:
by
  rw [pathConnectedSpace_iff_univ, ← hf.range_eq]
  exact isPathConnected_range hf'

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

Goal state before:
pp: case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
z : ℤ
⊢ closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅

Tactic:
simp only [Real.closedBall_eq_Icc] at hs ⊢

Goal state after:
case inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
⊢ l ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i

Tactic:
have ha : Antitone (fun n ↦ ∑ i ∈ range (2 * n + 1), (-1) ^ i * f i) := by
    refine antitone_nat_of_succ_le (fun n ↦ ?_)
    rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]
    simp_rw [_root_.pow_succ', show (-1 : E) ^ (2 * n) = 1 by simp, neg_one_mul, neg_neg, one_mul,
      ← sub_eq_add_neg, sub_add_eq_add_sub, sub_le_iff_le_add]
    gcongr
    exact hfa (by lia)

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
⊢ l ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
hx : x ∈ Icc (-1) 1
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
← arcsin_sin' hy,

Goal state after:
x y : ℝ
hx : x ∈ Icc (-1) 1
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin x ≤ arcsin (sin y) ↔ x ≤ sin (arcsin (sin y))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Goal state after:
case inl
⊢ ↑‖0‖ * cexp (↑(arg 0) * I) = 0

case inr
x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = ↑‖z‖ * cexp (↑z.arg * I)

Tactic:
hz,

Goal state after:
z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = ↑1 * cexp (↑z.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ arcsin x = π / 2 - arccos x

Tactic:
by simp [arccos]

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

Goal state before:
pp: x : ℝ
⊢ 0 < arccos x ↔ x < 1

Tactic:
by simp [arccos]

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

Goal state before:
pp: ⊢ arccos 0 = π / 2

Tactic:
by simp [arccos]

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

Goal state before:
pp: ⊢ arccos 1 = 0

Tactic:
by simp [arccos]

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

Goal state before:
pp: x : ℝ
⊢ arccos x = π / 2 ↔ x = 0

Tactic:
by simp [arccos]

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

Goal state before:
pp: x : ℝ
⊢ arccos x ≤ π / 2 ↔ 0 ≤ x

Tactic:
by simp [arccos]

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

Goal state before:
pp: x : ℝ
⊢ arccos x < π / 2 ↔ 0 < x

Tactic:
by simp [arccos]

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

Goal state before:
pp: x✝ y x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin x ∈ Icc (-1) 1

Tactic:
by simpa [← abs_le] using abs_sin_le_one x

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

Goal state before:
pp: z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin z.arg → 0 ≤ z.arg

Tactic:
contrapose!
        intro h
        exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)

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

Goal state before:
pp: x : ℂ
r : ℝ
hr : 0 < r
⊢ (↑r * x).arg = x.arg

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Goal state after:
case inl
r : ℝ
hr : 0 < r
⊢ (↑r * 0).arg = arg 0

case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ (↑r * x).arg = x.arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.re ∧ 0 = z.im ↔ 0 ≤ z

Tactic:
nonneg_iff

Goal state after:
z : ℂ
⊢ 0 ≤ z.re ∧ 0 = z.im ↔ 0 ≤ z.re ∧ 0 = z.im
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log ↑n

Tactic:
have : (1 : ℝ) ≤ n := mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
    exact log_nonneg this

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

Goal state before:
pp: case succ
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
⊢ log (x ^ (n + 1)) = ↑(n + 1) * log x

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Goal state after:
case succ.inl
n : ℕ
ih : log (0 ^ n) = ↑n * log 0
⊢ log (0 ^ (n + 1)) = ↑(n + 1) * log 0

case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ (n + 1)) = ↑(n + 1) * log x
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:
rw [hn]; norm_cast

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

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log e

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]
  rw [Real.log_neg_eq_log]
  apply Real.log_pos
  simpa using w

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

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

Tactic:
hz,

Goal state after:
case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ False) ↔ 0 < z.re ∨ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π → θ ≠ ↑π

Tactic:
rintro ⟨h, h'⟩ rfl
    simp at h

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

Goal state before:
pp: case neg
x y : ℝ
hx : ¬x = 0
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
· rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]

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

Goal state before:
pp: x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y

Tactic:
← hx

Goal state after:
x y z : ℝ
hxy : 0 < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
· rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]

Goal state after:
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ x = y ^ z⁻¹ ↔ x ^ z = y

Tactic:
rw [← rpow_left_inj hx _ hz, rpow_inv_rpow hy hz]

Goal state after:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ y ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a ↦ a ^ y) x

Tactic:
hz,

Goal state after:
case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a ↦ a ^ (-z)) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
z : ℝ
h : 0 < z
x : ℝ≥0
hxy : ↑x < ∞
⊢ (fun x ↦ x ^ z) ↑x < (fun x ↦ x ^ z) ∞

Tactic:
simp only [top_rpow_of_pos h, ← coe_rpow_of_nonneg _ h.le, coe_lt_top]

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

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ 1 ≤ ↑n

Tactic:
by
    exact_mod_cast Nat.one_le_of_lt h.lt

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

Goal state before:
pp: case hx
x : ℂ
⊢ 0 ≤ ‖x‖

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

pp: case hr
x : ℂ
⊢ x.arg ≤ π

Tactic:
exacts [norm_nonneg _, (neg_pi_lt_arg _).le, arg_le_pi _]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y z : M
hyz : SameRay R y z
hxy : SameRay R 0 y
hy : y = 0 → 0 = 0 ∨ z = 0
⊢ SameRay R 0 z

case inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
⊢ SameRay R x z
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 : Type u_6
inst✝¹ : FunLike F M N
inst✝ : LinearMapClass F R M N
f : F
hf : Function.Injective ⇑f
⊢ SameRay R (f x) (f y) ↔ SameRay R x y

Tactic:
by
  simp only [SameRay, map_zero, ← hf.eq_iff, map_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case mpr
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
hs : 0 ∈ s
x : V
⊢ x ∈ ↑s → x ∈ ↑s -ᵥ ↑s

Tactic:
exact fun h => ⟨x, h, 0, hs, by simp⟩

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

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
x : α
⊢ Absorbs G₀ s {x} ↔ ∀ᶠ (c : G₀) in cobounded G₀, c⁻¹ • x ∈ s

Tactic:
by simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_singleton]

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module 𝕜 (M i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
⊢ update y i '' [x₁ -[𝕜] x₂] = [update y i x₁ -[𝕜] update y i x₂]

Tactic:
rw [segment_eq_image₂, segment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp only [← update_smul, ← update_add, Convex.combo_self ha.2.2]

Goal state after: