awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
pos : ∀ (h : abscissaOfAbsConv f = ⊤), LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
have neg : ∀ (h : ¬abscissaOfAbsConv f = ⊤), LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
Tactic: by_cases h : abscissaOfAbsConv f = ⊤
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
have neg : LSeries f = 0 ↔ f = 0
Tactic: simp only [h, or_false]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0
have neg : ∀ (H : LSeries f = 0), f = 0
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ H ▸ LSeries_zero⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0
have a : f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0
Tactic: convert! (LSeries_eventually_eq_zero_iff'.mp ?_).resolve_right h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
a : f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f = 0
have neg : Filter.EventuallyEq (β := ℂ) Filter.atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
Tactic: convert! (LSeries_eventually_eq_zero_iff'.mp ?_).resolve_right h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : f = 0
x : ℕ
h_1 : x ≠ 0
⊢ f x = 0
have rw : Eq (α := ℂ) (0 x) 0
Tactic: rw [H', Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : f = 0
x : ℕ
h_1 : x ≠ 0
rw : Eq (α := ℂ) (0 x) 0
⊢ f x = 0
have rw₁ : Eq (α := ℂ) 0 0
Tactic: rw [H', Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0
have a : ∀ (H' : ∀ (n : ℕ), n ≠ 0 → f n = 0), f = 0
Tactic: refine ⟨fun H' _ _ ↦ by rw [H', Pi.zero_apply], fun H' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f = 0
have a : f 0 = 0 0
Tactic: ext (- | m)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
a : f 0 = 0 0
⊢ f = 0
have a₁ : ∀ (m : ℕ), f (m + 1) = 0 (m + 1)
Tactic: ext (- | m)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries (f - g) (↑x : ℂ)) 0
have rw : ∀ (h : ∃ (a : ℝ), ∀ b ≥ a, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)), ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
Tactic: rw [EventuallyEq, eventually_atTop] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
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
have obtain : ∀ (x₀ : ℝ) (hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)), ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
Tactic: obtain ⟨x₀, hx₀⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
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
have obtain : ∀ (yf : EReal) (hyf₁ : abscissaOfAbsConv f < yf) (hyf₂ : yf < ⊤), ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
Tactic: obtain ⟨yf, hyf₁, hyf₂⟩ := exists_between hf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
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
have obtain : ∀ (yg : EReal) (hyg₁ : abscissaOfAbsConv g < yg) (hyg₂ : yg < ⊤), ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
Tactic: obtain ⟨yg, hyg₁, hyg₂⟩ := exists_between hg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
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
have lift : ∀ (yf : ℝ) (hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)) (hyf₂ : (↑yf : EReal) < ⊤),
  ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
Tactic: lift yf to ℝ using ⟨hyf₂.ne, ((OrderBot.bot_le _).trans_lt hyf₁).ne'⟩
Cleared hypotheses: yf, hyf₁, hyf₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
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 : EReal)
hyf₂ : (↑yf : EReal) < ⊤
⊢ ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
have lift : ∀ (yg : ℝ) (hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)) (hyg₂ : (↑yg : EReal) < ⊤),
  ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
Tactic: lift yg to ℝ using ⟨hyg₂.ne, ((OrderBot.bot_le _).trans_lt hyg₁).ne'⟩
Cleared hypotheses: yg, hyg₁, hyg₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
⊢ ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
have refine : ∀ (x : ℝ) (hx : x ≥ max x₀ (max yf yg)), LSeries (f - g) (↑x : ℂ) = 0 x
Tactic: refine ⟨max x₀ (max yf yg), fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeriesSummable f (↑x : ℂ)
have refine : yf ≤ x
Tactic: refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyf₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeries (f - g) (↑x : ℂ) = 0 x
have Hf : LSeriesSummable f (↑x : ℂ)
Tactic: have Hf : LSeriesSummable f x := by
    refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyf₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
    exact (le_max_left _ yg).trans <| (le_max_right x₀ _).trans hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
⊢ LSeriesSummable g (↑x : ℂ)
have refine : yg ≤ x
Tactic: refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyg₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
⊢ LSeries (f - g) (↑x : ℂ) = 0 x
have Hg : LSeriesSummable g (↑x : ℂ)
Tactic: have Hg : LSeriesSummable g x := by
    refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyg₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
    exact (le_max_right yf _).trans <| (le_max_right x₀ _).trans hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
