awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x : X
⊢ Membership.mem (γ := Set X) (carrier ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) x ↔
    x ∈ D.carrier

Tactic:
simp [mapIsometry, IsometryEquiv.refl, DeloneSet.copy]

Premises used: Delone.DeloneSet.copy, Delone.DeloneSet.mapIsometry, IsometryEquiv.refl
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
⊢ (↑(packingRadius.{u_1} (X := X) ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) : ℝ) =
    (↑D.packingRadius : ℝ)

Tactic:
simp [mapIsometry, IsometryEquiv.refl, DeloneSet.copy]

Premises used: Delone.DeloneSet.copy, Delone.DeloneSet.mapIsometry, IsometryEquiv.refl
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
⊢ (↑(coveringRadius.{u_1} (X := X) ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) : ℝ) =
    (↑D.coveringRadius : ℝ)

Tactic:
simp [mapIsometry, IsometryEquiv.refl, DeloneSet.copy]

Premises used: Delone.DeloneSet.copy, Delone.DeloneSet.mapIsometry, IsometryEquiv.refl
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
⊢ (mapIsometry f).symm = mapIsometry f.symm

Tactic:
rfl

Premises used: Delone.DeloneSet.copy, Delone.DeloneSet.mapIsometry, Equiv.symm, rfl
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
carrier :
  ∀ (x : Z),
    Membership.mem (γ := Set Z) (DeloneSet.carrier ((mapIsometry (f.trans g) : (a : DeloneSet X) → DeloneSet Z) D)) x ↔
      Membership.mem (γ := Set Z)
        (DeloneSet.carrier
          ((mapIsometry g : (a : DeloneSet Y) → DeloneSet Z) ((mapIsometry f : (a : DeloneSet X) → DeloneSet Y) D)))
        x
packingRadius :
  (↑(DeloneSet.packingRadius.{u_3} (X := Z) ((mapIsometry (f.trans g) : (a : DeloneSet X) → DeloneSet Z) D)) : ℝ) =
    (↑(DeloneSet.packingRadius.{u_3} (X := Z)
          ((mapIsometry g : (a : DeloneSet Y) → DeloneSet Z) ((mapIsometry f : (a : DeloneSet X) → DeloneSet Y) D))) :
      ℝ)
coveringRadius :
  (↑(DeloneSet.coveringRadius.{u_3} (X := Z) ((mapIsometry (f.trans g) : (a : DeloneSet X) → DeloneSet Z) D)) : ℝ) =
    (↑(DeloneSet.coveringRadius.{u_3} (X := Z)
          ((mapIsometry g : (a : DeloneSet Y) → DeloneSet Z) ((mapIsometry f : (a : DeloneSet X) → DeloneSet Y) D))) :
      ℝ)
⊢ Eq.{u_3 + 1} (α := DeloneSet Z) ((mapIsometry (f.trans g) : (a : DeloneSet X) → DeloneSet Z) D : DeloneSet Z)
    ((mapIsometry g : (a : DeloneSet Y) → DeloneSet Z) ((mapIsometry f : (a : DeloneSet X) → DeloneSet Y) D) :
      DeloneSet Z)

Tactic:
ext
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
x : Z
⊢ Membership.mem (γ := Set Z) (carrier ((mapIsometry (f.trans g) : (a : DeloneSet X) → DeloneSet Z) D)) x ↔
    Membership.mem (γ := Set Z)
      (carrier
        ((mapIsometry g : (a : DeloneSet Y) → DeloneSet Z) ((mapIsometry f : (a : DeloneSet X) → DeloneSet Y) D)))
      x

Tactic:
simp [mapIsometry, DeloneSet.copy]

Premises used: Delone.DeloneSet.copy, Delone.DeloneSet.mapIsometry
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
⊢ (↑(packingRadius.{u_3} (X := Z) ((mapIsometry (f.trans g) : (a : DeloneSet X) → DeloneSet Z) D)) : ℝ) =
    (↑(packingRadius.{u_3} (X := Z)
          ((mapIsometry g : (a : DeloneSet Y) → DeloneSet Z) ((mapIsometry f : (a : DeloneSet X) → DeloneSet Y) D))) :
      ℝ)

Tactic:
simp [mapIsometry, DeloneSet.copy]

Premises used: Delone.DeloneSet.copy, Delone.DeloneSet.mapIsometry
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
⊢ (↑(coveringRadius.{u_3} (X := Z) ((mapIsometry (f.trans g) : (a : DeloneSet X) → DeloneSet Z) D)) : ℝ) =
    (↑(coveringRadius.{u_3} (X := Z)
          ((mapIsometry g : (a : DeloneSet Y) → DeloneSet Z) ((mapIsometry f : (a : DeloneSet X) → DeloneSet Y) D))) :
      ℝ)

Tactic:
simp [mapIsometry, DeloneSet.copy]

Premises used: Delone.DeloneSet.copy, Delone.DeloneSet.mapIsometry
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
⊢ (u - v) =o[l] v

Tactic:
h

Premises used: Asymptotics.IsEquivalent
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
⊢ u =O[l] v

Tactic:
(IsBigO.congr_of_sub h.isBigO.symm).mp (isBigO_refl _ _)

Premises used: Asymptotics.IsLittleO.isBigO, Iff.mp, Asymptotics.IsBigO.congr_of_sub, Asymptotics.IsBigO.symm, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
⊢ IsBigO (F := β) l v fun (x : α) ↦ (u - v) x + v x

Tactic:
h.isLittleO.right_isBigO_add

Premises used: Asymptotics.IsEquivalent.isLittleO, Asymptotics.IsLittleO.right_isBigO_add
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
h₁ : ∀ (x : α), u x = (u - v) x + v x
⊢ v =O[l] u

Tactic:
convert! h.isLittleO.right_isBigO_add

Premises used: Asymptotics.IsEquivalent.isLittleO, Asymptotics.IsLittleO.right_isBigO_add
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
x : α
⊢ u x = (u - v) x + v x

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
⊢ u =Θ[l] v

Tactic:
⟨h.isBigO, h.isBigO_symm⟩

Premises used: Asymptotics.IsEquivalent.isBigO_symm, Asymptotics.IsTheta, Asymptotics.IsEquivalent.isBigO, And.intro
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
⊢ v =Θ[l] u

Tactic:
⟨h.isBigO_symm, h.isBigO⟩

Premises used: Asymptotics.IsEquivalent.isBigO_symm, Asymptotics.IsTheta, Asymptotics.IsEquivalent.isBigO, And.intro
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
rw : IsLittleO (E := β) l 0 u
⊢ u ~[l] u

Tactic:
rw [IsEquivalent, sub_self]

Premises used: sub_self, Asymptotics.IsEquivalent
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ IsLittleO (E := β) l 0 u

Tactic:
isLittleO_zero _ _

Premises used: Asymptotics.isLittleO_zero
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ IsLittleO (E := β) l 0 u

Tactic:
exact isLittleO_zero _ _

Premises used: Asymptotics.isLittleO_zero
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
⊢ v ~[l] u

Tactic:
(h.isLittleO.trans_isBigO h.isBigO_symm).symm

Premises used: Asymptotics.IsEquivalent.isBigO_symm, Asymptotics.IsLittleO.symm, Asymptotics.IsEquivalent, Asymptotics.IsEquivalent.isLittleO, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
l : Filter α
u v w : α → β
huv : u ~[l] v
hvw : v ~[l] w
⊢ u ~[l] w

Tactic:
(huv.isLittleO.trans_isBigO hvw.isBigO).triangle hvw.isLittleO

Premises used: Asymptotics.IsEquivalent.isBigO, Asymptotics.IsEquivalent, Asymptotics.IsEquivalent.isLittleO, Asymptotics.IsLittleO.trans_isBigO, Asymptotics.IsLittleO.triangle
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
huw : u =ᶠ[l] w
⊢ w ~[l] v

Tactic:
huv.congr' (huw.sub (EventuallyEq.refl _ _)) (EventuallyEq.refl _ _)

Premises used: Asymptotics.IsLittleO.congr', Asymptotics.IsEquivalent, Filter.EventuallyEq.refl, Filter.EventuallyEq.sub
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hvw : v =ᶠ[l] w
⊢ u ~[l] w

Tactic:
(huv.symm.congr_left hvw).symm

Premises used: Asymptotics.IsEquivalent.congr_left, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
rw : IsLittleO (F := β) l u 0 ↔ u =ᶠ[l] 0
⊢ u ~[l] 0 ↔ u =ᶠ[l] 0

Tactic:
rw [IsEquivalent, sub_zero]

Premises used: sub_zero, Asymptotics.IsEquivalent
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ IsLittleO (F := β) l u 0 ↔ u =ᶠ[l] 0

Tactic:
isLittleO_zero_right_iff

Premises used: Asymptotics.isLittleO_zero_right_iff
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ IsLittleO (F := β) l u 0 ↔ u =ᶠ[l] 0

Tactic:
exact isLittleO_zero_right_iff

Premises used: Asymptotics.isLittleO_zero_right_iff
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] 0 ↔ IsBigO (F := β) l u 0

Tactic:
⟨IsEquivalent.isBigO, fun h ↦ ?_⟩

Premises used: Asymptotics.IsEquivalent.isBigO, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
refine : ∀ (h : IsBigO (F := β) l u 0), u ~[l] 0
⊢ u ~[l] 0 ↔ IsBigO (F := β) l u 0

Tactic:
refine ⟨IsEquivalent.isBigO, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
h : IsBigO (F := β) l u 0
rw : ∃ s ∈ l, Set.EqOn u 0 s
⊢ u ~[l] 0

Tactic:
rw [isEquivalent_zero_iff_eventually_zero, eventuallyEq_iff_exists_mem]

Premises used: Asymptotics.isEquivalent_zero_iff_eventually_zero, Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
h : IsBigO (F := β) l u 0
⊢ ∃ s ∈ l, Set.EqOn u 0 s

Tactic:
⟨{ x : α | u x = 0 }, isBigO_zero_right_iff.mp h, fun x hx ↦ hx⟩

Premises used: Asymptotics.isBigO_zero_right_iff, setOf, And.intro, Exists.intro, Iff.mp, OfNat.ofNat, Eq
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
h : IsBigO (F := β) l u 0
⊢ ∃ s ∈ l, Set.EqOn u 0 s

Tactic:
exact ⟨{ x : α | u x = 0 }, isBigO_zero_right_iff.mp h, fun x hx ↦ hx⟩
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
simp : Tendsto (u - fun (x : α) ↦ c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)
⊢ u ~[l] const α c ↔ Tendsto u l (𝓝 c)

Tactic:
simp +unfoldPartialApp only [IsEquivalent, const, isLittleO_const_iff h]

Premises used: Asymptotics.isLittleO_const_iff, Asymptotics.IsEquivalent, Function.const
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
mp : Tendsto (u - fun (x : α) ↦ c) l (𝓝 0) → Tendsto u l (𝓝 c)
mpr : Tendsto u l (𝓝 c) → Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
⊢ Tendsto (u - fun (x : α) ↦ c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)

Tactic:
constructor
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h_1 : c ≠ 0
h : Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
⊢ Tendsto (fun (x : α) ↦ HSub.hSub (β := α → β) u (fun (x : α) ↦ c) x - -c) l (𝓝 (0 - -c))

Tactic:
have := h.sub (tendsto_const_nhds (x := -c))
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h_1 : c ≠ 0
h : Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
this : Tendsto (fun (x : α) ↦ HSub.hSub (β := α → β) u (fun (x : α) ↦ c) x - -c) l (𝓝 (0 - -c))
⊢ Tendsto (fun (x : α) ↦ u x) l (𝓝 c)

Tactic:
simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this

