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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).re = re 0

pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).im = im 0

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).re = re 0

case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).im = im 0
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x✝ : ℂ
xr xi : ℝ
⊢ ((ofRealHom.comp (algebraMap R ℝ)) r * { re := xr, im := xi }).re =
    ({ re := xr, im := xi } * (ofRealHom.comp (algebraMap R ℝ)) r).re

pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x✝ : ℂ
xr xi : ℝ
⊢ ((ofRealHom.comp (algebraMap R ℝ)) r * { re := xr, im := xi }).im =
    ({ re := xr, im := xi } * (ofRealHom.comp (algebraMap R ℝ)) r).im

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x✝ : ℂ
xr xi : ℝ
⊢ ((ofRealHom.comp (algebraMap R ℝ)) r * { re := xr, im := xi }).re =
    ({ re := xr, im := xi } * (ofRealHom.comp (algebraMap R ℝ)) r).re

case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x✝ : ℂ
xr xi : ℝ
⊢ ((ofRealHom.comp (algebraMap R ℝ)) r * { re := xr, im := xi }).im =
    ({ re := xr, im := xi } * (ofRealHom.comp (algebraMap R ℝ)) r).im
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x : ℂ
⊢ (r • x).re = ((ofRealHom.comp (algebraMap R ℝ)) r * x).re

pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x : ℂ
⊢ (r • x).im = ((ofRealHom.comp (algebraMap R ℝ)) r * x).im

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x : ℂ
⊢ (r • x).re = ((ofRealHom.comp (algebraMap R ℝ)) r * x).re

case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x : ℂ
⊢ (r • x).im = ((ofRealHom.comp (algebraMap R ℝ)) r * x).im
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case «0»
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun z ↦ ![z.re, z.im]) ((fun c ↦ ↑(c 0) + c 1 • I) c) ((fun i ↦ i) ⟨0, ⋯⟩) = c ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun z ↦ ![z.re, z.im]) ((fun c ↦ ↑(c 0) + c 1 • I) c) ((fun i ↦ i) ⟨1, ⋯⟩) = c ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun z ↦ ![z.re, z.im]) ((fun c ↦ ↑(c 0) + c 1 • I) c) ((fun i ↦ i) ⟨0, ⋯⟩) = c ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun z ↦ ![z.re, z.im]) ((fun c ↦ ↑(c 0) + c 1 • I) c) ((fun i ↦ i) ⟨1, ⋯⟩) = c ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case «0»
j : Fin 2
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) j = (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) j

pp: case «1»
j : Fin 2
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) j = (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) j

Tactic:
<;>

Goal state after:
case «0»
j : Fin 2
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) j = (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) j

case «1»
j : Fin 2
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) j = (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) j
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case «0».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Complex.Module

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

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:
<;>

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

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

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

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

pp: 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, ⋯⟩)

pp: 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, ⋯⟩)

Tactic:
<;>

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

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

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: case refine_1
f : ℂ →ₐ[ℝ] ℂ
⊢ f I = I → f = AlgHom.id ℝ ℂ

pp: case refine_2
f : ℂ →ₐ[ℝ] ℂ
⊢ f I = -I → f = ↑conjAe

Tactic:
<;>

Goal state after:
case refine_1
f : ℂ →ₐ[ℝ] ℂ
⊢ f I = I → f = AlgHom.id ℝ ℂ

case refine_2
f : ℂ →ₐ[ℝ] ℂ
⊢ f I = -I → f = ↑conjAe
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (starRingEnd K) (↑(re z) + ↑(im z) * I) = ↑(re z) - ↑(im z) * I

Tactic:
rw [map_add, map_mul, conj_I, conj_ofReal, conj_ofReal, mul_neg, sub_eq_add_neg]

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

Goal state before:
pp: case hre
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re (z * (starRingEnd K) z) = re (↑‖z‖ ^ 2)

pp: case him
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im (z * (starRingEnd K) z) = im (↑‖z‖ ^ 2)

Tactic:
<;>

Goal state after:
case hre
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re (z * (starRingEnd K) z) = re (↑‖z‖ ^ 2)

case him
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im (z * (starRingEnd K) z) = im (↑‖z‖ ^ 2)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case hre
K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℝ
a : K
⊢ re (star (r • a)) = re (star r • star a)

pp: case him
K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℝ
a : K
⊢ im (star (r • a)) = im (star r • star a)

Tactic:
<;>

Goal state after:
case hre
K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℝ
a : K
⊢ re (star (r • a)) = re (star r • star a)

