awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : f₂ =o[l] g₂
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
have simp : ∀ (h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂) ⦃c : ℝ⦄,
  0 < c → IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
Tactic: simp only [IsLittleO_def] at *
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
have rcases : ∀ (c' : ℝ) (c'pos : c' > 0) (hc' : IsBigOWith c' l f₁ g₁),
  IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
Tactic: rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =o[l] g₁
h₂ : f₂ =O[l] g₂
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
have simp : ∀ (h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁) ⦃c : ℝ⦄,
  0 < c → IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
Tactic: simp only [IsLittleO_def] at *
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
have rcases : ∀ (c' : ℝ) (c'pos : c' > 0) (hc' : IsBigOWith c' l f₂ g₂),
  IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
Tactic: rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c : ℝ
l : Filter α
inst_3 : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℝ) 0 (norm.{u_13} (E := R) 1) fun (n : ℕ) ↦ c ^ (n + 1)) l
    (fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 0) fun (x : α) ↦ HPow.hPow (β := ℕ) (g x) 0
have this : Nontrivial S
Tactic: have : Nontrivial S := NormOneClass.nontrivial
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c c' : ℝ
l : Filter α
inst_3 : NormOneClass S
n : ℕ
f : α → S
g : α → R
h : IsBigOWith c l (f ^ n) (g ^ n)
hn : n ≠ 0
hc : c ≤ c' ^ n
hc' : 0 ≤ c'
x : α
hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖
⊢ c' ^ n * ‖g x ^ n‖ ≤ c' ^ n * ‖g x‖ ^ n
have hbc : ‖g x ^ n‖ ≤ ‖g x‖ ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
hn : 0 < n
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n) fun (x : α) ↦ g x ^ n
have obtain : ∀ (n : ℕ) (hn : 0 < n.succ),
  IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ (n + 1).succ) fun (x : α) ↦ g x ^ (n + 1).succ
have h₁ : ∀ (x : α), f x ^ (n + 1).succ = f x ^ n.succ * f x
Tactic: convert! ihn.mul h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
h₁ : ∀ (x : α), f x ^ (n + 1).succ = f x ^ n.succ * f x
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ (n + 1).succ) fun (x : α) ↦ g x ^ (n + 1).succ
have h₂ : ∀ (x : α), g x ^ (n + 1).succ = g x ^ n.succ * g x
Tactic: convert! ihn.mul h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
have zero : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ Nat.succ 0) fun (x : α) ↦ g x ^ Nat.succ 0
Tactic: induction n with
  | zero => simpa only [pow_one]
  | succ n ihn => convert! ihn.mul h <;> simp [pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
zero : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ Nat.succ 0) fun (x : α) ↦ g x ^ Nat.succ 0
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
have succ : ∀ (n : ℕ)
  (ihn : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ),
  IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ (n + 1).succ) fun (x : α) ↦ g x ^ (n + 1).succ
Tactic: induction n with
  | zero => simpa only [pow_one]
  | succ n ihn => convert! ihn.mul h <;> simp [pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ IsBigOWith.{u_1, u_16, u_15} (E := 𝕜') (F := 𝕜) c l (fun (x : α) ↦ (g x)⁻¹) fun (x : α) ↦ (f x)⁻¹
have refine : ∀ (x : α) (h₀ : f x = 0 → g x = 0) (hle : ‖f x‖ ≤ c * ‖g x‖), ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
Tactic: refine IsBigOWith.of_bound (h.bound.mp (h₀.mono fun x h₀ hle => ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀_1 : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
have inl : ∀ (hx : f x = 0), ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
Tactic: rcases eq_or_ne (f x) 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀_1 : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
inl : ∀ (hx : f x = 0), ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
have inr : ∀ (hx : f x ≠ 0), ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
Tactic: rcases eq_or_ne (f x) 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀_1 : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
have hc : 0 < c
Tactic: have hc : 0 < c := pos_of_mul_pos_left ((norm_pos_iff.2 hx).trans_le hle) (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀_1 : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
hc : 0 < c
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
have hle₁ : (c * ‖g x‖)⁻¹ ≤ ‖f x‖⁻¹
Tactic: replace hle := inv_anti₀ (norm_pos_iff.2 hx) hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s_1 : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g),
    IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ s, C i) l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
h : ∀ i_1 ∈ Finset.cons i s is, IsBigOWith (C i_1) l (A i_1) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ Finset.cons i s is, C i) l (fun (x : α) ↦ ∑ i ∈ Finset.cons i s is, A i x)
    g
have cons : ∀ (h : IsBigOWith (C i) l (A i) g ∧ ∀ x ∈ s, IsBigOWith (C x) l (A x) g),
  IsBigOWith.{u_1, u_6, u_4} (E := E') (C i + ∑ i ∈ s, C i) l (fun (x : α) ↦ A i x + ∑ i ∈ s, A i x) g
Tactic: simp only [Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ s, C i) l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBigOWith (C i) l (A i) g),
  IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ ∅, C i) l (fun (x : α) ↦ ∑ i ∈ ∅, A i x) g
Tactic: induction s using Finset.cons_induction with
  | empty => simp only [isBigOWith_zero', Finset.sum_empty]
  | cons i s is IH =>
    simp only [Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
    exact h.1.add (IH h.2)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBigOWith (C i) l (A i) g),
    IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ ∅, C i) l (fun (x : α) ↦ ∑ i ∈ ∅, A i x) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ s, C i) l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
