mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖(mk I) a‖ < ε₁ ∧ ‖(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖(mk I) b‖ < ε₂ ∧ ‖(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖(mk I) a‖ * ‖(mk I) b‖ < ε ∧ ‖(mk I) a‖ * ‖(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖a‖ - ‖(mk I) a‖ < ε₁

Tactic:
linarith

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖(mk I) a‖ < ε₁ ∧ ‖(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖(mk I) b‖ < ε₂ ∧ ‖(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖(mk I) a‖ * ‖(mk I) b‖ < ε ∧ ‖(mk I) a‖ * ‖(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖b‖ - ‖(mk I) b‖ < ε₂

Tactic:
linarith

Goal state after:
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:
simp [this]

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ π - 2 * θ = 2 * θ + θ

Tactic:
linarith

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c * c + (2 * c ^ 2 - 1) * s = s * (2 * c * c) + s * (2 * c ^ 2 - 1)

Tactic:
linarith

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

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

Tactic:
linarith

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

Goal state before:
pp: case pos
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
this : ‖∑' (b : ℕ), (fun n ↦ x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
linarith

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
a✝ : Nontrivial R
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
have : 1 ≤ ‖(1 : R)‖ := one_le_norm_one R

Goal state after:
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
a✝ : Nontrivial R
this : 1 ≤ ‖1‖
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
a✝ : Nontrivial R
this : 1 ≤ ‖1‖
⊢ 0 ≤ 1 - ‖x‖

Tactic:
linarith

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

Goal state before:
pp: case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ (2 + 2 * √5) / (2 * 4) = (1 + √5) / 4

Tactic:
linarith

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
a✝ : Nontrivial R
this✝ : 1 ≤ ‖1‖
this : 0 ≤ (1 - ‖x‖)⁻¹
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ x < π

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ -(π / 2) < x

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
⊢ 0 < -x

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
⊢ 0 ≤ -x

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
⊢ -x ≤ π / 2

Tactic:
linarith

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

Goal state before:
pp: x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ -(π / 2) < x

Tactic:
linarith

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

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

Tactic:
by
  convert! continuous_sin.continuousWithinAt.tendsto
  simp

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case e'_3
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : U ∈ {U | IsOpen[inst✝] U}
⊢ {f | MapsTo (⇑f) K U} = restrict K ⁻¹' {f | MapsTo (⇑f) univ U}

Tactic:
simp [Subtype.forall, MapsTo]

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

Goal state before:
pp: case h
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc p y 0) y
hγ₀s : range ⇑γ₀ ⊆ s
hγ₀p : ∀ (i : Fin n), p i ∈ range ⇑γ₀
γ₁ : Path y x
hγ₁ : range ⇑γ₁ ⊆ s
⊢ (range ⇑γ₀ ⊆ s ∧ range ⇑γ₁ ⊆ s) ∧ ∀ (i : Fin n), p i ∈ range ⇑γ₀ ∨ p i ∈ range ⇑γ₁

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ Tendsto (fun i ↦ restrict s (F i)) l
    (𝓝 (restrict s (liftCover' (fun s ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))

Tactic:
liftCover_restrict'

Goal state after:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s ?m.230))

X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ s ∈ fun s ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f
Module: Mathlib.Topology.Path

Goal state before:
pp: 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
⊢ ↑t = 1 / 2

Tactic:
linarith

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 ≤ 0
hc : ‖f a✝‖ = 0
⊢ False

Tactic:
linarith

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)
⊢ ¬Summable f

Tactic:
have key : ∀ᶠ n in atTop, ‖f n‖ ≠ 0 := by
    filter_upwards [h.eventually_const_le hl] with _ hn hc
    rw [hc, _root_.div_zero] at hn
    linarith
  rcases exists_between hl with ⟨r, hr₀, hr₁⟩
  refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently ?_
  filter_upwards [h.eventually_const_le hr₁, key] with _ _ h₁
  rwa [← le_div_iff₀ (lt_of_le_of_ne (norm_nonneg _) h₁.symm)]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
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
⊢ False

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h✝ : t ≤ 0
⊢ t ≤ 0

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h✝ : t ≤ 0
⊢ 2 * t ≤ 0

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ t ≤ 1

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ 1 - t ≤ 1 / 2

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case e_6
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ 1 - 2 * (1 - t) = 2 * t - 1

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.Instances.Sign

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_pos : 0 < a
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
· exact continuousAt_sign_of_pos h_pos

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ p / 2 - p = -(p / 2)

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg.e_6
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₁
⊢ ↑0 = t₁

Tactic:
linarith

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

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

Tactic:
linarith

Goal state after:
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))
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range n, (-1) ^ i * f i| ≤ f n

Tactic:
have upper := hfa.alternating_series_le_tendsto h

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
⊢ |∑' (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 inl.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 : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n)

Tactic:
rw [sub_le_iff_le_add, add_comm]

Goal state after:
case inl.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 : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i + f (2 * n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
h₁ : sin x = y
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin y = x

Tactic:
by
  subst y
  exact injOn_sin (arcsin_mem_Icc _) h₂ (sin_arcsin' (sin_mem_Icc x))

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

Goal state before:
pp: case left
x : ℝ
this : 0 < π
⊢ -(π / 2) < π / 4

Tactic:
linarith

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

Goal state before:
pp: case right
x : ℝ
this : 0 < π
⊢ π / 4 ≤ π / 2

Tactic:
linarith

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

Goal state before:
pp: case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ x ≤ π

Tactic:
linarith

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

Goal state before:
pp: case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ 0 ≤ x

Tactic:
linarith

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

Goal state before:
pp: case inr.left
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)

Tactic:
rw [sub_le_iff_le_add, add_comm]

Goal state after:
case inr.left
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.Complex.Arg

Goal state before:
pp: case refine_1
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ -(π / 2) < θ + π

Tactic:
linarith

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

Goal state before:
pp: case refine_2
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ θ + π < π / 2

Tactic:
linarith

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ θ < 0

Tactic:
linarith

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

Goal state before:
pp: case neg.inl.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ -(π / 2) ≤ θ + π

Tactic:
linarith

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

Goal state before:
pp: case neg.inl.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ + π ≤ π / 2

Tactic:
linarith

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ θ < π + π / 2

Tactic:
linarith

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

Goal state before:
pp: case mp
x : ℝ
a✝ : π / 2 - arcsin x ≤ π / 4
⊢ π / 4 ≤ arcsin x

Tactic:
linarith

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
⊢ 0 ≤ θ

Tactic:
linarith

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

Goal state before:
pp: case mpr
x : ℝ
a✝ : π / 4 ≤ arcsin x
⊢ π / 2 - arcsin x ≤ π / 4

Tactic:
linarith

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

Goal state before:
pp: case neg.inr.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ -(π / 2) ≤ θ - π

Tactic:
linarith

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

Goal state before:
pp: case neg.inr.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ θ - π ≤ π / 2

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
hx : x < -1
⊢ 1 < -x

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ 0 < -x

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ -x < 1

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x - 1 ≤ x

Tactic:
linarith

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

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

Tactic:
linarith

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

Goal state before:
pp: case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(π / 2) + ↑π = ↑(-π / 2)

Tactic:
rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]

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

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ x ≠ 0

Tactic:
linarith

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

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x

Tactic:
linarith

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

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y

Tactic:
linarith

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

Goal state before:
pp: case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Tactic:
rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)

Goal state after:
case mpr.inl
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0

case mpr.inr
⊢ 0 ^ 0 = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)

Goal state after:
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)

