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

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a✝ : α
hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖
hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖
⊢ ‖f₁ a✝‖ * ‖f₂ a✝‖ ≤ c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖

Tactic:
convert! mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a✝ : α
hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖
hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖
⊢ c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖ = c₁ * ‖g₁ a✝‖ * (c₂ * ‖g₂ a✝‖)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x ↦ ‖c • f' x‖) =O[l] g ↔ f' =O[l] g

Tactic:
simp only [norm_smul]

Goal state after:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x ↦ ‖c‖ * ‖f' x‖) =O[l] g ↔ f' =O[l] g
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x ↦ ‖c • f' x‖) =o[l] g ↔ f' =o[l] g

Tactic:
simp only [norm_smul]

Goal state after:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x ↦ ‖c‖ * ‖f' x‖) =o[l] g ↔ f' =o[l] g
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x ↦ ‖c • f' x‖) ↔ f =O[l] f'

Tactic:
simp only [norm_smul]

Goal state after:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x ↦ ‖c‖ * ‖f' x‖) ↔ f =O[l] f'
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ ‖c • f' x‖) ↔ f =o[l] f'

Tactic:
simp only [norm_smul]

Goal state after:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ ‖c‖ * ‖f' x‖) ↔ f =o[l] f'
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a✝ : α
hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖
hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖
⊢ ‖k₁ a✝‖ * ‖f' a✝‖ ≤ c * c' * ‖k₂ a✝ • g' a✝‖

Tactic:
convert! mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a✝ : α
hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖
hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖
⊢ c * c' * ‖k₂ a✝ • g' a✝‖ = c * ‖k₂ a✝‖ * (c' * ‖g' a✝‖)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range j with n ≤ m, 1 / ↑m.factorial = ∑ m ∈ range (j - n), 1 / ↑(m + n).factorial

Tactic:
by
        refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_ <;>
          simp +contextual [lt_tsub_iff_right, tsub_add_cancel_of_le]

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

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
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₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
m : ℕ
⊢ m ∈ Finset.Icc n₀ n₁ → ‖f m‖ ≤ C₁ * ‖g m‖

Tactic:
hm

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
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₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
⊢ ‖f m‖ ≤ C₁ * ‖g m‖
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 0 ≤ (1 - abv x ^ n) / (1 - abv x)

Tactic:
refine div_nonneg (sub_nonneg.2 ?_) (sub_nonneg.2 <| le_of_lt hx1)

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ abv x ^ n ≤ 1
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
x : E
s : Set E
⊢ infEDist x⁻¹ s⁻¹ = infEDist x s

Tactic:
rw [← image_inv_eq_inv, infEDist_image isometry_inv]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r✝ ε : ℝ
h : S ≤ T
x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T
r : ℝ
⊢ (∀ (m : M), ↑m = (quotientQuotientEquivQuotient S T h) x → r ≤ ‖m‖) ↔
    ∀ (m : M ⧸ S), ↑m = x → ∀ (m_1 : M), ↑m_1 = m → r ≤ ‖m_1‖

Tactic:
exact ⟨
      fun h₁ y h₂ z h₃ => h₁ z <| by subst_vars; rfl,
      fun h₁ y h₂ => h₁ y ((quotientQuotientEquivQuotient S T h).injective h₂) y rfl⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖(mk' S) m‖ = sInf ((fun x ↦ ‖m + x‖) '' ↑S)

Tactic:
by
  rw [mk'_apply, norm_mk, sInf_image', ← infDist_image isometry_neg, image_neg_eq_neg,
    neg_coe_set (H := S), infDist_eq_iInf]
  simp only [dist_eq_norm', sub_neg_eq_add, add_comm]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ (1 - r) * dist y x ≤ (1 - 0) * dist y x

Tactic:
gcongr; exact h.1

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

Goal state before:
pp: 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)⁻¹ʳ
⊢ (1 - x)⁻¹ʳ ^ 2 - (1 - x) * (1 - x)⁻¹ʳ * (1 - x)⁻¹ʳ = x * (1 - x)⁻¹ʳ ^ 2

Tactic:
by noncomm_ring

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F

Tactic:
constructor <;> rintro ⟨x, x_in, h⟩ <;> use x, x_in
  · ext y
    exact ⟨fun hy => hy.mem.2, @h _⟩
  · intro y y_in
    rwa [← h] at y_in

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

Goal state before:
pp: p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|

Tactic:
by
  conv_rhs =>
    congr
    rw [← abs_eq_self.mpr hp.le]
  rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄ : t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₀

pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑0
h✝ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₀

pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑0
h✝ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
· have h₄ : t₁ ≤ 0 := le_of_lt (by simpa using h₂)
      simp [γ.extend_of_le_zero h₄, γ.extend_of_le_zero h₁]

Goal state after:
case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑0
h✝ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₀

case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑0
h✝ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ ⋃ z, closedBall (x + z • p) ε

Tactic:
simp only [dist_eq_norm, mem_preimage, mem_closedBall, zsmul_eq_mul, mem_iUnion, Real.norm_eq_abs,
    ← QuotientAddGroup.mk_sub, norm_eq, ← sub_sub]

Goal state after:
case inr
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε ↔ ∃ i, |y - x - ↑i * p| ≤ ε
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
⊢ False

Tactic:
rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'

Goal state after:
case inr.inr.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ False

case inr.inr.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ False
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
⊢ False

Tactic:
rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
      · have : ↑z * p ≤ -p := by nlinarith
        linarith [abs_eq_self.mpr hp.le]
      · have : p ≤ ↑z * p := by nlinarith
        linarith [abs_eq_self.mpr hp.le]

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

Goal state before:
pp: case inr.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
⊢ False

Tactic:
rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'

Goal state after:
case inr.inr.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : ↑z ≤ -1
⊢ False

case inr.inr.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ False
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
n m : ℕ
⊢ m ∈ Set.Ici n → f m ≤ f n

Tactic:
hm

Goal state after:
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
n m : ℕ
hm : m ∈ Set.Ici n
⊢ f m ≤ f n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case inr.right
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 ∈ Finset.range (2 * n + 1), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n + 1)