Hg : LSeriesSummable g (↑x : ℂ)
⊢ LSeries (f - g) (↑x : ℂ) = 0 x
have rw : LSeries f (↑x : ℂ) - LSeries g (↑x : ℂ) = 0 x
Tactic: rw [LSeries_sub Hf Hg, hx₀ x <| (le_max_left ..).trans hx, sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
Hg : LSeriesSummable g (↑x : ℂ)
rw : LSeries f (↑x : ℂ) - LSeries g (↑x : ℂ) = 0 x
⊢ LSeries (f - g) (↑x : ℂ) = 0 x
have rw₁ : LSeries g (↑x : ℂ) - LSeries g (↑x : ℂ) = 0 x
Tactic: rw [LSeries_sub Hf Hg, hx₀ x <| (le_max_left ..).trans hx, sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
Hg : LSeriesSummable g (↑x : ℂ)
rw : LSeries f (↑x : ℂ) - LSeries g (↑x : ℂ) = 0 x
rw₁ : LSeries g (↑x : ℂ) - LSeries g (↑x : ℂ) = 0 x
⊢ LSeries (f - g) (↑x : ℂ) = 0 x
have rw₂ : Eq (α := ℂ) 0 (0 x)
Tactic: rw [LSeries_sub Hf Hg, hx₀ x <| (le_max_left ..).trans hx, sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
Hg : LSeriesSummable g (↑x : ℂ)
rw : LSeries f (↑x : ℂ) - LSeries g (↑x : ℂ) = 0 x
rw₁ : LSeries g (↑x : ℂ) - LSeries g (↑x : ℂ) = 0 x
rw₂ : Eq (α := ℂ) 0 (0 x)
⊢ LSeries (f - g) (↑x : ℂ) = 0 x
have rw₃ : Eq (α := ℂ) 0 0
Tactic: rw [LSeries_sub Hf Hg, hx₀ x <| (le_max_left ..).trans hx, sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)
n : ℕ
hn : n ≠ 0
⊢ f n = g n
have hsub : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries (f - g) (↑x : ℂ)) 0
Tactic: have hsub : (fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ) :=
    LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq hf hg h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)
n : ℕ
hn : n ≠ 0
hsub : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries (f - g) (↑x : ℂ)) 0
⊢ f n = g n
have ha : abscissaOfAbsConv (f - g) ≠ ⊤
Tactic: have ha : abscissaOfAbsConv (f - g) ≠ ⊤ :=
    lt_top_iff_ne_top.mp <| (abscissaOfAbsConv_sub_le f g).trans_lt <| max_lt hf hg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
⊢ LSeries f = LSeries g ↔ ∀ (n : ℕ), n ≠ 0 → f n = g n
have refine : ∀ (H : LSeries f = LSeries g) (n : ℕ) (hn : n ≠ 0), f n = g n
Tactic: refine ⟨fun H n hn ↦ ?_, fun H ↦ funext (LSeries_congr fun {n} ↦ H n)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ f n = g n
have refine : Filter.EventuallyEq (β := ℂ) Filter.atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)
Tactic: refine eq_of_LSeries_eventually_eq hf hg ?_ hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : LSeries f = LSeries g
⊢ f = g
have h₁ : ∀ (n : ℕ), n ≠ 0 → f n = g n
Tactic: replace h := (LSeries_eq_iff_of_abscissaOfAbsConv_lt_top hf.2 hg.2).mp h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
⊢ f = g
have h₁ : ∀ (n : ℕ), f n = g n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
n : ℕ
⊢ f n = g n
have h₁ : f 0 = g 0
Tactic: cases n with
  | zero => exact hf.1.trans hg.1.symm
  | succ n => exact h _ n.zero_ne_add_one.symm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
n : ℕ
h₁ : f 0 = g 0
⊢ f n = g n
have h₂ : ∀ (n : ℕ), f (n + 1) = g (n + 1)
Tactic: cases n with
  | zero => exact hf.1.trans hg.1.symm
  | succ n => exact h _ n.zero_ne_add_one.symm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
