internlm/Lean-Github huggingface dataset:
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
case neg.refine_2
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∀ (n : ℕ), n ≠ 0 → f n = 0
x : ℝ
⊢ (fun x => LSeries f ↑x) x = 0 x
Tactic:
simp only [LSeries_congr x fun {n} ↦ H n, show (fun _ : ℕ ↦ (0 : ℂ)) = 0 from rfl,
  LSeries_zero, Pi.zero_apply]
Proof state after:
no goals
Theorem: LSeries_eq_zero_iff
Proof state before:
f : ℕ → ℂ
hf : f 0 = 0
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
Tactic:
by_cases h : abscissaOfAbsConv f = ⊤ <;> simp only [h, or_true, or_false, iff_true]
Proof state after:
case pos
f : ℕ → ℂ
hf : f 0 = 0
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0

case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0
Theorem: LSeries_eq_zero_iff
Proof state before:
case pos
f : ℕ → ℂ
hf : f 0 = 0
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0
Tactic:
exact LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h
Proof state after:
no goals
Theorem: LSeries_eq_zero_iff
Proof state before:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0
Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H ▸ LSeries_zero⟩
Proof state after:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0
Theorem: LSeries_eq_zero_iff
Proof state before:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0
Tactic:
convert (LSeries_eventually_eq_zero_iff'.mp ?_).resolve_right h
Proof state after:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0

case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] 0
Theorem: LSeries_eq_zero_iff
Proof state before:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0
Tactic:
refine ⟨fun H' _ _ ↦ by rw [H', Pi.zero_apply], fun H' ↦ ?_⟩
Proof state after:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f = 0
Theorem: LSeries_eq_zero_iff
Proof state before:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f = 0
Tactic:
ext ⟨- | m⟩
Proof state after:
case a.h.zero
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0

