awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
⊢ (mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D = D
have carrier : ∀ (x : X),
  Membership.mem (γ := Set X) (carrier ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) x ↔
    x ∈ D.carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
carrier :
  ∀ (x : X),
    Membership.mem (γ := Set X)
        (DeloneSet.carrier ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) x ↔
      x ∈ D.carrier
⊢ (mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D = D
have packingRadius : (↑(packingRadius.{u_1} (X := X) ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) : ℝ) =
  (↑D.packingRadius : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
carrier :
  ∀ (x : X),
    Membership.mem (γ := Set X)
        (DeloneSet.carrier ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) x ↔
      x ∈ D.carrier
packingRadius :
  (↑(DeloneSet.packingRadius.{u_1} (X := X)
          ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) :
      ℝ) =
    (↑D.packingRadius : ℝ)
⊢ (mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D = D
have coveringRadius : (↑(coveringRadius.{u_1} (X := X) ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) : ℝ) =
  (↑D.coveringRadius : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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
⊢ 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)
have carrier : ∀ (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: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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
⊢ 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)
have packingRadius : (↑(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: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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))) :
      ℝ)
⊢ 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)
have coveringRadius : (↑(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: ext
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
⊢ v =O[l] u
have h₁ : ∀ (x : α), u x = (u - v) x + v x
Tactic: convert! h.isLittleO.right_isBigO_add
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] u
have rw : IsLittleO (E := β) l 0 u
Tactic: rw [IsEquivalent, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] 0 ↔ u =ᶠ[l] 0
have rw : IsLittleO (F := β) l u 0 ↔ u =ᶠ[l] 0
Tactic: rw [IsEquivalent, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] 0 ↔ IsBigO (F := β) l u 0
have refine : ∀ (h : IsBigO (F := β) l u 0), u ~[l] 0
Tactic: refine ⟨IsEquivalent.isBigO, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
h : IsBigO (F := β) l u 0
⊢ u ~[l] 0
have rw : ∃ s ∈ l, Set.EqOn u 0 s
Tactic: rw [isEquivalent_zero_iff_eventually_zero, eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ u ~[l] const α c ↔ Tendsto u l (𝓝 c)
have simp : Tendsto (u - fun (x : α) ↦ c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)
Tactic: simp +unfoldPartialApp only [IsEquivalent, const, isLittleO_const_iff h]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ Tendsto (u - fun (x : α) ↦ c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)
have mp : Tendsto (u - fun (x : α) ↦ c) l (𝓝 0) → Tendsto u l (𝓝 c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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)
⊢ Tendsto (u - fun (x : α) ↦ c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)
have mpr : Tendsto u l (𝓝 c) → Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
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 u l (𝓝 c)
have this : Tendsto (fun (x : α) ↦ HSub.hSub (β := α → β) u (fun (x : α) ↦ c) x - -c) l (𝓝 (0 - -c))
Tactic: have := h.sub (tendsto_const_nhds (x := -c))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h_1 : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
have this : Tendsto (fun (x : α) ↦ u x - c) l (𝓝 (c - c))
Tactic: have := h.sub (tendsto_const_nhds (x := c))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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))
⊢ Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
have mpr : ∀ (this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x - c) l (𝓝 0)), Tendsto (u - fun (x : α) ↦ c) l (𝓝 0)
Tactic: rwa [sub_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
⊢ Tendsto u l (𝓝 c)
have inl : ∀ (hu : u ~[l] const α 0), Tendsto u l (𝓝 0)
Tactic: rcases em <| c = 0 with rfl | h
Cleared hypotheses: c, hu
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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)
⊢ Tendsto u l (𝓝 c)
have inr : ∀ (h : ¬c = 0), Tendsto u l (𝓝 c)
Tactic: rcases em <| c = 0 with rfl | h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
⊢ Tendsto v l (𝓝 c)
have pos : ∀ (h : c = 0), Tendsto v l (𝓝 c)
Tactic: by_cases h : c = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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)
⊢ Tendsto v l (𝓝 c)
have neg : ∀ (h : ¬c = 0), Tendsto v l (𝓝 c)
Tactic: by_cases h : c = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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
⊢ Tendsto v l (𝓝 c)
have pos : ∀ (hu : Tendsto u l (𝓝 0)), Tendsto v l (𝓝 0)
Tactic: subst c
Cleared hypotheses: c, hu, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
hu : Tendsto u l (𝓝 0)
⊢ Tendsto v l (𝓝 0)
have pos : ∀ (hu : IsLittleO (F := ℝ) l u fun (_x : α) ↦ 1), IsLittleO (F := ℝ) l v fun (_x : α) ↦ 1
Tactic: rw [← isLittleO_one_iff ℝ] at hu ⊢
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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
⊢ Tendsto v l (𝓝 c)
have neg : ∀ (hu : u ~[l] const α c) (h : ¬c = 0), v ~[l] const α c
Tactic: rw [← isEquivalent_const_iff_tendsto h] at hu ⊢
Cleared hypotheses: hu, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ IsLittleO (F := β) l (HSub.hSub (α := α → β) (fun (x : α) ↦ -u x) fun (x : α) ↦ -v x) fun (x : α) ↦ -v x
have h : ∀ (x : α), HSub.hSub (α := α → β) (β := α → β) (fun (x : α) ↦ -u x) (fun (x : α) ↦ -v x) x = -(u - v) x
Tactic: convert! huv.isLittleO.neg_left.neg_right
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
⊢ u ~[l] v ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
have rw : (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
Tactic: rw [IsEquivalent, isLittleO_iff_exists_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
⊢ (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
have mp : (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) → ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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
⊢ (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
have mpr : (∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v) → ∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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
have mp : Tendsto (φ + 1) l (𝓝 1)
Tactic: refine ⟨φ + 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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)
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
have mp₁ : u =ᶠ[l] (φ + 1) * v
Tactic: refine ⟨φ + 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v
have mpr : Tendsto (φ - 1) l (𝓝 0)
Tactic: refine ⟨φ - 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
mpr : Tendsto (φ - 1) l (𝓝 0)
⊢ ∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v
have mpr₁ : u - v =ᶠ[l] (φ - 1) * v
Tactic: refine ⟨φ - 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
⊢ (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
have mp : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 0)) (h : u - v =ᶠ[l] φ * v), Tendsto (φ + 1) l (𝓝 1)
Tactic: constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine ⟨φ + 1, ?_, ?_⟩; refine ⟨φ - 1, ?_, ?_⟩]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
mp : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 0)) (h : u - v =ᶠ[l] φ * v), Tendsto (φ + 1) l (𝓝 1)
⊢ (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
have mp₁ : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 0)) (h : u - v =ᶠ[l] φ * v), u =ᶠ[l] (φ + 1) * v
Tactic: constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine ⟨φ + 1, ?_, ?_⟩; refine ⟨φ - 1, ?_, ?_⟩]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
mp : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 0)) (h : u - v =ᶠ[l] φ * v), Tendsto (φ + 1) l (𝓝 1)
mp₁ : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 0)) (h : u - v =ᶠ[l] φ * v), u =ᶠ[l] (φ + 1) * v
⊢ (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
have mpr : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)) (h : u =ᶠ[l] φ * v), Tendsto (φ - 1) l (𝓝 0)
Tactic: constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine ⟨φ + 1, ?_, ?_⟩; refine ⟨φ - 1, ?_, ?_⟩]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
mp : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 0)) (h : u - v =ᶠ[l] φ * v), Tendsto (φ + 1) l (𝓝 1)
mp₁ : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 0)) (h : u - v =ᶠ[l] φ * v), u =ᶠ[l] (φ + 1) * v
mpr : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)) (h : u =ᶠ[l] φ * v), Tendsto (φ - 1) l (𝓝 0)
⊢ (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
have mpr₁ : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)) (h : u =ᶠ[l] φ * v), u - v =ᶠ[l] (φ - 1) * v
Tactic: constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine ⟨φ + 1, ?_, ?_⟩; refine ⟨φ - 1, ?_, ?_⟩]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
| 𝓝 1
have rw : 𝓝 (HAdd.hAdd (α := β) 0 1)
Tactic: rw [← zero_add (1 : β)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 1)
have mp : Tendsto (φ + 1) l (𝓝 (HAdd.hAdd (α := β) 0 1))
Tactic: conv in 𝓝 _ => rw [← zero_add (1 : β)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ u =ᶠ[l] (φ + 1) * v
have h₁ : ∀ (x : α), u x = (u - v) x + v x
Tactic: convert! h.fun_add (EventuallyEq.refl l v)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
h₁ : ∀ (x : α), u x = (u - v) x + v x
⊢ u =ᶠ[l] (φ + 1) * v
have h₂ : ∀ (x : α), ((φ + 1) * v) x = (φ * v) x + v x
Tactic: convert! h.fun_add (EventuallyEq.refl l v)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
| 𝓝 0
have rw : 𝓝 (HSub.hSub (α := β) 1 1)
Tactic: rw [← sub_self (1 : β)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)
have mpr : Tendsto (φ - 1) l (𝓝 (HSub.hSub (α := β) 1 1))
Tactic: conv in 𝓝 _ => rw [← sub_self (1 : β)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v
have h₁ : ∀ (x : α), ((φ - 1) * v) x = (φ * v) x - v x
Tactic: convert! h.fun_sub (EventuallyEq.refl l v)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
this : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
⊢ u ~[l] v
have rw : ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
Tactic: rw [isEquivalent_iff_exists_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
⊢ u ~[l] v
have suffices : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
Tactic: suffices ∀ᶠ x in l, v x = 0 → u x = 0 by
    rw [isEquivalent_iff_exists_eq_mul]
    exact ⟨u / v, huv, this.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
⊢ ∀ᶠ (x : α) in l, v x = 0 → u x = 0
have by_contra! : ∀ (h : ∃ᶠ (x : α) in l, v x = 0 ∧ u x ≠ 0), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
h : ∃ᶠ (x : α) in l, v x = 0 ∧ u x ≠ 0
⊢ False
have h₁ : ∃ᶠ (t : α) in l, (u / v) t = 0
Tactic: replace h : ∃ᶠ t in l, (u / v) t = 0 := h.mono fun x ⟨hv, hu⟩ ↦ by simp [hv]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ u ~[l] v ↔ Tendsto (u / v) l (𝓝 1)
have mp : u ~[l] v → Tendsto (u / v) l (𝓝 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
mp : u ~[l] v → Tendsto (u / v) l (𝓝 1)
⊢ u ~[l] v ↔ Tendsto (u / v) l (𝓝 1)
have mpr : Tendsto (u / v) l (𝓝 1) → u ~[l] v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
⊢ Tendsto (u / v) l (𝓝 1)
have this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ (u - v) x / v x) l (𝓝 0)
Tactic: have := hequiv.isLittleO.tendsto_div_nhds_zero
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ (u - v) x / v x) l (𝓝 0)
⊢ Tendsto (u / v) l (𝓝 1)
have this₁ : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)
Tactic: simp only [Pi.sub_apply, sub_div] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)
⊢ Tendsto (u / v) l (𝓝 1)
have key : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ v x / v x) l (𝓝 1)
Tactic: have key : Tendsto (fun x ↦ v x / v x) l (𝓝 1) :=
      (tendsto_congr' <| hz.mono fun x hnz ↦ @div_self _ _ (v x) hnz).mpr tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ v x / v x) l (𝓝 1)
⊢ Tendsto (u / v) l (𝓝 1)
have h : ∀ (x : α), (u / v) x = u x / v x - v x / v x + v x / v x
Tactic: convert! this.add key
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ v x / v x) l (𝓝 1)
h : ∀ (x : α), (u / v) x = u x / v x - v x / v x + v x / v x
⊢ Tendsto (u / v) l (𝓝 1)
have h₁ : 1 = HAdd.hAdd (α := β) 0 1
Tactic: convert! this.add key
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
⊢ IsEquivalent.{u_1, u_2} (E' := E) l (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x
have rcases : ∀ (φ : α → 𝕜) (hφ : Tendsto φ l (𝓝 1)) (habφ : a =ᶠ[l] φ * b),
  IsEquivalent.{u_1, u_2} (E' := E) l (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x
Tactic: rcases hab.exists_eq_mul with ⟨φ, hφ, habφ⟩