⊢ term (f + g) s = term f s + term g s
have h : term (f + g) s 0 = (term f s + term g s) 0
Tactic: ext ⟨- | n⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
h : term (f + g) s 0 = (term f s + term g s) 0
⊢ term (f + g) s = term f s + term g s
have h₁ : ∀ (n : ℕ), term (f + g) s (n + 1) = (term f s + term g s) (n + 1)
Tactic: ext ⟨- | n⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f : ℕ → ℂ
s : ℂ
⊢ term (-f) s = -term f s
have h : term (-f) s 0 = (-term f s) 0
Tactic: ext ⟨- | n⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f : ℕ → ℂ
s : ℂ
h : term (-f) s 0 = (-term f s) 0
⊢ term (-f) s = -term f s
have h₁ : ∀ (n : ℕ), term (-f) s (n + 1) = (-term f s) (n + 1)
Tactic: ext ⟨- | n⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
⊢ term (f - g) s = term f s - term g s
have simp_rw : term (f + -g) s = term f s + -term g s
Tactic: simp_rw [sub_eq_add_neg, term_add, term_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
simp_rw : term (f + -g) s = term f s + -term g s
⊢ term (f - g) s = term f s - term g s
have simp_rw₁ : term f s + term (-g) s = term f s + -term g s
Tactic: simp_rw [sub_eq_add_neg, term_add, term_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f - g) s n = term f s n - term g s n
have rw : (term f s - term g s) n = term f s n - term g s n
Tactic: rw [term_sub, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
rw : (term f s - term g s) n = term f s n - term g s n
⊢ term (f - g) s n = term f s n - term g s n
have rw₁ : term f s n - term g s n = term f s n - term g s n
Tactic: rw [term_sub, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f : ℕ → ℂ
c s : ℂ
⊢ term (c • f) s = c • term f s
have h : term (c • f) s 0 = (c • term f s) 0
Tactic: ext ⟨- | n⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
f : ℕ → ℂ
c s : ℂ
h : term (c • f) s 0 = (c • term f s) 0
⊢ term (c • f) s = c • term f s
have h₁ : ∀ (n : ℕ), term (c • f) s (n + 1) = (c • term f s) (n + 1)
Tactic: ext ⟨- | n⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n
have inl : ∀ (hn : n = 0), term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Linearity (goal)
Goal:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
inl : ∀ (hn : n = 0), term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n
have inr : ∀ (hn : n ≠ 0), term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
⊢ HasSum (fun (i : ι) ↦ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s) (mellin F s)
have simp_rw : HasSum (α := ℂ) (fun (i : ι) ↦ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    ∑' (x_1 : ι), (↑x : ℂ) ^ (s - 1) * (a x_1 * (↑(rexp (-p x_1 * x)) : ℂ)))
Tactic: simp_rw [mellin, smul_eq_mul, ← setIntegral_congr_fun measurableSet_Ioi
    (fun t ht ↦ congr_arg _ (hF t ht).tsum_eq), ← tsum_mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
⊢ HasSum (α := ℂ) (fun (i : ι) ↦ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∑' (x_1 : ι), (↑x : ℂ) ^ (s - 1) * (a x_1 * (↑(rexp (-p x_1 * x)) : ℂ)))
have h : ∀ (i : ι),
  Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
    @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      (↑a_1 : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * a_1)) : ℂ))
Tactic: convert!
    hasSum_integral_of_summable_integral_norm (F := fun i t ↦ t ^ (s - 1) * (a i * rexp (-p i * t)))
      (fun i ↦ ?_) ?_ using
    2 with i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
h :
  ∀ (i : ι),
    Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        (↑a_1 : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * a_1)) : ℂ))
⊢ HasSum (α := ℂ) (fun (i : ι) ↦ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∑' (x_1 : ι), (↑x : ℂ) ^ (s - 1) * (a x_1 * (↑(rexp (-p x_1 * x)) : ℂ)))
have convert_3 : ∀ (i : ι),
  @Integrable ℂ _ _ ℝ Real.measurableSpace
    ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i) (Measure.restrict volume (Ioi 0))
Tactic: convert!
    hasSum_integral_of_summable_integral_norm (F := fun i t ↦ t ^ (s - 1) * (a i * rexp (-p i * t)))
      (fun i ↦ ?_) ?_ using
    2 with i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
h :
  ∀ (i : ι),
    Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        (↑a_1 : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * a_1)) : ℂ))
convert_3 :
  ∀ (i : ι),
    @Integrable ℂ _ _ ℝ Real.measurableSpace
      ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i)
      (Measure.restrict volume (Ioi 0))
⊢ HasSum (α := ℂ) (fun (i : ι) ↦ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∑' (x_1 : ι), (↑x : ℂ) ^ (s - 1) * (a x_1 * (↑(rexp (-p x_1 * x)) : ℂ)))
have convert_4 : Summable (α := ℝ) fun (i : ι) ↦
  @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
    Norm.norm (E := ℂ) ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i a_1)
Tactic: convert!
    hasSum_integral_of_summable_integral_norm (F := fun i t ↦ t ^ (s - 1) * (a i * rexp (-p i * t)))
      (fun i ↦ ?_) ?_ using
    2 with i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
    @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      (↑a_1 : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * a_1)) : ℂ))
have h : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
  a i *
    @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
Tactic: simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc (a _), mul_div_assoc, integral_const_mul]