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

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
⊢ cexp x - cexp y = cexp (y + (x - y)) - cexp y

Tactic:
]

Goal state after:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
⊢ cexp x - cexp y = cexp (y + (x - y)) - cexp y
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case refine_2
α : 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
⊢ (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv x)

Tactic:
]

Goal state after:
case refine_2
α : 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
⊢ (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv 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
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
⊢ r < 1

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
⊢ r < 1
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
⊢ ‖(cexp (x - y) - 1) * cexp y‖ < ε

Tactic:
]

Goal state after:
a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
⊢ ‖(cexp (x - y) - 1) * cexp y‖ < ε
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
inst✝ : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : 0 ≤ 0
hr1 : 0 < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : |0| < 1
m_pos : 0 < m
⊢ n.succ ≤ m

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : 0 ≤ 0
hr1 : 0 < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : |0| < 1
m_pos : 0 < m
⊢ n.succ ≤ m
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: x : ℝ
⊢ rexp x = rexp x

pp: case hx
x : ℝ
⊢ 0 ≤ rexp x

pp: case hy
x : ℝ
⊢ 0 ≤ rexp (x / 2)

Tactic:
]

Goal state after:
case hx
x : ℝ
⊢ 0 ≤ rexp x

case hy
x : ℝ
⊢ 0 ≤ rexp (x / 2)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
⊢ rexp x / x ^ n ∈ Set.Ici C

Tactic:
]

Goal state after:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
⊢ rexp x / x ^ n ∈ Set.Ici C
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr.zero
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = 0 + n.succ
⊢ abv (f n.succ) ≤ abv (f n.succ)

pp: case inr.zero.hb
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = 0 + n.succ
⊢ r ^ n.succ ≠ 0

Tactic:
]

Goal state after:
case inr.zero.hb
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = 0 + n.succ
⊢ r ^ n.succ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ rexp x / C

Tactic:
]

Goal state after:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ rexp x / C
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
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ k + (0 + n.succ) ≥ 0 + n.succ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ k + (0 + n.succ) ≥ 0 + n.succ
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ rexp x / C = rexp x / C

Tactic:
]

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

Goal state before:
pp: n : ℕ
x : ℝ
⊢ x ^ n * (rexp x)⁻¹ = x ^ n * (rexp x)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr.succ
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ) * r

Tactic:
]

Goal state after:
case inr.succ
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ) * r
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
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ r * ?a

pp: case a
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ α

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ r * ?a

case a
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ α
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
x : ℝ
⊢ x ^ n / (b * rexp x + c) = x ^ n / (b * rexp x + c)

Tactic:
]

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

Goal state before:
pp: case e'_5
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ 𝓝 0 = 𝓝 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ↑⟨rexp x, ⋯⟩) atTop atTop

Tactic:
]

Goal state after:
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ↑⟨rexp x, ⋯⟩) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Continuous cos

Tactic:
change Continuous fun z => (exp (z * I) + exp (-z * I)) / 2
  fun_prop

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

Goal state before:
pp: ⊢ Set.Ioi 0 = Set.Ioi 0

Tactic:
]

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

Goal state before:
pp: ⊢ cos (Classical.choose exists_cos_eq_zero) = 0

Tactic:
]

Goal state after:
⊢ cos (Classical.choose exists_cos_eq_zero) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 1 ≤ Classical.choose exists_cos_eq_zero

Tactic:
]

Goal state after:
⊢ 1 ≤ Classical.choose exists_cos_eq_zero
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Classical.choose exists_cos_eq_zero ≤ 2

Tactic:
]

Goal state after:
⊢ Classical.choose exists_cos_eq_zero ≤ 2
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ Set.Ioo 0 ↑(expOrderIso a) = Set.Ioo 0 ↑(expOrderIso a)

Tactic:
]

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

Goal state before:
pp: ⊢ 1 ≤ π / 2

Tactic:
]

Goal state after:
⊢ 1 ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0

Tactic:
]

Goal state after:
⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 2 * 0 ^ 2 - 1 = -1

Tactic:
]

Goal state after:
⊢ 2 * 0 ^ 2 - 1 = -1
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ Set.Ioc 0 ↑(expOrderIso a) = Set.Ioc 0 ↑(expOrderIso a)

Tactic:
]

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

Goal state before:
pp: ⊢ atTop = atTop

Tactic:
]

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

Goal state before:
pp: ⊢ Filter.map Subtype.val atBot = Filter.map Subtype.val atBot

Tactic:
]

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

Goal state before:
pp: ⊢ atBot = atBot