Goal state after:
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
k : ℤ
h : -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π
⊢ (2 * ↑k - 1) * π < θ

Tactic:
linarith

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

Goal state before:
pp: θ : ℝ
k : ℤ
h : -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π
⊢ θ ≤ (2 * ↑k + 1) * π

Tactic:
linarith

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

Goal state before:
pp: θ : ℝ
k : ℤ
h : (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
⊢ -π < θ - 2 * ↑k * π

Tactic:
linarith

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

Goal state before:
pp: θ : ℝ
k : ℤ
h : (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
⊢ θ - 2 * ↑k * π ≤ π

Tactic:
linarith

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

Goal state before:
pp: θ : Angle
h : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π
⊢ π / 2 < θ.toReal

Tactic:
linarith

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

Goal state before:
pp: θ : Angle
h : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π
⊢ θ.toReal ≤ -π / 2

Tactic:
linarith

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

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)

Tactic:
suffices ContinuousAt (Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π) (-x) by
      rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ if False then if x = 0 then 1 else 0 else rexp (log b * x) * cos (x * π)) atTop (𝓝 0)

Tactic:
ite_false

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ rexp (log b * x) * cos (x * π)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ 0 < -b

Tactic:
linarith

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ -b < 1

Tactic:
linarith

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

Goal state before:
pp: case mpr
x a : ℝ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Tactic:
rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)

Goal state after:
case mpr.inl
x : ℝ
h : x ≠ 0
⊢ 0 ^ x = 0

case mpr.inr
⊢ 0 ^ 0 = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case neg
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y
⊢ ↑x < ↑(a ^ y)

Tactic:
exact mod_cast hc a ha

Goal state after: