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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
⊢ meromorphicOrderAt f u ≠ ⊤

Tactic:
(h₂f ⟨u, hu⟩)

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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
refine_2 :
  ∀ (n : ℤ) (hn : (↑n : WithTop ℤ) = meromorphicOrderAt f u),
    -(↑(↑n : WithTop ℤ).untop₀ : WithTop ℤ) + (↑n : WithTop ℤ) = 0
⊢ -(↑(meromorphicOrderAt f u).untop₀ : WithTop ℤ) + meromorphicOrderAt f u = 0

Tactic:
lift meromorphicOrderAt f u to ℤ using (h₂f ⟨u, hu⟩) with n hn

Premises used: meromorphicOrderAt, 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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f u
refine_2 : (↑(-n + n) : WithTop ℤ) = 0
⊢ -(↑(↑n : WithTop ℤ).untop₀ : WithTop ℤ) + (↑n : WithTop ℤ) = 0

Tactic:
rw [WithTop.untop₀_coe, ← WithTop.LinearOrderedAddCommGroup.coe_neg, ← WithTop.coe_add]

Premises used: WithTop.LinearOrderedAddCommGroup.coe_neg, WithTop.untop₀_coe, WithTop.coe_add
-- 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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f u
⊢ (↑(-n + n) : WithTop ℤ) = 0

Tactic:
simp
-- 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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
h :
  ∀ (a : 𝕜) (h₂a : Eq (α := ℤ) ((divisor f U : (a : 𝕜) → ℤ) a : ℤ) (0 a : ℤ)) (h₃a : MeromorphicNFAt (φ⁻¹ • f) a)
    (h₄a : a ∈ U),
    f a =
      HSMul.hSMul (α := 𝕜 → 𝕜)
        (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g a
⊢ f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g

Tactic:
filter_upwards [(divisor f U).eq_zero_codiscreteWithin,
      (hφ.inv.smul h₁f).meromorphicNFAt_mem_codiscreteWithin,
      self_mem_codiscreteWithin U] with a h₂a h₃a h₄a

Premises used: Function.locallyFinsuppWithin.eq_zero_codiscreteWithin, MeromorphicOn.divisor, MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin, MeromorphicOn.inv, Filter.self_mem_codiscreteWithin, MeromorphicOn.smul
-- 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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
a : 𝕜
h₂a : Eq (α := ℤ) ((divisor f U : (a : 𝕜) → ℤ) a : ℤ) (0 a : ℤ)
h₃a : MeromorphicNFAt (φ⁻¹ • f) a
h₄a : a ∈ U
h :
  f a =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ))
      (toMeromorphicNFOn (φ⁻¹ • f) U) a
⊢ f a =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g a

Tactic:
unfold g
-- 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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
a : 𝕜
h₂a : Eq (α := ℤ) ((divisor f U : (a : 𝕜) → ℤ) a : ℤ) (0 a : ℤ)
h₃a : MeromorphicNFAt (φ⁻¹ • f) a
h₄a : a ∈ U
h :
  f a =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜)
      ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a)
      ((φ a)⁻¹ • f a)
⊢ f a =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ))
      (toMeromorphicNFOn (φ⁻¹ • f) U) a

Tactic:
simp only [Pi.smul_apply', toMeromorphicNFOn_eq_toMeromorphicNFAt (hφ.inv.smul h₁f) h₄a,
      toMeromorphicNFAt_eq_self.2 h₃a, Pi.inv_apply]

Premises used: Iff.mpr, toMeromorphicNFOn_eq_toMeromorphicNFAt, Pi.smul_apply', toMeromorphicNFAt_eq_self, MeromorphicOn.inv, MeromorphicOn.smul, Pi.inv_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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
a : 𝕜
h₂a : Eq (α := ℤ) ((divisor f U : (a : 𝕜) → ℤ) a : ℤ) (0 a : ℤ)
h₃a : MeromorphicNFAt (φ⁻¹ • f) a
h₄a : a ∈ U
rw :
  Ne.{u_1 + 1} (α := 𝕜)
    ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a) 0
⊢ f a =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜)
      ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a)
      ((φ a)⁻¹ • f a)

Tactic:
rw [← smul_assoc, smul_eq_mul, mul_inv_cancel₀ _, one_smul]

Premises used: smul_assoc, mul_inv_cancel₀, one_smul, smul_eq_mul
-- 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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
a : 𝕜
h₂a : Eq (α := ℤ) ((divisor f U : (a : 𝕜) → ℤ) a : ℤ) (0 a : ℤ)
h₃a : MeromorphicNFAt (φ⁻¹ • f) a
h₄a : a ∈ U
rwa :
  meromorphicOrderAt (E := 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a =
    0
rwa₁ : Eq (α := WithTop ℤ) ((↑((divisor f U : (a : 𝕜) → ℤ) a) : WithTop ℤ) : WithTop ℤ) (0 : WithTop ℤ)
h₁d : HasFiniteSupport (α := 𝕜) (M := ℤ) (⇑(divisor f U) : (a : 𝕜) → ℤ)
rwa₂ : Eq (α := WithTop ℤ) (↑(0 a) : WithTop ℤ) 0
h₁d₁ : HasFiniteSupport (α := 𝕜) (M := ℤ) (⇑(divisor f U) : (a : 𝕜) → ℤ)
rwa₃ : Eq (α := WithTop ℤ) (↑0 : WithTop ℤ) 0
h₁d₂ : HasFiniteSupport (α := 𝕜) (M := ℤ) (⇑(divisor f U) : (a : 𝕜) → ℤ)
rwa₄ : Eq (α := WithTop ℤ) 0 0
h₁d₃ : HasFiniteSupport (α := 𝕜) (M := ℤ) (⇑(divisor f U) : (a : 𝕜) → ℤ)
rwa₅ : Eq (α := WithTop ℤ) 0 0
h₁d₄ h₁d₅ h₁d₆ : HasFiniteSupport (α := 𝕜) (M := ℤ) (⇑(divisor f U) : (a : 𝕜) → ℤ)
⊢ Ne.{u_1 + 1} (α := 𝕜)
    ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a) 0