Premises used: zero_add, sub_add_cancel, sub_neg_eq_add, Pi.sub_apply
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h_1 : c ≠ 0
h : Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
this : Tendsto (fun (x : α) ↦ u x) l (𝓝 c)
⊢ Tendsto u l (𝓝 c)

Tactic:
this
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h_1 : c ≠ 0
h : Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
this : Tendsto (fun (x : α) ↦ u x) l (𝓝 c)
⊢ Tendsto u l (𝓝 c)

Tactic:
exact this
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h_1 : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (fun (x : α) ↦ u x - c) l (𝓝 (c - c))

Tactic:
have := h.sub (tendsto_const_nhds (x := c))
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h_1 : c ≠ 0
h : Tendsto u l (𝓝 c)
this : Tendsto (fun (x : α) ↦ u x - c) l (𝓝 (c - c))
mpr mpr₁ mpr₂ mpr₃ :
  ∀ (this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x - c) l (𝓝 0)), Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
⊢ Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)

Tactic:
rwa [sub_self] at this

Premises used: sub_self
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
inl : ∀ (hu : u ~[l] const α 0), Tendsto u l (𝓝 0)
inr : ∀ (h : ¬c = 0), Tendsto u l (𝓝 c)
⊢ Tendsto u l (𝓝 c)

Tactic:
rcases em <| c = 0 with rfl | h

Premises used: em, rfl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)

Tactic:
(tendsto_congr' <| isEquivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds

Premises used: Iff.mpr, tendsto_const_nhds, Asymptotics.isEquivalent_zero_iff_eventually_zero, Iff.mp, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)

Tactic:
exact (tendsto_congr' <| isEquivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds

Premises used: Iff.mpr, tendsto_const_nhds, Asymptotics.isEquivalent_zero_iff_eventually_zero, Iff.mp, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)

Tactic:
(isEquivalent_const_iff_tendsto h).mp hu

Premises used: Iff.mp, Asymptotics.isEquivalent_const_iff_tendsto
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)

Tactic:
exact (isEquivalent_const_iff_tendsto h).mp hu

Premises used: Iff.mp, Asymptotics.isEquivalent_const_iff_tendsto
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
pos : ∀ (h : c = 0), Tendsto v l (𝓝 c)
neg : ∀ (h : ¬c = 0), Tendsto v l (𝓝 c)
⊢ Tendsto v l (𝓝 c)

Tactic:
by_cases h : c = 0
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : c = 0
pos : ∀ (hu : Tendsto u l (𝓝 0)), Tendsto v l (𝓝 0)
⊢ Tendsto v l (𝓝 c)

Tactic:
subst c
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
hu : Tendsto u l (𝓝 0)
pos : ∀ (hu : IsLittleO (F := ℝ) l u fun (_x : α) ↦ 1), IsLittleO (F := ℝ) l v fun (_x : α) ↦ 1
⊢ Tendsto v l (𝓝 0)

Tactic:
rw [← isLittleO_one_iff ℝ] at hu ⊢

Premises used: Real, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
hu : IsLittleO (F := ℝ) l u fun (_x : α) ↦ 1
⊢ IsLittleO (F := ℝ) l v fun (_x : α) ↦ 1

Tactic:
simpa using (huv.symm.isLittleO.trans hu).add hu

Premises used: Asymptotics.IsLittleO.add, Asymptotics.IsEquivalent.isLittleO, Asymptotics.IsLittleO.trans, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
neg : ∀ (hu : u ~[l] const α c) (h : ¬c = 0), v ~[l] const α c
⊢ Tendsto v l (𝓝 c)

Tactic:
rw [← isEquivalent_const_iff_tendsto h] at hu ⊢

Premises used: Asymptotics.isEquivalent_const_iff_tendsto
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : u ~[l] const α c
h : ¬c = 0
⊢ v ~[l] const α c

Tactic:
huv.symm.trans hu

Premises used: Asymptotics.IsEquivalent.trans, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : u ~[l] const α c
h : ¬c = 0
⊢ v ~[l] const α c