case him
K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℝ
a : K
⊢ im (star (r • a)) = im (star r • star a)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ re ↑n = ↑n

Tactic:
rw [← ofReal_natCast, ofReal_re]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
hxy : re x ≤ re y ∧ im x = im y
z : K
⊢ re (z + x) ≤ re (z + y) ∧ im (z + x) = im (z + y)

Tactic:
simpa [map_add, add_le_add_iff_left, add_right_inj] using hxy

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ re a.1

pp: case refine_2
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ re a.2

pp: case refine_3
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ im a.1

pp: case refine_4
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ im a.2

Tactic:
<;>

Goal state after:
case refine_1
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ re a.1

case refine_2
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ re a.2

case refine_3
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ im a.1

case refine_4
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ im a.2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

Tactic:
rw [← mul_right_inj' (neg_ne_zero.mpr this)]

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ ‖z‖ ≤ im z ↔ -I * z = -I * (I * ↑‖z‖)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z w : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w +
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w

Tactic:
subst h''; exact h.mul_im_ax

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ f =o[map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)

Tactic:
simp only [IsLittleO_def, isBigOWith_map]

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

Goal state before:
pp: case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ c₁ ≤ max c₁ c₂

pp: case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ c₂ ≤ max c₁ c₂

Tactic:
<;>

Goal state after:
case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ c₁ ≤ max c₁ c₂

case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ c₂ ≤ max c₁ c₂
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case refine_1
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
x : α
⊢ ‖g₁ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

pp: case refine_2
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
⊢ ∀ (x : α), ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
x : α
⊢ ‖g₁ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

case refine_2
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
⊢ ∀ (x : α), ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case e'_7
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ
x✝ : α
⊢ f x✝ ^ (n + 1).succ = f x✝ ^ n.succ * f x✝

pp: case e'_8
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ
x✝ : α
⊢ g x✝ ^ (n + 1).succ = g x✝ ^ n.succ * g x✝

Tactic:
<;>

Goal state after:
case e'_7
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ
x✝ : α
⊢ f x✝ ^ (n + 1).succ = f x✝ ^ n.succ * f x✝

case e'_8
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ
x✝ : α
⊢ g x✝ ^ (n + 1).succ = g x✝ ^ n.succ * g x✝
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
⊢ f =o[l] g

Tactic:
apply Asymptotics.isLittleO_of_tendsto'

Goal state after:
case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
⊢ ∀ᶠ (x : α) in l, g x = 0 → f x = 0

case a
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖

Tactic:
refine h.symm.rw (fun x a => ‖a‖ ≤ c * ‖v x‖) (hφ.mono fun x hx => ?_)

Goal state after:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖(φ * v) x‖ ≤ c * ‖v x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
⊢ f =O[l] g ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x / g x‖

Tactic:
refine ⟨div_isBoundedUnder_of_isBigO, fun h => ?_⟩

Goal state after:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x / g x‖
⊢ f =O[l] g
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inl
x : ℝ
h✝ : x ≤ 0
⊢ rexp |x| ≤ rexp x + rexp (-x)

pp: case inr
x : ℝ
h✝ : 0 ≤ x
⊢ rexp |x| ≤ rexp x + rexp (-x)

Tactic:
<;>

Goal state after:
case inl
x : ℝ
h✝ : x ≤ 0
⊢ rexp |x| ≤ rexp x + rexp (-x)

case inr
x : ℝ
h✝ : 0 ≤ x
⊢ rexp |x| ≤ rexp x + rexp (-x)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, a - n ∈ range (j - n)

pp: case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ range (j - n), a + n ∈ {m ∈ range j | n ≤ m}

pp: case refine_3
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, a - n + n = a

pp: case refine_4
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ range (j - n), a + n - n = a

pp: case refine_5
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, 1 / ↑a.factorial = 1 / ↑(a - n + n).factorial

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, a - n ∈ range (j - n)

case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ range (j - n), a + n ∈ {m ∈ range j | n ≤ m}

case refine_3
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, a - n + n = a

case refine_4
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ range (j - n), a + n - n = a

case refine_5
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, 1 / ↑a.factorial = 1 / ↑(a - n + n).factorial
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case a
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ (sin (x * I)).re = (-(I * sin (x * I)) * I).re

pp: case a
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ (sin (x * I)).im = (-(I * sin (x * I)) * I).im

Tactic:
<;>

Goal state after:
case a
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ (sin (x * I)).re = (-(I * sin (x * I)) * I).re

case a
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ (sin (x * I)).im = (-(I * sin (x * I)) * I).im
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case calc_1.e_a
x y : ℂ
⊢ x = (x + y) / 2 + (x - y) / 2

pp: case calc_1.e_a
x y : ℂ
⊢ y = (x + y) / 2 - (x - y) / 2

Tactic:
<;>

Goal state after:
case calc_1.e_a
x y : ℂ
⊢ x = (x + y) / 2 + (x - y) / 2

case calc_1.e_a
x y : ℂ
⊢ y = (x + y) / 2 - (x - y) / 2
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case e'_3
x : ℂ
⊢ cexp x = cexp x - ∑ m ∈ range 0, x ^ m / ↑m.factorial

pp: case e'_4
x : ℂ
⊢ Real.exp ‖x‖ = Real.exp ‖x‖ - ∑ m ∈ range 0, ‖x‖ ^ m / ↑m.factorial

Tactic:
<;>

Goal state after:
case e'_3
x : ℂ
⊢ cexp x = cexp x - ∑ m ∈ range 0, x ^ m / ↑m.factorial

case e'_4
x : ℂ
⊢ Real.exp ‖x‖ = Real.exp ‖x‖ - ∑ m ∈ range 0, ‖x‖ ^ m / ↑m.factorial
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖
⊢ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖

pp: case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖
⊢ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖

case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case inl
x : ℝ
h✝ : x ≤ 0
⊢ cos |x| = cos x

pp: case inr
x : ℝ
h✝ : 0 ≤ x
⊢ cos |x| = cos x

Tactic:
<;>

Goal state after:
case inl
x : ℝ
h✝ : x ≤ 0
⊢ cos |x| = cos x

case inr
x : ℝ
h✝ : 0 ≤ x
⊢ cos |x| = cos x
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
rw [← CauSeq.lim_const (abv := norm) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_norm]
  refine CauSeq.lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
  change ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ _
  rw [← sum_Ico_eq_sub _ hj]
  calc
    ‖∑ m ∈ Ico n j, (x ^ m / m.factorial : ℂ)‖
      = ‖∑ m ∈ Ico n j, (x ^ n * (x ^ (m - n) / m.factorial) : ℂ)‖ := by
      refine congr_arg norm (sum_congr rfl fun m hm => ?_)
      rw [mem_Ico] at hm
      rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.1]
    _ ≤ ∑ m ∈ Ico n j, ‖x ^ n * (x ^ (m - n) / m.factorial)‖ :=
      IsAbsoluteValue.abv_sum norm ..
    _ ≤ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (m - n).factorial) := by
      simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
      gcongr with i hi
      · rw [Complex.norm_pow]
      · simp
    _ = ‖x‖ ^ n * ∑ m ∈ range (j - n), (‖x‖ ^ m / m.factorial) := by
      simp [← mul_sum, sum_Ico_eq_sum_range]
    _ ≤ ‖x‖ ^ n * Real.exp ‖x‖ := by
      gcongr
      refine Real.sum_le_exp_of_nonneg ?_ _
      exact norm_nonneg _

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

