mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ LipschitzWith 1 ⇑re

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im x - im y‖ₑ = ‖im (x - y)‖ₑ

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im (x - y)‖ₑ ≤ ‖x - y‖ₑ

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ LipschitzWith 1 ⇑im

Tactic:
by

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝² : RCLike K
𝕜 : Type u_3
𝕜' : Type u_4
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
x✝¹ x✝ : 𝕜
⊢ ↑(re (x✝¹ + x✝)) + ↑(im (x✝¹ + x✝)) * I = ↑(re x✝¹) + ↑(im x✝¹) * I + (↑(re x✝) + ↑(im x✝) * I)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝² : RCLike K
𝕜 : Type u_3
𝕜' : Type u_4
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
x✝¹ : ℝ
x✝ : 𝕜
⊢ ↑(re (x✝¹ • x✝)) + ↑(im (x✝¹ • x✝)) * I = (RingHom.id ℝ) x✝¹ • (↑(re x✝) + ↑(im x✝) * I)

Tactic:
by

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
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ map K K = ContinuousLinearMap.id ℝ K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ map K ℝ = reCLM

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ map ℝ K = ofRealCLM

Tactic:
by

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
f : Z → X
h : f ⁻¹' e.source = univ
⊢ Continuous[inst✝, inst✝²] f ↔ Continuous[inst✝, inst✝¹] (↑e ∘ f)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
h : I = 0
z : K
⊢ im z = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
x : K
⊢ ↑(re x) = x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
⊢ ∀ (x y : K), re (x * y) = re x * re y

Tactic:
by

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
⊢ ∀ (x y : K), re (x * y) = re x * re y

Tactic:
by simp [im_eq_zero h]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
z : K
⊢ ‖{ toFun := (realRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (realRingEquiv h).invFun, left_inv := ⋯,
          right_inv := ⋯ }
        z‖ =
    ‖z‖

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
x✝ : I = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z ≤ -‖z‖ ↔ z = -(I * ↑‖z‖)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : RCLike K
G : Type u_3
inst✝¹ : Finite G
inst✝ : AddCommGroup G
ψ : AddChar G K
x : G
⊢ ψ (-x) = (starRingEnd K) (ψ x)

Tactic:
by

Goal state after:
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
⊢ ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ a, x < ‖a‖ ∧ ‖a‖ < y

Tactic:
by

Goal state after:
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
⊢ Function.Involutive star

Tactic:
by

Goal state after:
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
⊢ ∀ (r s : 𝕜), star (r * s) = star s * star r

Tactic:
by

Goal state after:
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
⊢ ∀ (r s : 𝕜), star (r + s) = star r + star s

Tactic:
by

Goal state after:
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
⊢ (algebraMap ℝ 𝕜) 1 = 1

Tactic:
by

Goal state after:
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
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x * y) = (algebraMap ℝ 𝕜) x * (algebraMap ℝ 𝕜) y

Tactic:
by

Goal state after:
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
⊢ (algebraMap ℝ 𝕜) 0 = 0

Tactic:
by

Goal state after:
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
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x + y) = (algebraMap ℝ 𝕜) x + (algebraMap ℝ 𝕜) y

Tactic:
by

