awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h_1 :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
u : 𝕜
hx : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = -1
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have hy₁ : LT.lt (α := ℝ) 1 0
Tactic: simp only [h, lt_neg_self_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h_1 :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
u : 𝕜
hx : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
y : 𝕜
h : ‖y‖ = -1
hy : LT.lt (α := ℝ) 1 0
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have linarith : LT.lt (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ) → -1 + HSub.hSub (α := ℝ) 1 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h_1 :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
u : 𝕜
hx : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
y : 𝕜
h : ‖y‖ = -1
hy : LT.lt (α := ℝ) 1 0
linarith : LT.lt (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ) → -1 + HSub.hSub (α := ℝ) 1 0 = 0
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have linarith₁ : LT.lt (α := ℤ) (0 : ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) → -1 + HSub.hSub (α := ℝ) 1 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
⊢ (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U]
    HAdd.hAdd (α := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : 𝕜) ↦
      log ‖g x‖
have t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
Tactic: have t₁ : (fun u ↦ (D u * log ‖· - u‖)).support = D.support := by
    ext u
    rw [← not_iff_not]
    simp only [ne_eq, not_not, Function.mem_support]
    constructor <;> intro hx
    · obtain ⟨y, hy⟩ := NormedField.exists_one_lt_norm 𝕜
      have := congrFun hx (y + u)
      simp only [add_sub_cancel_right, Pi.zero_apply, mul_eq_zero, Int.cast_eq_zero, log_eq_zero,
        norm_eq_zero] at this
      rcases this with h | h | h | h
      · assumption
      · simp only [h, norm_zero] at hy
        linarith
      · simp only [h, lt_self_iff_false] at hy
      · simp only [h, lt_neg_self_iff] at hy
        linarith
    · simp_all [Pi.zero_def]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
⊢ (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U]
    HAdd.hAdd (α := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : 𝕜) ↦
      log ‖g x‖
have pos : ∀ (h₃f : D.support (U := U).Finite),
  (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U]
    HAdd.hAdd (α := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : 𝕜) ↦
      log ‖g x‖
Tactic: by_cases h₃f : D.support.Finite
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
pos :
  ∀ (h₃f : D.support (U := U).Finite),
    (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U]
      HAdd.hAdd (α := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : 𝕜) ↦
        log ‖g x‖
⊢ (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U]
    HAdd.hAdd (α := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : 𝕜) ↦
      log ‖g x‖
have by_cases : ∀ (h₃f : ¬D.support (U := U).Finite),
  (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U]
    HAdd.hAdd (α := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : 𝕜) ↦
      log ‖g x‖
Tactic: by_cases h₃f : D.support.Finite
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : ¬D.support (U := U).Finite
⊢ (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U]
    HAdd.hAdd (α := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : 𝕜) ↦
      log ‖g x‖
have rw : (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U] HAdd.hAdd (α := 𝕜 → ℝ) 0 fun (x : 𝕜) ↦ log ‖g x‖
Tactic: rw [finsum_of_infinite_support (by simpa [t₁] using h₃f)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : ¬D.support (U := U).Finite
⊢ (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U] HAdd.hAdd (α := 𝕜 → ℝ) 0 fun (x : 𝕜) ↦ log ‖g x‖
have h₁ : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
Tactic: rw [finprod_of_infinite_mulSupport (by simpa [FactorizedRational.mulSupport] using h₃f)] at h
Cleared hypotheses: h, t₁, h₃f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : ¬D.support (U := U).Finite
⊢ (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U] HAdd.hAdd (α := 𝕜 → ℝ) 0 fun (x : 𝕜) ↦ log ‖g x‖
have h₁ : ∀ (x : 𝕜) (hx : f x = HSMul.hSMul (α := 𝕜 → 𝕜) 1 g x),
  log ‖f x‖ = HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ) 0 (fun (x : 𝕜) ↦ log ‖g x‖) x
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
⊢ (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U]
    HAdd.hAdd (α := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : 𝕜) ↦
      log ‖g x‖
have h₁ : ∀ (z : 𝕜)
  (hz :
    f z =
      HSMul.hSMul (α := 𝕜 → 𝕜)
        (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z)
  (h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 z : ℤ)) (h₃z : z ∈ U),
  log ‖f z‖ =
    HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖)
      (fun (x : 𝕜) ↦ log ‖g x‖) z