have cons : ∀ (i : ι) (s : Finset ι) (is : i ∉ s)
  (IH :
    ∀ (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g),
      IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ s, C i) l (fun (x : α) ↦ ∑ i ∈ s, A i x) g)
  (h : ∀ i_1 ∈ Finset.cons i s is, IsBigOWith (C i_1) l (A i_1) g),
  IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ Finset.cons i s is, C i) l (fun (x : α) ↦ ∑ i ∈ Finset.cons i s is, A i x)
    g
Tactic: induction s using Finset.cons_induction with
  | empty => simp only [isBigOWith_zero', Finset.sum_empty]
  | cons i s is IH =>
    simp only [Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
    exact h.1.add (IH h.2)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =O[l] g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
have simp : ∀ (h : ∀ i ∈ s, ∃ (c : ℝ), IsBigOWith c l (A i) g),
  ∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
Tactic: simp only [IsBigO_def] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, ∃ (c : ℝ), IsBigOWith c l (A i) g
⊢ ∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
have choose! : ∀ (C : (i : ι) → ℝ) (hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) g),
  ∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
Tactic: choose! C hC using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =o[l] g'
⊢ IsLittleO.{u_1, u_6, u_7} (E := E') l (fun (x : α) ↦ ∑ i ∈ s, A i x) g'
have simp : IsLittleO.{u_1, u_6, u_7} (E := E') l (fun (x : α) ↦ (∑ c ∈ s, A c) x) g'
Tactic: simp only [← Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑s : Set ι))) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦
    ∑ i ∈ s, ‖B i H‖
have inl : ∀ (hAB : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBigOWith (C i) l (A i) (B i)),
  IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑∅ : Set ι))) l (fun (H : α) ↦ ∑ i ∈ ∅, A i H) fun (H : α) ↦
    ∑ i ∈ ∅, ‖B i H‖
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s, hAB
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
inl :
  ∀ (hAB : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBigOWith (C i) l (A i) (B i)),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑∅ : Set ι))) l (fun (H : α) ↦ ∑ i ∈ ∅, A i H)
      fun (H : α) ↦ ∑ i ∈ ∅, ‖B i H‖
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑s : Set ι))) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦
    ∑ i ∈ s, ‖B i H‖
have inr : ∀ (hs : s.Nonempty),
  IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑s : Set ι))) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦
    ∑ i ∈ s, ‖B i H‖
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
hs : s.Nonempty
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑s : Set ι))) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦
    ∑ i ∈ s, ‖B i H‖
have inr : ∀ (hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖),
  ∀ᶠ (x : α) in l, norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
Tactic: simp only [IsBigOWith_def] at *
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ∀ᶠ (x : α) in l, norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
have h : ∀ (x : α) (hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖),
  norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
Tactic: filter_upwards [(eventually_all_finset s).mpr hAB]
    with x hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ LE.le (α := ℝ) (∑ i ∈ s, C i * ‖B i x‖) (∑ i ∈ s, sSup (C '' (↑s : Set ι)) * ‖B i x‖)
have refine : ∀ i ∈ s, C i * ‖B i x‖ ≤ sSup (C '' (↑s : Set ι)) * ‖B i x‖
Tactic: refine Finset.sum_le_sum ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ C j * ‖B j x‖ ≤ sSup (C '' (↑s : Set ι)) * ‖B j x‖
have hbc : C j ≤ sSup (C '' (↑s : Set ι))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ C j ≤ sSup (C '' (↑s : Set ι))
have hbc : ∃ b ∈ s, C j ≤ C b
Tactic: rw [← s.sup'_eq_csSup_image hs, Finset.le_sup'_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
w : ι
⊢ ∃ b ∈ s, C j ≤ C b
have h : j ∈ s ∧ C j ≤ C j
Tactic: use j
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ sSup (C '' (↑s : Set ι)) * ∑ i ∈ s, ‖B i x‖ = sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
have e_a : ∑ i ∈ s, ‖B i x‖ = norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ∑ i ∈ s, ‖B i x‖ = norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
have e_a : Eq (α := ℝ) (∑ i ∈ s, ‖B i x‖) (∑ i ∈ s, ‖B i x‖)
Tactic: rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
have i : LE.le (α := ℝ) (∑ i ∈ s, C i * ‖B i x‖) (∑ i ∈ s, sSup (C '' (↑s : Set ι)) * ‖B i x‖)
Tactic: calc
    ‖∑ i ∈ s, A i x‖ ≤ ∑ i ∈ s, ‖A i x‖ := norm_sum_le ..
    _ ≤ ∑ i ∈ s, C i * ‖B i x‖ := Finset.sum_le_sum (fun j hj ↦ hx j hj)
    _ ≤ ∑ i ∈ s, sSup (C '' s) * ‖B i x‖ := by
        refine Finset.sum_le_sum ?_
        intro j hj; gcongr
        rw [← s.sup'_eq_csSup_image hs, Finset.le_sup'_iff]; use j
    _ = sSup (C '' s) * ∑ i ∈ s, ‖B i x‖ := (Finset.mul_sum ..).symm
    _ = sSup (C '' s) * ‖∑ i ∈ s, ‖B i x‖‖ := by
      congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
i : LE.le (α := ℝ) (∑ i ∈ s, C i * ‖B i x‖) (∑ i ∈ s, sSup (C '' (↑s : Set ι)) * ‖B i x‖)
⊢ norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
have i₁ : sSup (C '' (↑s : Set ι)) * ∑ i ∈ s, ‖B i x‖ = sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
Tactic: calc
    ‖∑ i ∈ s, A i x‖ ≤ ∑ i ∈ s, ‖A i x‖ := norm_sum_le ..
    _ ≤ ∑ i ∈ s, C i * ‖B i x‖ := Finset.sum_le_sum (fun j hj ↦ hx j hj)
    _ ≤ ∑ i ∈ s, sSup (C '' s) * ‖B i x‖ := by
        refine Finset.sum_le_sum ?_
        intro j hj; gcongr
        rw [← s.sup'_eq_csSup_image hs, Finset.le_sup'_iff]; use j
    _ = sSup (C '' s) * ∑ i ∈ s, ‖B i x‖ := (Finset.mul_sum ..).symm
    _ = sSup (C '' s) * ‖∑ i ∈ s, ‖B i x‖‖ := by
      congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, A i =O[l] B i
⊢ IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
have simp : ∀ (hAB : ∀ i ∈ s, ∃ (c : ℝ), IsBigOWith c l (A i) (B i)),
  ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
Tactic: simp only [IsBigO_def] at *
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, ∃ (c : ℝ), IsBigOWith c l (A i) (B i)
⊢ ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
have choose! : ∀ (C : (i : ι) → ℝ) (hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)),
  ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
Tactic: choose! C hC using hAB
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s_1 : Finset ι
B : ι → α → ℝ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (hAB : ∀ i ∈ s, A i =o[l] B i),
    IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ Finset.cons i s his, A i H) fun (H : α) ↦
    ∑ i ∈ Finset.cons i s his, ‖B i H‖
have cons : IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ A i H + ∑ i ∈ s, A i H) fun (H : α) ↦
  ‖B i H‖ + ∑ i ∈ s, ‖B i H‖
Tactic: simp_rw [Finset.sum_cons]