Tactic:
simpa [Finset.sum_range_succ, add_comm, pow_add] using upper

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

Goal state before:
pp: case neg
x : ℝ
hx₁ : x < -1
⊢ sin π = √(1 - x ^ 2)

Tactic:
sin_pi,

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ 0 = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0

Tactic:
· obtain ⟨x, y⟩ := z
    rintro ⟨h, rfl : y = 0⟩
    exact arg_ofReal_of_nonneg h

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

Goal state before:
pp: x : ℂ
⊢ x ∈ range cexp → x ∈ {0}ᶜ

Tactic:
rintro ⟨x, rfl⟩
      exact exp_ne_zero x

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ -log x ≤ x⁻¹

Tactic:
← log_inv

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ log x⁻¹ ≤ x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
← log_inv

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

Goal state before:
pp: case mp
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) → ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

pp: case mpr
x : ℂ
⊢ (∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x) → ∃ θ, cexp (↑θ * I) = x

Tactic:
· rintro ⟨θ, rfl⟩
    refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
    · convert! toIocMod_mem_Ioc _ _ _
      ring
    · rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]

Goal state after:
case mpr
x : ℂ
⊢ (∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x) → ∃ θ, cexp (↑θ * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ₁ θ₂ : Angle
⊢ (θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin

Tactic:
induction θ₁ using Real.Angle.induction_on
  induction θ₂ using Real.Angle.induction_on
  exact Real.sin_add _ _

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

Goal state before:
pp: θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
⊢ 2 • θ = 2 • ψ ↔ θ = ψ

Tactic:
simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two hθ hψ]

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

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ ∀ (i : ℝ), 0 ≤ i → ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici i

Tactic:
intro b

Goal state after:
y : ℝ
hy : 0 < y
b : ℝ
⊢ 0 ≤ b → ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (Complex.exp (↑(log (-x) * y) + ↑(y * π) * Complex.I)).re = rexp (log x * y) * cos (y * π)

Tactic:
Complex.exp_add_mul_I,

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (Complex.exp ↑(log (-x) * y) * (Complex.cos ↑(y * π) + Complex.sin ↑(y * π) * Complex.I)).re =
    rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ |x ^ y| = x ^ y

Tactic:
abs_eq_self.mpr h_rpow_nonneg

Goal state after:
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ x ^ y = x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.«0»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = 2 * π * ↑((Nat.castEmbedding.trans (addLeftEmbedding (-1))) 0) + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

pp: case inr.«1»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = 2 * π * ↑((Nat.castEmbedding.trans (addLeftEmbedding (-1))) 1) + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
all_goals simp at hk; grind

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

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ≥0), ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Tactic:
intro b

Goal state after:
y : ℝ
hy : 0 < y
b : ℝ≥0
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
by
  rw [← rpow_neg_eq_inv_rpow, rpow_neg hx]

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

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map f l).prod ^ r

Tactic:
by
  rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]
  · rfl
  simpa using hl

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

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

Tactic:
by
  simp only [lt_top_iff_ne_top, Ne, rpow_eq_top_iff_of_pos hy]

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

Goal state before:
pp: case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ^ y ≤ 0 ^ z

Tactic:
rw [zero_rpow hy0]

Goal state after:
case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ≤ 0 ^ z
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:
by
  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: p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖1‖ ≤ 1 / 2
⊢ False

Tactic:
norm_one

Goal state after:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : 1 ≤ 1 / 2
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ (x ^ 2⁻¹).re = √((‖x‖ + x.re) / 2)

Tactic:
← ofReal_ofNat,

Goal state after:
x : ℂ
⊢ (x ^ (↑2)⁻¹).re = √((‖x‖ + x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ (x ^ 2⁻¹).im = √((‖x‖ - x.re) / 2)

Tactic:
← ofReal_ofNat,

Goal state after:
x : ℂ
hx : 0 ≤ x.im
⊢ (x ^ (↑2)⁻¹).im = √((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : x.im < 0
⊢ (x ^ 2⁻¹).im = -√((‖x‖ - x.re) / 2)

Tactic:
← ofReal_ofNat,

Goal state after:
x : ℂ
hx : x.im < 0
⊢ (x ^ (↑2)⁻¹).im = -√((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ |(x ^ 2⁻¹).im| = √((‖x‖ - x.re) / 2)

Tactic:
← ofReal_ofNat,

Goal state after:
x : ℂ
⊢ |(x ^ (↑2)⁻¹).im| = √((‖x‖ - x.re) / 2)