Goal state before:
pp: case e'_3
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖↑x‖ ≤ 1
⊢ |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| = ‖cexp ↑x - ∑ m ∈ range n, ↑x ^ m / ↑m.factorial‖

pp: case e'_4.e'_5
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖↑x‖ ≤ 1
⊢ |x| = ‖↑x‖

pp: case e'_4.e'_6
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖↑x‖ ≤ 1
⊢ ↑n.succ / (↑n.factorial * ↑n) = ↑n.succ * (↑n.factorial * ↑n)⁻¹

Tactic:
<;>

Goal state after:
case e'_3
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖↑x‖ ≤ 1
⊢ |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| = ‖cexp ↑x - ∑ m ∈ range n, ↑x ^ m / ↑m.factorial‖

case e'_4.e'_5
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖↑x‖ ≤ 1
⊢ |x| = ‖↑x‖

case e'_4.e'_6
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖↑x‖ ≤ 1
⊢ ↑n.succ / (↑n.factorial * ↑n) = ↑n.succ * (↑n.factorial * ↑n)⁻¹
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← cos_sq',

Goal state after:
x : ℝ
⊢ |cos x| = √(cos x ^ 2)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case inl
x : ℝ
h✝ : x ≤ 0
⊢ cosh |x| = cosh x

pp: case inr
x : ℝ
h✝ : 0 ≤ x
⊢ cosh |x| = cosh x

Tactic:
<;>

Goal state after:
case inl
x : ℝ
h✝ : x ≤ 0
⊢ cosh |x| = cosh x

case inr
x : ℝ
h✝ : 0 ≤ x
⊢ cosh |x| = cosh x