awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 𝕜 → 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
⊢ f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g
have 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
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
-- 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 : 𝕜 → 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
⊢ f a =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ))
      (toMeromorphicNFOn (φ⁻¹ • f) U) a
have 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)
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]
-- 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 : 𝕜 → 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
⊢ 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)
have rw : Ne.{u_1 + 1} (α := 𝕜)
  ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a) 0
Tactic: rw [← smul_assoc, smul_eq_mul, mul_inv_cancel₀ _, one_smul]
-- 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 : 𝕜 → 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
⊢ Ne.{u_1 + 1} (α := 𝕜)
    ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a) 0
have rwa : meromorphicOrderAt (E := 𝕜)
    (∏ᶠ (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]
-- 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 : 𝕜 → 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
⊢ Ne.{u_1 + 1} (α := 𝕜)
    ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a) 0
have rwa₁ : Eq (α := WithTop ℤ) ((↑((divisor f U : (a : 𝕜) → ℤ) a) : WithTop ℤ) : WithTop ℤ) (0 : WithTop ℤ)
Tactic: rwa [← ((meromorphicNFOn_univ (divisor f U)) trivial).meromorphicOrderAt_eq_zero_iff,
      meromorphicOrderAt_eq, h₂a, Pi.zero_apply, WithTop.coe_zero]
-- 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 : 𝕜 → 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 ℤ)
⊢ Ne.{u_1 + 1} (α := 𝕜)
    ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a) 0
have h₁d : HasFiniteSupport (α := 𝕜) (M := ℤ) (⇑(divisor f U) : (a : 𝕜) → ℤ)
Tactic: rwa [← ((meromorphicNFOn_univ (divisor f U)) trivial).meromorphicOrderAt_eq_zero_iff,
      meromorphicOrderAt_eq, h₂a, Pi.zero_apply, WithTop.coe_zero]
-- 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 : 𝕜 → 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 : 𝕜) → ℤ)
⊢ Ne.{u_1 + 1} (α := 𝕜)
    ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a) 0
have rwa₂ : Eq (α := WithTop ℤ) (↑(0 a) : WithTop ℤ) 0
Tactic: rwa [← ((meromorphicNFOn_univ (divisor f U)) trivial).meromorphicOrderAt_eq_zero_iff,
      meromorphicOrderAt_eq, h₂a, Pi.zero_apply, WithTop.coe_zero]
-- 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 : 𝕜 → 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 : 𝕜) → ℤ)
⊢ Ne.{u_1 + 1} (α := 𝕜)
    ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a) 0
have rwa₃ : Eq (α := WithTop ℤ) (↑0 : WithTop ℤ) 0
Tactic: rwa [← ((meromorphicNFOn_univ (divisor f U)) trivial).meromorphicOrderAt_eq_zero_iff,
      meromorphicOrderAt_eq, h₂a, Pi.zero_apply, WithTop.coe_zero]
-- 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 : 𝕜 → 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 : 𝕜) → ℤ)
⊢ Ne.{u_1 + 1} (α := 𝕜)
    ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) a) 0
have rwa₄ : Eq (α := WithTop ℤ) 0 0
Tactic: rwa [← ((meromorphicNFOn_univ (divisor f U)) trivial).meromorphicOrderAt_eq_zero_iff,
      meromorphicOrderAt_eq, h₂a, Pi.zero_apply, WithTop.coe_zero]
-- 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
⊢ (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
have h₁ : ∀ (u : 𝕜),
  Membership.mem (γ := Set 𝕜) (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) u ↔
    u ∈ D.support (U := U)
Tactic: ext u
-- 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
u : 𝕜
⊢ Membership.mem (γ := Set 𝕜) (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) u ↔
    u ∈ D.support (U := U)
have h₁ : (u ∉ support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) ↔ u ∉ D.support (U := U)
Tactic: rw [← not_iff_not]
-- 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
u : 𝕜
⊢ (u ∉ support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) ↔ u ∉ D.support (U := U)
have h₁ : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0 ↔
  Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
Tactic: simp only [ne_eq, not_not, Function.mem_support]
-- 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
u : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0 ↔
    Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have h₁ : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0 →
  Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
Tactic: constructor
-- 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
u : 𝕜
h₁ :
  Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0 →
    Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0 ↔
    Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have h₂ : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ) →
  Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
Tactic: constructor
-- 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
u : 𝕜
hx : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have h₁ : ∀ (y : 𝕜) (hy : 1 < ‖y‖), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
Tactic: obtain ⟨y, hy⟩ := NormedField.exists_one_lt_norm 𝕜
-- 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
u : 𝕜
hx : Eq.{u_1 + 1} (α := 𝕜 → ℝ) (fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) 0
y : 𝕜
hy : 1 < ‖y‖
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have this : (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖y + u - u‖ = 0 (y + u)
Tactic: have := congrFun hx (y + u)
-- 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
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 : ℤ)
have this₁ : 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
Cleared hypotheses: this
-- 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
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
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have h₁ : ∀ (h : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
Tactic: rcases this with h | h | h | h
Cleared hypotheses: this
-- 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
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 : ℤ)
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have h₂ : ∀ (h : y = 0), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
Tactic: rcases this with h | h | h | h
Cleared hypotheses: this
-- 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
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 : ℤ)
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have h₃ : ∀ (h : ‖y‖ = 1), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
Tactic: rcases this with h | h | h | h
Cleared hypotheses: this
-- 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
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 : ℤ)
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have h₄ : ∀ (h : ‖y‖ = -1), Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
Tactic: rcases this with h | h | h | h
Cleared hypotheses: 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 𝕜
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
⊢ Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
have hy₁ : LT.lt (α := ℝ) 1 0
Tactic: simp only [h, norm_zero] 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 = 0
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 = 0
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