case a.h.succ
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
n✝ : ℕ
⊢ f (n✝ + 1) = 0 (n✝ + 1)
Theorem: LSeries_eq_zero_iff
Proof state before:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : f = 0
x✝¹ : ℕ
x✝ : x✝¹ ≠ 0
⊢ f x✝¹ = 0
Tactic:
rw [H', Pi.zero_apply]
Proof state after:
no goals
Theorem: LSeries_eq_zero_iff
Proof state before:
case a.h.zero
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0
Tactic:
simp only [zero_eq, hf, Pi.zero_apply]
Proof state after:
no goals
Theorem: LSeries_eq_zero_iff
Proof state before:
case a.h.succ
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
n✝ : ℕ
⊢ f (n✝ + 1) = 0 (n✝ + 1)
Tactic:
simp only [ne_eq, succ_ne_zero, not_false_eq_true, H', Pi.zero_apply]
Proof state after:
no goals
Theorem: LSeries_eq_zero_iff
Proof state before:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] 0
Tactic:
simp only [H, Pi.zero_apply]
Proof state after:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => 0) =ᶠ[Filter.atTop] 0
Theorem: LSeries_eq_zero_iff
Proof state before:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => 0) =ᶠ[Filter.atTop] 0
Tactic:
exact Filter.EventuallyEq.rfl
Proof state after:
no goals
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
⊢ (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
Tactic:
rw [EventuallyEq, eventually_atTop] at h ⊢
Proof state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ a, ∀ b ≥ a, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ a, ∀ b ≥ a, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
obtain ⟨x₀, hx₀⟩ := h
Proof state after:
case intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
case intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
obtain ⟨yf, hyf₁, hyf₂⟩ := exists_between hf
Proof state after:
case intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
case intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
obtain ⟨yg, hyg₁, hyg₂⟩ := exists_between hg
Proof state after:
case intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
case intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
lift yf to ℝ using ⟨hyf₂.ne, ((OrderBot.bot_le _).trans_lt hyf₁).ne'⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
case intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
lift yg to ℝ using ⟨hyg₂.ne, ((OrderBot.bot_le _).trans_lt hyg₁).ne'⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
refine ⟨max x₀ (max yf yg), fun x hx ↦ ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeries (f - g) ↑x = 0 x
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeries (f - g) ↑x = 0 x
Tactic:
have Hf : LSeriesSummable f x := by
  refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyf₁.trans_le ?_
  refine (le_max_left _ (yg : EReal)).trans <| (le_max_right (x₀ : EReal) _).trans ?_
  simpa only [max_le_iff, EReal.coe_le_coe_iff] using hx
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ LSeries (f - g) ↑x = 0 x
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ LSeries (f - g) ↑x = 0 x
Tactic:
have Hg : LSeriesSummable g x := by
  refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyg₁.trans_le ?_
  refine (le_max_right (yf : EReal) _).trans <| (le_max_right (x₀ : EReal) _).trans ?_
  simpa only [max_le_iff, EReal.coe_le_coe_iff] using hx
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
Hg : LSeriesSummable g ↑x
⊢ LSeries (f - g) ↑x = 0 x
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
Hg : LSeriesSummable g ↑x
⊢ LSeries (f - g) ↑x = 0 x
Tactic:
rw [LSeries_sub Hf Hg, hx₀ x <| (le_max_left ..).trans hx, sub_self, Pi.zero_apply]
Proof state after:
no goals
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeriesSummable f ↑x
Tactic:
refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyf₁.trans_le ?_
Proof state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ ↑yf ≤ ↑x
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ ↑yf ≤ ↑x
Tactic:
refine (le_max_left _ (yg : EReal)).trans <| (le_max_right (x₀ : EReal) _).trans ?_
Proof state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ max (↑x₀) (max ↑yf ↑yg) ≤ ↑x
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ max (↑x₀) (max ↑yf ↑yg) ≤ ↑x
Tactic:
simpa only [max_le_iff, EReal.coe_le_coe_iff] using hx
Proof state after:
no goals
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ LSeriesSummable g ↑x
Tactic:
refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyg₁.trans_le ?_
Proof state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ ↑yg ≤ ↑x
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ ↑yg ≤ ↑x
Tactic:
refine (le_max_right (yf : EReal) _).trans <| (le_max_right (x₀ : EReal) _).trans ?_
Proof state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ max (↑x₀) (max ↑yf ↑yg) ≤ ↑x
Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ max (↑x₀) (max ↑yf ↑yg) ≤ ↑x
Tactic:
simpa only [max_le_iff, EReal.coe_le_coe_iff] using hx
Proof state after:
no goals
Theorem: LSeries.eq_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
⊢ f n = g n
Tactic:
have hsub : (fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ) :=
  LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq hf hg h
Proof state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
⊢ f n = g n
Theorem: LSeries.eq_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
⊢ f n = g n
Tactic:
have ha : abscissaOfAbsConv (f - g) ≠ ⊤ :=
  lt_top_iff_ne_top.mp <| (abscissaOfAbsConv_sub_le f g).trans_lt <| max_lt hf hg
Proof state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
ha : abscissaOfAbsConv (f - g) ≠ ⊤
⊢ f n = g n
Theorem: LSeries.eq_of_LSeries_eventually_eq
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
ha : abscissaOfAbsConv (f - g) ≠ ⊤
⊢ f n = g n
Tactic:
simpa only [Pi.sub_apply, sub_eq_zero]
  using (LSeries_eventually_eq_zero_iff'.mp hsub).resolve_right ha n hn
Proof state after:
no goals
Theorem: LSeries_eq_iff_of_abscissaOfAbsConv_lt_top
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ f n = g n
Tactic:
refine eq_of_LSeries_eventually_eq hf hg ?_ hn
Proof state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x
Theorem: LSeries_eq_iff_of_abscissaOfAbsConv_lt_top
Proof state before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x
Tactic:
exact Filter.eventually_of_forall fun x ↦ congr_fun H x
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.prop_left
Proof state before:
P✝ : Sort u_1
A : Typ P✝
B : Bunch P✝
⊢ ¬PreEquiv (prop A) B
Tactic:
intro h
Proof state after:
P✝ : Sort u_1
A : Typ P✝
B : Bunch P✝
h : PreEquiv (prop A) B
⊢ False
Theorem: BunchImpl.PreEquiv.prop_left
Proof state before:
P✝ : Sort u_1
A : Typ P✝
B : Bunch P✝
h : PreEquiv (prop A) B
⊢ False
Tactic:
generalize hA' : prop A = A' at h
Proof state after:
P✝ : Sort u_1
A : Typ P✝
B A' : Bunch P✝
hA' : prop A = A'
h : PreEquiv A' B
⊢ False
Theorem: BunchImpl.PreEquiv.prop_left
Proof state before:
P✝ : Sort u_1
A : Typ P✝
B A' : Bunch P✝
hA' : prop A = A'
h : PreEquiv A' B
⊢ False
Tactic:
induction h <;> simp at hA'
Proof state after:
case subbunch
P✝ : Sort u_1
A : Typ P✝
B A' : Bunch P✝
h✝ : BunchWithHole P✝
b1✝ b2✝ : Bunch P✝
a✝ : PreEquiv b1✝ b2✝
a_ih✝ : prop A = b1✝ → False
hA' : h✝ = BunchWithHole.hole ∧ b1✝ = prop A
⊢ False
Theorem: BunchImpl.PreEquiv.prop_left
Proof state before:
case subbunch
P✝ : Sort u_1
A : Typ P✝
B A' : Bunch P✝
h✝ : BunchWithHole P✝
b1✝ b2✝ : Bunch P✝
a✝ : PreEquiv b1✝ b2✝
a_ih✝ : prop A = b1✝ → False
hA' : h✝ = BunchWithHole.hole ∧ b1✝ = prop A
⊢ False
Tactic:
rcases hA' with ⟨rfl,rfl⟩
Proof state after:
case subbunch.intro
P✝ : Sort u_1
A : Typ P✝
B A' b2✝ : Bunch P✝
a✝ : PreEquiv (prop A) b2✝
a_ih✝ : prop A = prop A → False
⊢ False
Theorem: BunchImpl.PreEquiv.prop_left
Proof state before:
case subbunch.intro
P✝ : Sort u_1
A : Typ P✝
B A' b2✝ : Bunch P✝
a✝ : PreEquiv (prop A) b2✝
a_ih✝ : prop A = prop A → False
⊢ False
Tactic:
simp at *
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.sunit_left
Proof state before:
P✝ : Sort u_1
B : Bunch P✝
⊢ ¬PreEquiv sunit B
Tactic:
intro h
Proof state after:
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv sunit B
⊢ False
Theorem: BunchImpl.PreEquiv.sunit_left
Proof state before:
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv sunit B
⊢ False
Tactic:
generalize hA' : sunit = A' at h
Proof state after:
P✝ : Sort u_1
B A' : Bunch P✝
hA' : sunit = A'
h : PreEquiv A' B
⊢ False
Theorem: BunchImpl.PreEquiv.sunit_left
Proof state before:
P✝ : Sort u_1
B A' : Bunch P✝
hA' : sunit = A'
h : PreEquiv A' B
⊢ False
Tactic:
induction h <;> simp at hA'
Proof state after:
case subbunch
P✝ : Sort u_1
B A' : Bunch P✝
h✝ : BunchWithHole P✝
b1✝ b2✝ : Bunch P✝
a✝ : PreEquiv b1✝ b2✝
a_ih✝ : sunit = b1✝ → False
hA' : h✝ = BunchWithHole.hole ∧ b1✝ = sunit
⊢ False
Theorem: BunchImpl.PreEquiv.sunit_left
Proof state before:
case subbunch
P✝ : Sort u_1
B A' : Bunch P✝
h✝ : BunchWithHole P✝
b1✝ b2✝ : Bunch P✝
a✝ : PreEquiv b1✝ b2✝
a_ih✝ : sunit = b1✝ → False
hA' : h✝ = BunchWithHole.hole ∧ b1✝ = sunit
⊢ False
Tactic:
rcases hA' with ⟨rfl,rfl⟩
Proof state after:
case subbunch.intro
P✝ : Sort u_1
B A' b2✝ : Bunch P✝
a✝ : PreEquiv sunit b2✝
a_ih✝ : sunit = sunit → False
⊢ False
Theorem: BunchImpl.PreEquiv.sunit_left
Proof state before:
case subbunch.intro
P✝ : Sort u_1
B A' b2✝ : Bunch P✝
a✝ : PreEquiv sunit b2✝
a_ih✝ : sunit = sunit → False
⊢ False
Tactic:
simp at *
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.cunit_left
Proof state before:
P✝ : Sort u_1
B : Bunch P✝
⊢ ¬PreEquiv cunit B
Tactic:
intro h
Proof state after:
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv cunit B
⊢ False
Theorem: BunchImpl.PreEquiv.cunit_left
Proof state before:
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv cunit B
⊢ False
Tactic:
generalize hA' : cunit = A' at h
Proof state after:
P✝ : Sort u_1
B A' : Bunch P✝
hA' : cunit = A'
h : PreEquiv A' B
⊢ False
Theorem: BunchImpl.PreEquiv.cunit_left
Proof state before:
P✝ : Sort u_1
B A' : Bunch P✝
hA' : cunit = A'
h : PreEquiv A' B
⊢ False
Tactic:
induction h <;> simp at hA'
Proof state after:
case subbunch
P✝ : Sort u_1
B A' : Bunch P✝
h✝ : BunchWithHole P✝
b1✝ b2✝ : Bunch P✝
a✝ : PreEquiv b1✝ b2✝
a_ih✝ : cunit = b1✝ → False
hA' : h✝ = BunchWithHole.hole ∧ b1✝ = cunit
⊢ False
Theorem: BunchImpl.PreEquiv.cunit_left
Proof state before:
case subbunch
P✝ : Sort u_1
B A' : Bunch P✝
h✝ : BunchWithHole P✝
b1✝ b2✝ : Bunch P✝
a✝ : PreEquiv b1✝ b2✝
a_ih✝ : cunit = b1✝ → False
hA' : h✝ = BunchWithHole.hole ∧ b1✝ = cunit
⊢ False
Tactic:
rcases hA' with ⟨rfl,rfl⟩
Proof state after:
case subbunch.intro
P✝ : Sort u_1
B A' b2✝ : Bunch P✝
a✝ : PreEquiv cunit b2✝
a_ih✝ : cunit = cunit → False
⊢ False
Theorem: BunchImpl.PreEquiv.cunit_left
Proof state before:
case subbunch.intro
P✝ : Sort u_1
B A' b2✝ : Bunch P✝
a✝ : PreEquiv cunit b2✝
a_ih✝ : cunit = cunit → False
⊢ False
Tactic:
simp at *
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.prop_right
Proof state before:
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
⊢ PreEquiv B (prop A) ↔ B = (cunit ,ᵇ prop A) ∨ B = (prop A ,ᵇ cunit) ∨ B = (sunit ;ᵇ prop A) ∨ B = (prop A ;ᵇ sunit)
Tactic:
constructor
Proof state after:
case mp
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
⊢ PreEquiv B (prop A) → B = (cunit ,ᵇ prop A) ∨ B = (prop A ,ᵇ cunit) ∨ B = (sunit ;ᵇ prop A) ∨ B = (prop A ;ᵇ sunit)

case mpr
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
⊢ B = (cunit ,ᵇ prop A) ∨ B = (prop A ,ᵇ cunit) ∨ B = (sunit ;ᵇ prop A) ∨ B = (prop A ;ᵇ sunit) → PreEquiv B (prop A)
Theorem: BunchImpl.PreEquiv.prop_right
Proof state before:
case mp
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
⊢ PreEquiv B (prop A) → B = (cunit ,ᵇ prop A) ∨ B = (prop A ,ᵇ cunit) ∨ B = (sunit ;ᵇ prop A) ∨ B = (prop A ;ᵇ sunit)
Tactic:
intro h
Proof state after:
case mp
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
h : PreEquiv B (prop A)
⊢ B = (cunit ,ᵇ prop A) ∨ B = (prop A ,ᵇ cunit) ∨ B = (sunit ;ᵇ prop A) ∨ B = (prop A ;ᵇ sunit)
Theorem: BunchImpl.PreEquiv.prop_right
Proof state before:
case mp
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
h : PreEquiv B (prop A)
⊢ B = (cunit ,ᵇ prop A) ∨ B = (prop A ,ᵇ cunit) ∨ B = (sunit ;ᵇ prop A) ∨ B = (prop A ;ᵇ sunit)
Tactic:
generalize hA' : prop A = A' at h
Proof state after:
case mp
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
A' : Bunch P✝
hA' : prop A = A'
h : PreEquiv B A'
⊢ B = (cunit ,ᵇ A') ∨ B = (A' ,ᵇ cunit) ∨ B = (sunit ;ᵇ A') ∨ B = (A' ;ᵇ sunit)
Theorem: BunchImpl.PreEquiv.prop_right
Proof state before:
case mp
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
A' : Bunch P✝
hA' : prop A = A'
h : PreEquiv B A'
⊢ B = (cunit ,ᵇ A') ∨ B = (A' ,ᵇ cunit) ∨ B = (sunit ;ᵇ A') ∨ B = (A' ;ᵇ sunit)
Tactic:
induction h <;> simp_all
Proof state after:
no goals