Tactic:
]

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x ↦ f (rexp x)) atBot l ↔ Tendsto (f ∘ rexp) atBot l

Tactic:
]

Goal state after:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x ↦ f (rexp x)) atBot l ↔ Tendsto (f ∘ rexp) atBot l
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x

Tactic:
]

Goal state after:
x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inl
x : ℝ
hx : |x| ≤ π
h : x < 0
⊢ -sin x = -sin x

Tactic:
]

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

Goal state before:
pp: case inr
x : ℝ
hx : |x| ≤ π
h : 0 ≤ x
⊢ sin x = sin x

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ sin x = sin x

Tactic:
]

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

Goal state before:
pp: x : ℝ
hl : 0 ≤ x
hu : x ≤ π
⊢ sin x = sin x

Tactic:
]

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

Goal state before:
pp: x : ℝ
hl : -(π / 2) ≤ x
hu : x ≤ π / 2
⊢ cos x = cos x

Tactic:
]

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

Goal state before:
pp: x : ℝ
hl : -π ≤ x
hr : x ≤ π
this : 0 ≤ cos (x / 2)
⊢ √(1 / 2 + cos x / 2) = √(1 / 2 + cos x / 2)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ sin (x / 2) = sin (x / 2)

pp: x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ sin (x / 2)

Tactic:
]

Goal state after:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ sin (x / 2)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: k : ℕ
r : ℝ
hr : 0 < r
⊢ 0 < r

Tactic:
]

Goal state after:
k : ℕ
r : ℝ
hr : 0 < r
⊢ 0 < r
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
⊢ (∃ x_1 ∈ {x | ‖x‖ < ε}, ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
⊢ (∃ x_1 ∈ {x | ‖x‖ < ε}, ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ comap re atTop = comap re atTop

Tactic:
]

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

Goal state before:
pp: x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) = sin (x / 2)

pp: x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) ≤ 0

Tactic:
]

Goal state after:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ comap (fun x ↦ ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Tactic:
]

Goal state after:
⊢ comap (fun x ↦ ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}
⊢ (Filter.map mk (𝓝 1)).HasBasis (fun ε ↦ 0 < ε) fun x ↦ mk '' ball 1 x

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}
⊢ (Filter.map mk (𝓝 1)).HasBasis (fun ε ↦ 0 < ε) fun x ↦ mk '' ball 1 x
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ comap re atBot = comap re atBot

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ sin x = 0 ↔ sin x = 0

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ cos x = 0 ↔ cos x = 0

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ infDist ((IsometryEquiv.divLeft x) 1) (⇑(IsometryEquiv.divLeft x).symm ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ infDist ((IsometryEquiv.divLeft x) 1) (⇑(IsometryEquiv.divLeft x).symm ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑n * π = x

Tactic:
]

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑n * π = x
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S ↔
    m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S

pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ (↑S).Nonempty

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ (↑S).Nonempty
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
]

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
⊢ m ∈ S ↔ m ∈ S

Tactic:
]

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

Goal state before:
pp: x : ℝ
n : ℤ
h : -1 = 1
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
]

Goal state after:
x : ℝ
n : ℤ
h : -1 = 1
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
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 b ↦ a * b) s t)

Tactic:
]

Goal state after:
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded (image2 (fun a b ↦ a * b) s t)
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:
]

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

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

Goal state before:
pp: n : ℤ
hx₁ : -(2 * π) < ↑n * (2 * π)
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0

Tactic:
]

Goal state after:
n : ℤ
hx₁ : -(2 * π) < ↑n * (2 * π)
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0
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 ε : ℝ
⊢ ⨅ i, ⨅ (_ : 0 < i), Filter.principal ((fun p ↦ p.1⁻¹ * p.2) ⁻¹' {x | ‖x‖ < i}) =
    ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ ⨅ i, ⨅ (_ : 0 < i), Filter.principal ((fun p ↦ p.1⁻¹ * p.2) ⁻¹' {x | ‖x‖ < i}) =
    ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
hx₁ : -↑n < 1
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0

Tactic:
]

Goal state after:
n : ℤ
hx₁ : -↑n < 1
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ ball (x * y) δ = ball (x * y) δ

Tactic:
]

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 ε : ℝ
⊢ ∀ (x : M ⧸ ⊥), ‖quotientBot x‖ = ‖x‖

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ ∀ (x : M ⧸ ⊥), ‖quotientBot x‖ = ‖x‖
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball x δ = ball x δ

Tactic:
]

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

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

Tactic:
]

Goal state after:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball x⁻¹ δ = ball x⁻¹ δ

Tactic:
]

Goal state after: