awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : ¬z ∉ U
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
have hz₁ : z ∈ U
Tactic: rw [not_not] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
have neg : (meromorphicOrderAt f₁ z).untop₀ = (meromorphicOrderAt f₂ z).untop₀
Tactic: rw [divisor_apply hf₁ hz, divisor_apply hf₂ hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
⊢ (meromorphicOrderAt f₁ z).untop₀ = (meromorphicOrderAt f₂ z).untop₀
have neg : meromorphicOrderAt f₁ z = meromorphicOrderAt f₂ z
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
⊢ meromorphicOrderAt f₁ z = meromorphicOrderAt f₂ z
have neg : f₁ =ᶠ[𝓝[≠] z] f₂
Tactic: apply meromorphicOrderAt_congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
have pos : ∀ (hf₁ : MeromorphicOn f₁ U), Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
Tactic: by_cases hf₁ : MeromorphicOn f₁ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
pos : ∀ (hf₁ : MeromorphicOn f₁ U), Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
have neg : ∀ (hf₁ : ¬MeromorphicOn f₁ U), Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
Tactic: by_cases hf₁ : MeromorphicOn f₁ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
have pos : ∀ (x : 𝕜), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
have pos : ∀ (hx : x ∈ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
pos : ∀ (hx : x ∈ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
have neg : ∀ (hx : x ∉ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
have pos : (meromorphicOrderAt f₁ x).untop₀ = (meromorphicOrderAt f₂ x).untop₀
Tactic: simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin h₁ h₂]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ (meromorphicOrderAt f₁ x).untop₀ = (meromorphicOrderAt f₂ x).untop₀
have pos : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have pos : f₁ =ᶠ[𝓝[≠] x] f₂
Tactic: apply meromorphicOrderAt_congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ f₁ =ᶠ[𝓝[≠] x] f₂
have h₃ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
Tactic: simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
        disjoint_principal_right] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
⊢ U ∈ 𝓝[≠] x
have apply : ∃ (u : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
Tactic: apply mem_nhdsWithin.mpr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
w : Set 𝕜
left : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
left₁ : x ∈ U
⊢ ∃ (u : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
have right : U ∩ {x}ᶜ ⊆ U
Tactic: use U, h₂, hx, Set.inter_subset_left
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
⊢ f₁ =ᶠ[𝓝[≠] x] f₂
have this : U ∈ 𝓝[≠] x
Tactic: have : U ∈ 𝓝[≠] x := by
        apply mem_nhdsWithin.mpr
        use U, h₂, hx, Set.inter_subset_left
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
⊢ f₁ =ᶠ[𝓝[≠] x] f₂
have h : ∀ (a : 𝕜) (h₁a : a ∈ U) (h₂a : a ∈ (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ), f₁ a = f₂ a
Tactic: filter_upwards [this, h₁ x hx] with a h₁a h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
h₂a : a ∈ (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ
⊢ f₁ a = f₂ a
have h₂a₁ : a ∈ U → ¬¬f₁ a = f₂ a
Tactic: simp only [Set.mem_compl_iff, Set.mem_diff, Set.mem_setOf_eq, not_and] at h₂a
Cleared hypotheses: h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
h₂a : a ∈ U → ¬¬f₁ a = f₂ a
⊢ f₁ a = f₂ a
have h : ∀ (h₂a : a ∉ U), f₁ a = f₂ a
Tactic: tauto
Cleared hypotheses: h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
h₂a : a ∈ U → ¬¬f₁ a = f₂ a
h : ∀ (h₂a : a ∉ U), f₁ a = f₂ a
⊢ f₁ a = f₂ a
have h₃ : ∀ (h₂a : ¬¬f₁ a = f₂ a), f₁ a = f₂ a
Tactic: tauto
Cleared hypotheses: h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
h₂a : a ∈ U → ¬¬f₁ a = f₂ a
h : ∀ (h₂a : a ∉ U), f₁ a = f₂ a
h₃ h₄ h₅ : ∀ (h₂a : ¬¬f₁ a = f₂ a), f₁ a = f₂ a
⊢ f₁ a = f₂ a
have h₆ : ∀ (h₂a : f₁ a = f₂ a), f₁ a = f₂ a
Tactic: tauto
Cleared hypotheses: h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((divisor f U : (a : 𝕜) → ℤ) x : ℤ)
have pos : ∀ (hx : x ∈ U), LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((divisor f U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
pos : ∀ (hx : x ∈ U), LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((divisor f U : (a : 𝕜) → ℤ) x : ℤ)
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((divisor f U : (a : 𝕜) → ℤ) x : ℤ)
have neg : ∀ (hx : x ∉ U), LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((divisor f U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
e : E
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U) 0
have h : ∀ (x : 𝕜), Eq (α := ℤ) ((divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U : (a : 𝕜) → ℤ) x : ℤ) ((0 : (a : 𝕜) → ℤ) x : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
e : E
x : 𝕜
⊢ Eq (α := ℤ) ((divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U : (a : 𝕜) → ℤ) x : ℤ) ((0 : (a : 𝕜) → ℤ) x : ℤ)
have h : MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬e = 0 ∨ e = 0
Tactic: simp only [divisor_def, meromorphicOrderAt_const, Function.locallyFinsuppWithin.coe_zero,
    Pi.zero_apply, ite_eq_right_iff, WithTop.untop₀_eq_zero,
    LinearOrderedAddCommGroupWithTop.top_ne_zero, imp_false, ite_eq_left_iff, WithTop.zero_ne_top,
    Decidable.not_not, and_imp]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
e : E
x : 𝕜
h h₁ h₂ h₃ h₄ : MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬e = 0 ∨ e = 0
⊢ MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬e = 0 ∨ e = 0
have h₅ : MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬¬e = 0 → e = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
e : E
x : 𝕜
h h₁ h₂ h₃ h₄ : MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬e = 0 ∨ e = 0
h₅ : MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬¬e = 0 → e = 0
⊢ MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬e = 0 ∨ e = 0
have h₆ : MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → e = 0 → e = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
e : E
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U) 0
have h : ∀ (x : 𝕜), Eq (α := ℤ) ((divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U : (a : 𝕜) → ℤ) x : ℤ) ((0 : (a : 𝕜) → ℤ) x : ℤ)
Tactic: classical
  ext x
  simp only [divisor_def, meromorphicOrderAt_const, Function.locallyFinsuppWithin.coe_zero,
    Pi.zero_apply, ite_eq_right_iff, WithTop.untop₀_eq_zero,
    LinearOrderedAddCommGroupWithTop.top_ne_zero, imp_false, ite_eq_left_iff, WithTop.zero_ne_top,
    Decidable.not_not, and_imp]
  tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
e : E
h :
  ∀ (x : 𝕜),
    Eq (α := ℤ) ((divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U : (a : 𝕜) → ℤ) x : ℤ) ((0 : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U) 0
have h₁ : ∀ (x : 𝕜), MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬e = 0 ∨ e = 0
Tactic: classical
  ext x
  simp only [divisor_def, meromorphicOrderAt_const, Function.locallyFinsuppWithin.coe_zero,
    Pi.zero_apply, ite_eq_right_iff, WithTop.untop₀_eq_zero,
    LinearOrderedAddCommGroupWithTop.top_ne_zero, imp_false, ite_eq_left_iff, WithTop.zero_ne_top,
    Decidable.not_not, and_imp]
  tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
n : ℕ
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (OfNat.ofNat n) U) 0
have h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) ((OfNat.ofNat n : 𝕜 → 𝕜) x) (↑n : 𝕜)
Tactic: convert! divisor_const (n : 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
⊢ LE.le (α := ℤ) (min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z) : ℤ)
    ((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hz : z ∉ U),
  LE.le (α := ℤ) (min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z) : ℤ)
    ((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases! hz : z ∉ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
pos :
  ∀ (hz : z ∉ U),
    LE.le (α := ℤ) (min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z) : ℤ)
      ((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z : ℤ)
⊢ LE.le (α := ℤ) (min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z) : ℤ)
    ((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hz : z ∈ U),
  LE.le (α := ℤ) (min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z) : ℤ)
    ((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases! hz : z ∉ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
⊢ LE.le (α := ℤ) (min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z) : ℤ)
    ((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z : ℤ)
have neg : min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
Tactic: rw [divisor_apply hf₁ hz, divisor_apply hf₂ hz, divisor_apply (hf₁.add hf₂) hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
have pos : ∀ (h₁ : meromorphicOrderAt f₁ z = ⊤),
  min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
Tactic: by_cases h₁ : meromorphicOrderAt f₁ z = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
pos :
  ∀ (h₁ : meromorphicOrderAt f₁ z = ⊤),
    min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
have neg : ∀ (h₁ : ¬meromorphicOrderAt f₁ z = ⊤),
  min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
Tactic: by_cases h₁ : meromorphicOrderAt f₁ z = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
have pos : ∀ (h₂ : meromorphicOrderAt f₂ z = ⊤),
  min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
Tactic: by_cases h₂ : meromorphicOrderAt f₂ z = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
pos :
  ∀ (h₂ : meromorphicOrderAt f₂ z = ⊤),
    min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
have neg : ∀ (h₂ : ¬meromorphicOrderAt f₂ z = ⊤),
  min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
Tactic: by_cases h₂ : meromorphicOrderAt f₂ z = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
h₂ : ¬meromorphicOrderAt f₂ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
have neg : (min (meromorphicOrderAt f₁ z) (meromorphicOrderAt f₂ z)).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
Tactic: rw [← WithTop.untop₀_min h₁ h₂]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
h₂ : ¬meromorphicOrderAt f₂ z = ⊤
⊢ (min (meromorphicOrderAt f₁ z) (meromorphicOrderAt f₂ z)).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
have neg : min (meromorphicOrderAt f₁ z) (meromorphicOrderAt f₂ z) ≤ meromorphicOrderAt (f₁ + f₂) z
Tactic: apply WithTop.untop₀_le_untop₀ h₃
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) z) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
    (((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hz : z ∉ U),
  LE.le (α := (fun (a : 𝕜) ↦ ℤ) z) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
    (((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases! hz : z ∉ U