Tactic:
exact huv.symm.trans hu

Premises used: Asymptotics.IsEquivalent.trans, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
⊢ Tendsto u l (𝓝 c) ↔ Tendsto v l (𝓝 c)

Tactic:
⟨huv.tendsto_nhds, huv.symm.tendsto_nhds⟩

Premises used: Asymptotics.IsEquivalent.tendsto_nhds, Iff.intro, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hwv : w =o[l] v
⊢ u + w ~[l] v

Tactic:
simpa only [IsEquivalent, add_sub_right_comm] using huv.add hwv

Premises used: add_sub_right_comm, Asymptotics.IsEquivalent, Asymptotics.IsLittleO.add
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hwv : w =o[l] v
⊢ u - w ~[l] v

Tactic:
simpa only [sub_eq_add_neg] using huv.add_isLittleO hwv.neg_left

Premises used: Asymptotics.IsEquivalent.add_isLittleO, sub_eq_add_neg, Asymptotics.IsLittleO.neg_left
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v w : α → β
l : Filter α
hu : u =o[l] w
hv : v ~[l] w
⊢ u + v ~[l] w

Tactic:
add_comm v u ▸ hv.add_isLittleO hu

Premises used: Asymptotics.IsEquivalent.add_isLittleO, Eq.rec, add_comm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hv : Tendsto (norm ∘ v) l atTop
⊢ (fun (x : α) ↦ u x + c) ~[l] v

Tactic:
huv.add_isLittleO <| isLittleO_const_left.mpr (Or.inr hv)

Premises used: Iff.mpr, Asymptotics.isLittleO_const_left, Asymptotics.IsEquivalent.add_isLittleO, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hv : Tendsto (norm ∘ v) l atTop
⊢ (fun (x : α) ↦ c + u x) ~[l] v

Tactic:
(isLittleO_const_left.mpr (Or.inr hv)).add_isEquivalent huv

Premises used: Iff.mpr, Asymptotics.isLittleO_const_left, Asymptotics.IsLittleO.add_isEquivalent, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : (u - v) =o[l] v
⊢ u ~[l] v

Tactic:
huv

Premises used: Asymptotics.IsEquivalent
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ IsLittleO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (x : α) ↦ -(u - v) x) fun (x : α) ↦ -v x

Tactic:
huv.isLittleO.neg_left.neg_right

Premises used: Asymptotics.IsLittleO.neg_left, Asymptotics.IsEquivalent.isLittleO, Asymptotics.IsLittleO.neg_right
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
h : ∀ (x : α), HSub.hSub (α := α → β) (β := α → β) (fun (x : α) ↦ -u x) (fun (x : α) ↦ -v x) x = -(u - v) x
⊢ IsLittleO (F := β) l (HSub.hSub (α := α → β) (fun (x : α) ↦ -u x) fun (x : α) ↦ -v x) fun (x : α) ↦ -v x

Tactic:
convert! huv.isLittleO.neg_left.neg_right

Premises used: Asymptotics.IsLittleO.neg_left, Asymptotics.IsEquivalent.isLittleO, Asymptotics.IsLittleO.neg_right
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
x : α
⊢ HSub.hSub (α := α → β) (β := α → β) (fun (x : α) ↦ -u x) (fun (x : α) ↦ -v x) x = -(u - v) x

Tactic:
simp [neg_add_eq_sub]

Premises used: neg_add_eq_sub
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
rw : (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
⊢ u ~[l] v ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
rw [IsEquivalent, isLittleO_iff_exists_eq_mul]

Premises used: Asymptotics.IsEquivalent, Asymptotics.isLittleO_iff_exists_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
mp : (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) → ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
mpr : (∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v) → ∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v
⊢ (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
constructor
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
⟨φ + 1, ?_, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
mp : Tendsto (φ + 1) l (𝓝 1)
mp₁ : u =ᶠ[l] (φ + 1) * v
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
refine ⟨φ + 1, ?_, ?_⟩