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

Goal state before:
pp: case «1»
j : Fin 2
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, 0; 0, -1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: ⊢ ℝ[I] = ⊤

Tactic:
refine top_unique fun x hx => ?_; clear hx
  rw [← x.re_add_im, ← smul_eq_mul, ← Complex.coe_algebraMap]
  exact add_mem (algebraMap_mem _ _) (Subalgebra.smul_mem _ (subset_adjoin <| by simp) _)

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ (liftAux I' hI').range = ℝ[I']

Tactic:
[

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ (liftAux I' hI').range = ℝ[I']
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ⊢ ∀ (x y : ℤ), dist ↑x ↑y = dist x y

Tactic:
[

Goal state after:
⊢ ∀ (x y : ℤ), dist ↑x ↑y = dist x y
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ s ⊆ slitPlane ↔ -↑r ∉ s

Tactic:
[

Goal state after:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ s ⊆ slitPlane ↔ -↑r ∉ s
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: r : ℝ
⊢ ↑(ℜ ↑r) = ↑r

Tactic:
by
  rw [realPart_apply_coe, star_def, conj_ofReal, ← two_smul ℝ (r : ℂ)]
  simp

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
hz : ‖z‖ = 1
⊢ (starRingEnd K) z * z = 1

Tactic:
[

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
hz : ‖z‖ = 1
⊢ (starRingEnd K) z * z = 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z⁻¹ = -im z / normSq z

Tactic:
rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing (codRestrict (e.source.domRestrict ↑e.toPartialEquiv) e.target ⋯)

Tactic:
← PartialEquiv.toEquiv_eq_codRestrict_restrict

Goal state after:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing ⇑e.toEquiv
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ z < w ↔ re z < re w ∧ im z = im w

Tactic:
[

Goal state after:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ z < w ↔ re z < re w ∧ im z = im w
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ ∃ x ≥ 0, ↑x = z

Tactic:
[

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ ∃ x ≥ 0, ↑x = z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ ∃ x > 0, ↑x = z

Tactic:
[

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ ∃ x > 0, ↑x = z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z ≤ 0 ↔ ∃ x ≤ 0, ↑x = z

Tactic:
[

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z ≤ 0 ↔ ∃ x ≤ 0, ↑x = z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ ∃ x < 0, ↑x = z

Tactic:
[

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ ∃ x < 0, ↑x = z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
by
  rw [eq_comm, ← norm_le_re_iff_eq_norm, ← sqrt_normSq_eq_norm, normSq_apply]
  simp [nonneg_iff.mp hx]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑e.symm ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑e.symm ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
x : Y
h : x ∈ e.target
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x)

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
x : Y
h : x ∈ e.target
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ IsClosed {p | re p.1 ≤ re p.2 ∧ im p.1 = im p.2}

Tactic:
[

Goal state after:
K : Type u_1
inst✝ : RCLike K
⊢ IsClosed {p | re p.1 ≤ re p.2 ∧ im p.1 = im p.2}
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case mpr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < ↑n
hn₀ : 0 < ↑n
x : α
hfg : ‖f x‖ ≤ (↑n)⁻¹ * ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
⊢ 0 < (↑n)⁻¹

Tactic:
exact inv_pos.2 hn₀

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

Goal state before:

Tactic:
‖f x‖ ≤ c * ‖g x‖ := hx
    _ ≤ c * (c' * ‖k x‖) := by gcongr
    _ = c * c' * ‖k x‖ := (mul_assoc _ _ _).symm

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'

Tactic:
[

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'

Tactic:
[

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'
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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
⊢ ε > 0 → ∃ i, ∀ j ≥ i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) i) < ε

Tactic:
ε0

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) i) < ε
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : E →ₛₗ[σ₁₂] E₂
hf : Isometry ⇑f
⊢ ∀ (x : E), ‖f x‖ = ‖x‖

Tactic:
[

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : E →ₛₗ[σ₁₂] E₂
hf : Isometry ⇑f
⊢ ∀ (x : E), ‖f x‖ = ‖x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
s : Set α
⊢ f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
[

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
s : Set α
⊢ f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
⊢ f =O[⊤] g ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖

Tactic:
[

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
⊢ f =O[⊤] g ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case empty
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ ∅, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith (∑ i ∈ ∅, C i) l (∑ i ∈ ∅, A i) g

Tactic:
Finset.sum_empty

Goal state after:
case empty
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ ∅, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith 0 l (∑ i ∈ ∅, A i) g
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case cons
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s✝ : Finset ι
B : ι → α → ℝ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, A i =o[l] B i) → (fun H ↦ ∑ i ∈ s, A i H) =o[l] fun H ↦ ∑ i ∈ s, ‖B i H‖
hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1
⊢ (fun H ↦ ∑ i ∈ Finset.cons i s his, A i H) =o[l] fun H ↦ ∑ i ∈ Finset.cons i s his, ‖B i H‖

Tactic:
[

Goal state after:
case cons
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s✝ : Finset ι
B : ι → α → ℝ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, A i =o[l] B i) → (fun H ↦ ∑ i ∈ s, A i H) =o[l] fun H ↦ ∑ i ∈ s, ‖B i H‖
hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1
⊢ (fun H ↦ ∑ i ∈ Finset.cons i s his, A i H) =o[l] fun H ↦ ∑ i ∈ Finset.cons i s his, ‖B i H‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =O[⊤ ×ˢ l] Function.uncurry B
⊢ (fun H ↦ ∑ j ∈ i H, A j H) =O[l] fun H ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
simp only [IsBigO_def]
  obtain ⟨C, hC⟩ := hAB.isBigOWith
  exact ⟨C, hC.sum_congr'⟩

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

Goal state before:
pp: x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ cexp (x + y) = cexp x * cexp y

Tactic:
[

Goal state after:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ cexp (x + y) = cexp x * cexp y
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (cosh ↑x).im = 0

Tactic:
← ofReal_cosh_ofReal_re,

Goal state after:
x : ℝ
⊢ (↑(cosh ↑x).re).im = 0
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 - n), 1 / ↑(m + n).factorial ≤ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹

Tactic:
[

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range (j - n), 1 / ↑(m + n).factorial ≤ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹))) j

Tactic:
[

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹))) j
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'' → F''
s : Set E''
x₀ : E''
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : n ≠ 0
⊢ ‖x₀ - x₀‖ ^ n = 0

Tactic:
[

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
s : Set E''
x₀ : E''
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : n ≠ 0
⊢ ‖x₀ - x₀‖ ^ n = 0
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)

Tactic:
[

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (‖x‖ ^ n / ↑n.factorial * 2)) j

Tactic:
[

Goal state after:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (‖x‖ ^ n / ↑n.factorial * 2)) j
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := ⋯
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ i / ↑n.succ ^ i ≤ 2

Tactic:
[

Goal state after:
case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := ⋯
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ i / ↑n.succ ^ i ≤ 2
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖↑x‖ ≤ 1

Tactic:
by exact_mod_cast hx

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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial)) j

Tactic:
[

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

Goal state before:
pp: G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

Tactic:
[

Goal state after:
G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial) * I / 2 -
        (cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial) * I / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial‖ / 2

Tactic:
grw [norm_sub_le]

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial) * I / 2‖ +
      ‖(cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial) * I / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial‖ / 2
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ Ico n j, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)

Tactic:
[

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ Ico n j, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ Summable fun n ↦ ‖∑ k ∈ range (n + 1), f k * g (n - k)‖

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ Summable fun n ↦ ‖∑ k ∈ range (n + 1), f k * g (n - k)‖
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
by
  have H : 0 < 1 - (1 + x + x ^ 2) * (1 - x) := calc
    0 < x ^ 3 := by positivity
    _ = 1 - (1 + x + x ^ 2) * (1 - x) := by ring
  calc
    exp x ≤ _ := exp_bound' h1.le h2.le zero_lt_three
    _ ≤ 1 + x + x ^ 2 := by
      -- Porting note: was `norm_num [Finset.sum] <;> nlinarith`
      -- This proof should be restored after the norm_num plugin for big operators is ported.
      -- (It may also need the positivity extensions in https://github.com/leanprover-community/mathlib4/pull/3907.)
      rw [show 3 = 1 + 1 + 1 from rfl]
      repeat rw [Finset.sum_range_succ]
      norm_num [Nat.factorial]
      nlinarith
    _ < 1 / (1 - x) := by rw [lt_div_iff₀] <;> nlinarith

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
⊢ f =O[atTop] g

Tactic:
refine isBigO_nat_atTop_induction ?hzero ?hrec

Goal state after:
case hzero
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 : ℕ) in atTop, g n = 0 → f n = 0

case hrec
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₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