Goal state after:
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
⊢ ∀ (r : ℝ) (x : 𝕜),
    { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
      x * { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
by

Goal state after:
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
⊢ ∀ (r : ℝ) (x : 𝕜),
    r • x = { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
by

Goal state after:
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
⊢ ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
by

Goal state after:
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
⊢ ∀ {f : Filter 𝕜}, Cauchy f → ∃ x, f ≤ nhds x

Tactic:
by

Goal state after:
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
⊢ 𝕜 →+ ℝ

Tactic:
by

Goal state after:
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
⊢ (⋯ ▸
        let __spread.0 := h.toNormedField;
        re)
      I =
    0

Tactic:
by

Goal state after:
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
⊢ I = 0 ∨ I * I = -1

Tactic:
by

Goal state after:
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 : 𝕜),
    { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
          ((⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z) +
        { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
            ((⋯ ▸
                let __spread.0 := h.toNormedField;
                im)
              z) *
          I =
      z

Tactic:
by

Goal state after:
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
⊢ ∀ (r : ℝ),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ({ toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r) =
      r

Tactic:
by

Goal state after:
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
⊢ ∀ (r : ℝ),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ({ toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r) =
      0

Tactic:
by

Goal state after:
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;
          re)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w -
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w

Tactic:
by

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

Goal state after:
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 : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ((starRingEnd 𝕜) z) =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        z

Tactic:
by

Goal state after:
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 : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ((starRingEnd 𝕜) z) =
      -(⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          z

Tactic:
by

Goal state after:
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
⊢ (starRingEnd 𝕜) I = -I

Tactic:
by

Goal state after:
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 : 𝕜),
    ‖z‖ ^ 2 =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z +
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z

Tactic:
by

Goal state after:
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 : 𝕜),
    (⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          z *
        (⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          I =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        z

Tactic:
by

Goal state after:
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 : 𝕜},
    z ≤ w ↔
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z ≤
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w ∧
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z =
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w

Tactic:
by

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
hk : NormedField 𝕜
h : IsRCLikeNormedField 𝕜
⊢ RCLike 𝕜

Tactic:
by

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁷ : RCLike K
𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : SeminormedAddCommGroup W
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] W
x✝ : V
⊢ ‖(Unitary.toUnits α • e.toLinearEquiv) x✝‖ = ‖x✝‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_3
W : Type u_5
G : Type u_6
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup W
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : G ≃ₗᵢ[𝕜] W
α : ↥(unitary 𝕜)
⊢ (α • e).symm = α⁻¹ • e.symm

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : SeminormedAddCommGroup W
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] G
f : G ≃ₗᵢ[𝕜] W
⊢ (α • e).trans f = α • e.trans f

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : SeminormedAddCommGroup W
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] G
f : G ≃ₗᵢ[𝕜] W
⊢ e.trans (α • f) = α • e.trans f

Tactic:
by

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

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 =Θ[⊥] g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =Θ[l] fun x ↦ ‖g' x‖) ↔ f =Θ[l] g'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
g : α → ℝ
h : (fun x ↦ ‖f' x‖) =ᶠ[l] g
x : α
hx : (fun x ↦ ‖f' x‖) x = g x
⊢ (fun x ↦ ‖f' x‖) x = (fun x ↦ ‖g x‖) x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
l : Filter α
h : f'' =Θ[l] g''
⊢ Tendsto f'' l (𝓝 0) ↔ Tendsto g'' l (𝓝 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ Tendsto (norm ∘ f') l atTop ↔ Tendsto (norm ∘ g') l atTop

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f') ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ g')

Tactic:
by

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : (fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹
⊢ f =Θ[l] g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f₁ f₂ : α → 𝕜
g₁ g₂ : α → 𝕜'
h₁ : f₁ =Θ[l] g₁
h₂ : f₂ =Θ[l] g₂
⊢ (fun x ↦ f₁ x / f₂ x) =Θ[l] fun x ↦ g₁ x / g₂ x

Tactic:
by

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
c : ℝ
f : α → E
g : α → F
l : Filter α
⊢ IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
n : ℤ
⊢ (fun x ↦ f x ^ n) =Θ[l] fun x ↦ g x ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
c₁ : E''
c₂ : F''
⊢ ((fun x ↦ c₁) =Θ[l] fun x ↦ c₂) ↔ (c₁ = 0 ↔ c₂ = 0)

Tactic:
by

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
f : α → E
g : α → F
l : Filter α
⊢ f =O[l] g ↔ ∃ c, IsBigOWith c l f g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F'' : Type u_10
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
⊢ (fun x ↦ 0) =Θ[l] g'' ↔ g'' =ᶠ[l] 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
𝕜 : Type u_14
inst✝¹ : Norm F
inst✝ : NormedField 𝕜
g : α → F
l : Filter α
c : 𝕜
f : α → 𝕜
hc : c ≠ 0
⊢ (fun x ↦ c * f x) =Θ[l] g ↔ f =Θ[l] g

Tactic:
by

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
f : α → E
g : α → F
l : Filter α
⊢ f =O[l] g ↔ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
𝕜 : Type u_14
inst✝¹ : Norm E
inst✝ : NormedField 𝕜
f : α → E
l : Filter α
c : 𝕜
g : α → 𝕜
hc : c ≠ 0
⊢ (f =Θ[l] fun x ↦ c * g x) ↔ f =Θ[l] g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
inst✝ : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ f =Θ[l] g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =Θ[l ×ˢ l'] g → ∀ᶠ (x : α) in l, (fun x_1 ↦ f (x, x_1)) =Θ[l'] fun x_1 ↦ g (x, x_1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =Θ[l ×ˢ l'] g → ∀ᶠ (y : β) in l', (fun x ↦ f (x, y)) =Θ[l] fun x ↦ g (x, y)

Tactic:
by

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

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
l : Filter α
l' : Filter β
⊢ f =Θ[l] g → (f ∘ Prod.fst) =Θ[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
by

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

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
l : Filter α
l' : Filter β
⊢ f =Θ[l] g → (f ∘ Prod.snd) =Θ[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ (fun x ↦ ‖↑(f x)‖) =Θ[l] f

Tactic:
by

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

Goal state before:
pp: f g : ℂ → ℂ
x : ℝ
h : f =O[𝓝[≠] ↑x] g
x✝¹ : ℝ
x✝ : x✝¹ ∈ {x}ᶜ
⊢ ↑x✝¹ ∈ {↑x}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ‖↑n‖ = ‖↑n‖

Tactic:
by

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

Goal state before:
pp: ⊢ Int.cast =Θ[cofinite] Int.cast

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ c⁻¹ > 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ 0 < c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ c⁻¹ > 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
x : α
hx : c⁻¹⁻¹ * ‖f x‖ ≤ ‖g x‖
⊢ 0 < c⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
by

Goal state after: