awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
⊢ Set.Infinite.{u_1} (α := 𝕜) (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖)

Tactic:
simpa [t₁] using h₃f
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
rw : (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U] HAdd.hAdd (α := 𝕜 → ℝ) 0 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‖

Tactic:
rw [finsum_of_infinite_support (by simpa [t₁] using h₃f)]

Premises used: finsum_of_infinite_support
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
⊢ Set.Infinite.{u_1} (α := 𝕜)
    (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦
      HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ))

Tactic:
simpa [FactorizedRational.mulSupport] using h₃f

Premises used: Function.FactorizedRational.mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
⊢ f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g

Tactic:
rw [finprod_of_infinite_mulSupport (by simpa [FactorizedRational.mulSupport] using h₃f)] at h

Premises used: finprod_of_infinite_mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
h₁ : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
⊢ (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)

Tactic:
rw [finprod_of_infinite_mulSupport (by simpa [FactorizedRational.mulSupport] using h₃f)] at h

Premises used: finprod_of_infinite_mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
h₁ : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
t₂ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
⊢ ¬D.support (U := U).Finite

Tactic:
rw [finprod_of_infinite_mulSupport (by simpa [FactorizedRational.mulSupport] using h₃f)] at h

Premises used: finprod_of_infinite_mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
h₁ :
  ∀ (x : 𝕜) (hx : f x = HSMul.hSMul (α := 𝕜 → 𝕜) 1 g x),
    log ‖f x‖ = HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ) 0 (fun (x : 𝕜) ↦ log ‖g x‖) x
⊢ (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U] HAdd.hAdd (α := 𝕜 → ℝ) 0 fun (x : 𝕜) ↦ log ‖g x‖

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
x : 𝕜
hx : f x = HSMul.hSMul (α := 𝕜 → 𝕜) 1 g x
⊢ log ‖f x‖ = HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ) 0 (fun (x : 𝕜) ↦ log ‖g x‖) x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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‖

Tactic:
case neg =>
    rw [finsum_of_infinite_support (by simpa [t₁] using h₃f)]
    rw [finprod_of_infinite_mulSupport (by simpa [FactorizedRational.mulSupport] using h₃f)] at h
    filter_upwards [h] with x hx
    simp [hx]

Premises used: MeromorphicOn.neg, finprod_of_infinite_mulSupport, finsum_of_infinite_support
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
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
⊢ (fun (x : 𝕜) ↦ log ‖f x‖) =ᶠ[codiscreteWithin U]
    HAdd.hAdd (α := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : 𝕜) ↦
      log ‖g x‖

Tactic:
filter_upwards [h, D.eq_zero_codiscreteWithin, self_mem_codiscreteWithin U] with z hz h₂z h₃z

Premises used: Function.locallyFinsuppWithin.eq_zero_codiscreteWithin, Filter.self_mem_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)

Tactic:
rw [Pi.zero_apply] at h₂z

Premises used: Pi.zero_apply
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
h₂z₁ : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
⊢ z ∈ U

Tactic:
rw [Pi.zero_apply] at h₂z

Premises used: Pi.zero_apply
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
⊢ (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦
      HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) ⊆
    (↑(h₃f.toFinset (s := D.support (U := U))) : Set 𝕜)

Tactic:
simp_all [FactorizedRational.mulSupport]

Premises used: Function.FactorizedRational.mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
⊢ (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) ⊆
    (↑(h₃f.toFinset (s := D.support (U := U))) : Set 𝕜)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
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
⊢ log ‖f z‖ =
    HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ) (∑ᶠ (u : 𝕜), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖)
      (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)]

Premises used: finsum_eq_sum_of_support_subset, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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))
⊢ Ne (α := ℤ) ((D : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)

Tactic:
rw [Finite.mem_toFinset, Function.mem_support] at hx

Premises used: Set.Finite.mem_toFinset, Function.mem_support
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 : ℤ)
rw : ¬x = z
⊢ HPow.hPow (β := ℤ) ‖z - x‖ ((D : (a : 𝕜) → ℤ) x : ℤ) ≠ 0

Tactic:
rw [ne_eq, zpow_eq_zero_iff hx, norm_eq_zero, sub_eq_zero, eq_comm]

Premises used: norm_eq_zero, sub_eq_zero, zpow_eq_zero_iff, eq_comm, ne_eq
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 : ℤ)
apply : Ne (α := ℤ) ((D : (a : 𝕜) → ℤ) x : ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ)
⊢ ¬x = z

Tactic:
apply ne_of_apply_ne D

Premises used: ne_of_apply_ne, DFunLike.coe
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℤ) ((D : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
⊢ Ne (α := ℤ) ((D : (a : 𝕜) → ℤ) x : ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
rwa [h₂z]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 ∈ 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]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
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
⊢ 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:
simp only [Pi.smul_apply', Finset.prod_apply, Pi.pow_apply, norm_smul, norm_prod, norm_zpow]

Premises used: norm_smul, Finset.prod_apply, Pi.smul_apply', norm_prod, Pi.pow_apply, norm_zpow
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
⊢ ‖g z‖ ≠ 0

Tactic:
simp [hg ⟨z, h₃z⟩]

Premises used: Subtype.mk
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
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
⊢ 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:
rw [log_mul (Finset.prod_ne_zero_iff.2 this) (by simp [hg ⟨z, h₃z⟩]), log_prod this]

Premises used: Iff.mpr, Real.log_prod, Finset.prod_ne_zero_iff, Real.log_mul