awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 < g y) x} x →
        Membership.mem (γ := Set ℕ)
          {x : ℕ |
            Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 ≤ f y) x} x →
              Membership.mem (γ := Set ℕ)
                {x : ℕ |
                  Membership.mem (γ := Set ℕ)
                      {x : ℕ |
                        (fun (n₀ : ℕ) ↦
                            ∃ (C₀ : ℝ),
                              ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n)
                          x}
                      x →
                    Membership.mem (γ := Set ℕ)
                      {x : ℕ |
                        (fun (n₀ : ℕ) ↦
                            ∃ (C₀ : ℝ),
                              ∀ᶠ (n : ℕ) in atTop,
                                ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖)
                          x}
                      x}
                x}
          x}
    a
Tactic: case hrec =>
    filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec
    obtain ⟨C₀, hnrec⟩ := hnrec
    refine ⟨C₀, ?_⟩
    filter_upwards [hnrec, eventually_ge_atTop n₀]
    grind [Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 < g y) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 ≤ f y) x} x →
                Membership.mem (γ := Set ℕ)
                  {x : ℕ |
                    Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n)
                            x}
                        x →
                      Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop,
                                  ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖)
                            x}
                        x}
                  x}
            x}
      a
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
have h₁ : ∀ (a : ℕ),
  (∀ (y : ℕ), a ≤ y → 0 < g y) →
    (∀ (y : ℕ), a ≤ y → 0 ≤ f y) →
      (∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico a n, f m ≤ C * g m) → f n ≤ C * g n) →
        ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico a n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
Tactic: case hrec =>
    filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec
    obtain ⟨C₀, hnrec⟩ := hnrec
    refine ⟨C₀, ?_⟩
    filter_upwards [hnrec, eventually_ge_atTop n₀]
    grind [Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 < g y) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 ≤ f y) x} x →
                Membership.mem (γ := Set ℕ)
                  {x : ℕ |
                    Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n)
                            x}
                        x →
                      Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop,
                                  ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖)
                            x}
                        x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y)
    (hnrec : ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
have h₃ : ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y) (C₀ : ℝ)
  (hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
  ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
Tactic: case hrec =>
    filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec
    obtain ⟨C₀, hnrec⟩ := hnrec
    refine ⟨C₀, ?_⟩
    filter_upwards [hnrec, eventually_ge_atTop n₀]
    grind [Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 < g y) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 ≤ f y) x} x →
                Membership.mem (γ := Set ℕ)
                  {x : ℕ |
                    Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n)
                            x}
                        x →
                      Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop,
                                  ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖)
                            x}
                        x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y)
    (hnrec : ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
h₃ :
  ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y) (C₀ : ℝ)
    (hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
have h₄ : ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y) (C₀ : ℝ)
  (hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
  ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
Tactic: case hrec =>
    filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec
    obtain ⟨C₀, hnrec⟩ := hnrec
    refine ⟨C₀, ?_⟩
    filter_upwards [hnrec, eventually_ge_atTop n₀]
    grind [Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 < g y) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 ≤ f y) x} x →
                Membership.mem (γ := Set ℕ)
                  {x : ℕ |
                    Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n)
                            x}
                        x →
                      Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop,
                                  ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖)
                            x}
                        x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y)
    (hnrec : ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
h₃ :
  ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y) (C₀ : ℝ)
    (hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
h₄ :
  ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y) (C₀ : ℝ)
    (hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
    ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
have h₅ : ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y) (C₀ : ℝ)
  (hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n) (a : ℕ),
  (∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ a, f m ≤ C * g m) → f a ≤ C * g a) →
    n₀ ≤ a → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ a, ‖f m‖ ≤ C * ‖g m‖) → ‖f a‖ ≤ C * ‖g a‖
Tactic: case hrec =>
    filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec
    obtain ⟨C₀, hnrec⟩ := hnrec
    refine ⟨C₀, ?_⟩
    filter_upwards [hnrec, eventually_ge_atTop n₀]
    grind [Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
F : Type u_1
ι : Type u_2
inst : NormedRing F
inst_1 : NormMulClass F
inst_2 : NormOneClass F
inst_3 : CompleteSpace F
f g : ι → F
hf : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
c : F
hg : Tendsto g cofinite (𝓝 c)
⊢ Summable.{u_1, u_2} (α := F) fun (n : ι) ↦ f n * g n
have apply : IsBigO.{u_2, u_1, 0} (E := F) (F := ℝ) cofinite (fun (n : ι) ↦ f n * g n) fun (n : ι) ↦ ‖f n‖
Tactic: apply summable_of_isBigO hf
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
⊢ Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)
have this : ContinuousAt (↑e : α → β) ((↑e.symm : β → α) b)
Tactic: have := e.continuousAt (e.map_target hb)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
this : ContinuousAt (↑e : α → β) ((↑e.symm : β → α) b)
⊢ Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)
have rwa : ∀ (this : Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 ((↑e : α → β) ((↑e.symm : β → α) b)))),
  Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)
Tactic: rwa [ContinuousAt, e.rightInvOn hb] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
this : ContinuousAt (↑e : α → β) ((↑e.symm : β → α) b)
rwa :
  ∀ (this : Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 ((↑e : α → β) ((↑e.symm : β → α) b)))),
    Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)
⊢ Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)
have rwa₁ : ∀ (this : Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)), Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)
Tactic: rwa [ContinuousAt, e.rightInvOn hb] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ f =O[𝓝 b] g ↔ (f ∘ (↑e : α → β)) =O[𝓝 ((↑e.symm : β → α) b)] (g ∘ (↑e : α → β))
have simp : (∃ (c : ℝ), IsBigOWith c (𝓝 b) f g) ↔
  ∃ (c : ℝ), IsBigOWith c (𝓝 ((↑e.symm : β → α) b)) (f ∘ (↑e : α → β)) (g ∘ (↑e : α → β))
Tactic: simp only [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ f =o[𝓝 b] g ↔ (f ∘ (↑e : α → β)) =o[𝓝 ((↑e.symm : β → α) b)] (g ∘ (↑e : α → β))
have simp : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
  ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 ((↑e.symm : β → α) b)) (f ∘ (↑e : α → β)) (g ∘ (↑e : α → β))
Tactic: simp only [IsLittleO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ f =O[𝓝 b] g ↔
    IsBigO.{u_1, u_3, u_4} (α := α) (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
      (g ∘ (⇑e : (a : α) → β) : α → F)
have simp : (∃ (c : ℝ), IsBigOWith c (𝓝 b) f g) ↔
  ∃ (c : ℝ),
    IsBigOWith.{u_1, u_3, u_4} (α := α) c (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
      (g ∘ (⇑e : (a : α) → β) : α → F)
Tactic: simp only [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ f =o[𝓝 b] g ↔
    IsLittleO.{u_1, u_3, u_4} (α := α) (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
      (g ∘ (⇑e : (a : α) → β) : α → F)
have simp : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
  ∀ ⦃c : ℝ⦄,
    0 < c →
      IsBigOWith.{u_1, u_3, u_4} (α := α) c (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
        (g ∘ (⇑e : (a : α) → β) : α → F)
Tactic: simp only [IsLittleO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
c : F
inst_1 : SeminormedAddGroup E
inst_2 : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
⊢ IsBigOWith.{u_1, u_2, u_3} (F := F) (sSup (Norm.norm '' f '' s) / ‖c‖) (𝓟 s) f fun (x : α) ↦ c
have rw : ∀ x ∈ s, ‖f x‖ ≤ sSup (Norm.norm '' f '' s)
Tactic: rw [isBigOWith_principal, div_mul_cancel₀ _ hc]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
⊢ IsBigOWith.{u_1, u_3, u_2} (E := F) (‖c‖ / sInf (Norm.norm '' f '' s)) (𝓟 s) (fun (x : α) ↦ c) f
have refine : ∀ (x : α) (hx : x ∈ s), ‖c‖ ≤ ‖c‖ / sInf (Norm.norm '' f '' s) * ‖f x‖
Tactic: refine isBigOWith_principal.mpr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ / sInf (Norm.norm '' f '' s) * ‖f x‖
have rw : ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' f '' s))
Tactic: rw [mul_comm_div]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' f '' s))
have hs₁ : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
Tactic: replace hs := hs.image_of_continuousOn hf |>.image continuous_norm
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' f '' s))
have h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
Tactic: have h_sInf := hs.isGLB_sInf <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' f '' s))
have refine : 0 < sInf (Norm.norm '' f '' s)
Tactic: refine le_mul_of_one_le_right (norm_nonneg c) <| (one_le_div ?_).mpr <|
    h_sInf.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
⊢ 0 < sInf (Norm.norm '' f '' s)
have obtain : ∀ (w : E) (hnormCx : Eq (α := ℝ) ((fun (a : E) ↦ ‖a‖) w) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))) (x : α) (hx : x ∈ s)
  (hCx : f x = w), 0 < sInf (Norm.norm '' f '' s)
Tactic: obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x_1 : α
hx_1 : x_1 ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
w : E
hnormCx : Eq (α := ℝ) ((fun (a : E) ↦ ‖a‖) w) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
x : α
hx : x ∈ s
hCx : f x = w
⊢ 0 < sInf (Norm.norm '' f '' s)
have rw : LT.lt (α := ℝ) 0 ((fun (a : E) ↦ ‖a‖) (f x))
Tactic: rw [← hnormCx, ← hCx]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
l : Filter ι
ε : ι → 𝕜
f : ι → E
hε : Tendsto ε l (𝓝 0)
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
⊢ Tendsto (ε • f) l (𝓝 0)
have rw : ∀ (hε : IsLittleO (F := 𝕜) l ε fun (_x : ι) ↦ 1) (hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)),
  IsLittleO.{u_1, u_3, u_2} (F := 𝕜) l (ε • f) fun (_x : ι) ↦ 1
Tactic: rw [← isLittleO_one_iff 𝕜] at hε ⊢
Cleared hypotheses: hε, hf
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ v n
n : ℕ
u_v : u n ≤ v n
⊢ u n / (↑n : EReal) ≤ v n / (↑n : EReal)
have h₁ : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
⊢ linearGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)
have rw : (∀ y > a, ∃ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)
Tactic: rw [linearGrowthInf, liminf_le_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)
have refine : ∀ b > a, ∀ n ≥ 1, u n / (↑n : EReal) ≤ b ↔ u n ≤ b * (↑n : EReal)
Tactic: refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
⊢ LT.lt (α := EReal) 0 (↑n : EReal)
have norm_cast : 0 < n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
⊢ u n / (↑n : EReal) ≤ b ↔ u n ≤ b * (↑n : EReal)
have rw : u n ≤ (↑n : EReal) * b ↔ u n ≤ b * (↑n : EReal)
Tactic: rw [div_le_iff_le_mul (by norm_cast) (natCast_ne_top n), mul_comm _ b]