Tactic: filter_upwards [h, D.eq_zero_codiscreteWithin, self_mem_codiscreteWithin U] with z hz h₂z h₃z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
z : 𝕜
hz :
  f z =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z
h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 z : ℤ)
h₃z : z ∈ U
⊢ log ‖f z‖ =
    HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖)
      (fun (x : 𝕜) ↦ log ‖g x‖) z
have h₂z₁ : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
Tactic: rw [Pi.zero_apply] at h₂z
Cleared hypotheses: h₂z, h₃z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
z : 𝕜
hz :
  f z =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z
h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
h₃z : z ∈ U
⊢ log ‖f z‖ =
    HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖)
      (fun (x : 𝕜) ↦ log ‖g x‖) z
have h₁ : log
    ‖HSMul.hSMul (α := 𝕜 → 𝕜)
        (∏ i ∈ h₃f.toFinset (s := D.support (U := U)),
          HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - i) ((D : (a : 𝕜) → ℤ) i : ℤ))
        g z‖ =
  HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ)
    (∑ i ∈ h₃f.toFinset (s := D.support (U := U)), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) i) : ℝ) * log ‖x - i‖)
    (fun (x : 𝕜) ↦ log ‖g x‖) z
Tactic: rw [hz, finprod_eq_prod_of_mulSupport_subset (s := h₃f.toFinset) _
      (by simp_all [FactorizedRational.mulSupport]),
    finsum_eq_sum_of_support_subset (s := h₃f.toFinset) _ (by simp_all)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
z : 𝕜
hz :
  f z =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z
h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
h₃z : z ∈ U
x : 𝕜
hx : x ∈ h₃f.toFinset (s := D.support (U := U))
⊢ HPow.hPow (β := ℤ) ‖z - x‖ ((D : (a : 𝕜) → ℤ) x : ℤ) ≠ 0
have hx₁ : Ne (α := ℤ) ((D : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
Tactic: rw [Finite.mem_toFinset, Function.mem_support] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
z : 𝕜
hz :
  f z =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z
h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
h₃z : z ∈ U
x : 𝕜
hx : Ne (α := ℤ) ((D : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
⊢ HPow.hPow (β := ℤ) ‖z - x‖ ((D : (a : 𝕜) → ℤ) x : ℤ) ≠ 0
have rw : ¬x = z
Tactic: rw [ne_eq, zpow_eq_zero_iff hx, norm_eq_zero, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
z : 𝕜
hz :
  f z =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z
h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
h₃z : z ∈ U
x : 𝕜
hx : Ne (α := ℤ) ((D : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
⊢ ¬x = z
have apply : Ne (α := ℤ) ((D : (a : 𝕜) → ℤ) x : ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ)
Tactic: apply ne_of_apply_ne D
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
z : 𝕜
hz :
  f z =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z
h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
h₃z : z ∈ U
⊢ log
      ‖HSMul.hSMul (α := 𝕜 → 𝕜)
          (∏ i ∈ h₃f.toFinset (s := D.support (U := U)),
            HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - i) ((D : (a : 𝕜) → ℤ) i : ℤ))
          g z‖ =
    HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ)
      (∑ i ∈ h₃f.toFinset (s := D.support (U := U)), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) i) : ℝ) * log ‖x - i‖)
      (fun (x : 𝕜) ↦ log ‖g x‖) z
have this : ∀ x ∈ h₃f.toFinset (s := D.support (U := U)), HPow.hPow (β := ℤ) ‖z - x‖ ((D : (a : 𝕜) → ℤ) x : ℤ) ≠ 0
Tactic: have : ∀ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x ≠ 0 := by
    intro x hx
    rw [Finite.mem_toFinset, Function.mem_support] at hx
    rw [ne_eq, zpow_eq_zero_iff hx, norm_eq_zero, sub_eq_zero, eq_comm]
    apply ne_of_apply_ne D
    rwa [h₂z]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
z : 𝕜
hz :
  f z =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z
h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
h₃z : z ∈ U
this : ∀ x ∈ h₃f.toFinset (s := D.support (U := U)), HPow.hPow (β := ℤ) ‖z - x‖ ((D : (a : 𝕜) → ℤ) x : ℤ) ≠ 0
⊢ log
      ‖HSMul.hSMul (α := 𝕜 → 𝕜)
          (∏ i ∈ h₃f.toFinset (s := D.support (U := U)),
            HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - i) ((D : (a : 𝕜) → ℤ) i : ℤ))
          g z‖ =
    HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ)
      (∑ i ∈ h₃f.toFinset (s := D.support (U := U)), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) i) : ℝ) * log ‖x - i‖)
      (fun (x : 𝕜) ↦ log ‖g x‖) z