Tactic:
rwa [← ((meromorphicNFOn_univ (divisor f U)) trivial).meromorphicOrderAt_eq_zero_iff,
      meromorphicOrderAt_eq, h₂a, Pi.zero_apply, WithTop.coe_zero]

Premises used: trivial, Function.FactorizedRational.meromorphicOrderAt_eq, Pi.zero_apply, MeromorphicOn.divisor, WithTop.coe_zero, Function.FactorizedRational.meromorphicNFOn_univ, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff, 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
h₁ :
  ∀ (u : 𝕜),
    Membership.mem (γ := Set 𝕜) (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) u ↔
      u ∈ D.support (U := U)
⊢ (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)

Tactic:
ext u
-- 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
u : 𝕜
h₁ : (u ∉ support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) ↔ u ∉ D.support (U := U)
⊢ Membership.mem (γ := Set 𝕜) (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) u ↔
    u ∈ D.support (U := U)

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- 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
u : 𝕜
h₁ :
  Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0 ↔
    Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ (u ∉ support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) ↔ u ∉ D.support (U := U)

Tactic:
simp only [ne_eq, not_not, Function.mem_support]

Premises used: Classical.not_not, ne_eq, 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
u : 𝕜
h₁ :
  Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0 →
    Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
h₂ :
  Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ) →
    Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
⊢ Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0 ↔
    Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)

Tactic:
constructor
-- 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
u : 𝕜
hx : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
h₁ : ∀ (y : 𝕜) (hy : 1 < ‖y‖), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)

Tactic:
obtain ⟨y, hy⟩ := NormedField.exists_one_lt_norm 𝕜

Premises used: NormedField.exists_one_lt_norm
-- 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
u : 𝕜
hx : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
y : 𝕜
hy : 1 < ‖y‖
⊢ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖y + u - u‖ = 0 (y + u)

Tactic:
have := congrFun hx (y + u)
-- 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
u : 𝕜
hx : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
y : 𝕜
hy : 1 < ‖y‖
this : (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖y + u - u‖ = 0 (y + u)
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ) ∨ y = 0 ∨ ‖y‖ = 1 ∨ ‖y‖ = -1

Tactic:
simp only [add_sub_cancel_right, Pi.zero_apply, mul_eq_zero, Int.cast_eq_zero, log_eq_zero,
        norm_eq_zero] at this

Premises used: norm_eq_zero, Pi.zero_apply, Real.log_eq_zero, mul_eq_zero, Int.cast_eq_zero, add_sub_cancel_right
-- 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
u : 𝕜
hx : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
y : 𝕜
hy : 1 < ‖y‖
this : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ) ∨ y = 0 ∨ ‖y‖ = 1 ∨ ‖y‖ = -1
h₁ : ∀ (h : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
h₂ : ∀ (h : y = 0), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
h₃ : ∀ (h : ‖y‖ = 1), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
h₄ : ∀ (h : ‖y‖ = -1), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)

Tactic:
rcases this with h | h | h | h
-- 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_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 : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)

Tactic:
assumption
-- 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_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 = 0
⊢ LT.lt (α := ℝ) 1 0

Tactic:
simp only [h, norm_zero] at hy

Premises used: norm_zero
-- 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_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 = 0
hy : LT.lt (α := ℝ) 1 0
linarith : LT.lt (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ) → -1 + HSub.hSub (α := ℝ) 1 0 = 0
linarith₁ : LT.lt (α := ℤ) (0 : ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) → -1 + HSub.hSub (α := ℝ) 1 0 = 0
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)

Tactic:
linarith
-- 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_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 : ℤ)

Tactic:
simp only [h, lt_self_iff_false] at hy

Premises used: lt_self_iff_false
-- 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_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
⊢ LT.lt (α := ℝ) 1 0

Tactic:
simp only [h, lt_neg_self_iff] at hy

Premises used: lt_neg_self_iff
-- 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_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
linarith₁ : LT.lt (α := ℤ) (0 : ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) → -1 + HSub.hSub (α := ℝ) 1 0 = 0
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)

Tactic:
linarith
-- 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
u : 𝕜
hx : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0

Tactic:
simp_all [Pi.zero_def]

Premises used: Pi.zero_def
-- 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
⊢ (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]
-- 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)
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‖
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‖
⊢ (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

Premises used: Set.Finite, Function.locallyFinsuppWithin.support