have h₁ : log ((∏ x ∈ h₃f.toFinset (s := D.support (U := U)), HPow.hPow (β := ℤ) ‖z - x‖ ((D : (a : 𝕜) → ℤ) x : ℤ)) * ‖g z‖) =
  HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ)
    (∑ i ∈ h₃f.toFinset (s := D.support (U := U)), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) i) : ℝ) * log ‖x - i‖)
    (fun (x : 𝕜) ↦ log ‖g x‖) z
Tactic: simp only [Pi.smul_apply', Finset.prod_apply, Pi.pow_apply, norm_smul, norm_prod, norm_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
z : 𝕜
hz :
  f z =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z
h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
h₃z : z ∈ U
this : ∀ x ∈ h₃f.toFinset (s := D.support (U := U)), HPow.hPow (β := ℤ) ‖z - x‖ ((D : (a : 𝕜) → ℤ) x : ℤ) ≠ 0
⊢ log ((∏ x ∈ h₃f.toFinset (s := D.support (U := U)), HPow.hPow (β := ℤ) ‖z - x‖ ((D : (a : 𝕜) → ℤ) x : ℤ)) * ‖g z‖) =
    HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ)
      (∑ i ∈ h₃f.toFinset (s := D.support (U := U)), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) i) : ℝ) * log ‖x - i‖)
      (fun (x : 𝕜) ↦ log ‖g x‖) z
have h₁ : ∑ i ∈ h₃f.toFinset (s := D.support (U := U)), log (HPow.hPow (β := ℤ) ‖z - i‖ ((D : (a : 𝕜) → ℤ) i : ℤ)) + log ‖g z‖ =
  HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ)
    (∑ i ∈ h₃f.toFinset (s := D.support (U := U)), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) i) : ℝ) * log ‖x - i‖)
    (fun (x : 𝕜) ↦ log ‖g x‖) z
Tactic: rw [log_mul (Finset.prod_ne_zero_iff.2 this) (by simp [hg ⟨z, h₃z⟩]), log_prod this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
⊢ meromorphicTrailingCoeffAt f x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) D x 0 u) (g x)
have t₀ : MeromorphicAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x
Tactic: have t₀ : MeromorphicAt (∏ᶠ u, (· - u) ^ D u) x :=
    (FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
t₀ : MeromorphicAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x
⊢ meromorphicTrailingCoeffAt f x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) D x 0 u) (g x)
have rw : HSMul.hSMul (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x)
    (g x) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) D x 0 u) (g x)
Tactic: rw [meromorphicTrailingCoeffAt_congr_nhdsNE
      (hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (by fun_prop) h₁x h₂x h),
    t₀.meromorphicTrailingCoeffAt_smul h₁g.meromorphicAt,
    h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
⊢ log ‖meromorphicTrailingCoeffAt f x‖ = ∑ᶠ (u : 𝕜), (↑(D u) : ℝ) * log ‖x - u‖ + log ‖g x‖
have hx : Norm.norm (E := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x) ≠ 0
Tactic: rw [meromorphicTrailingCoeffAt_congr_nhdsNE
      (hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin
        (((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).smul h₁g.meromorphicAt)
          h₁x h₂x h),
    ((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).meromorphicTrailingCoeffAt_smul
      h₁g.meromorphicAt, h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g,
    norm_smul, log_mul, log_norm_meromorphicTrailingCoeffAt hD]