awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)

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

Tactic:
simp [divisor, hf₁, (meromorphicOn_congr_codiscreteWithin h₁ h₂).not.1 hf₁]

Premises used: MeromorphicOn.divisor, Iff.not, meromorphicOn_congr_codiscreteWithin, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)
neg : ∀ (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 : ℤ)

Tactic:
by_cases hx : x ∈ U
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : 𝕜
hx : x ∈ U
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((divisor f U : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
simp [hf.meromorphicOn, hx, (hf x hx).meromorphicOrderAt_nonneg]

Premises used: AnalyticAt.meromorphicOrderAt_nonneg, AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : 𝕜
hx : x ∉ U
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((divisor f U : (a : 𝕜) → ℤ) x : ℤ)

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

Tactic:
ext x
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
e : E
x : 𝕜
h : MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬e = 0 ∨ e = 0
⊢ Eq (α := ℤ) ((divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U : (a : 𝕜) → ℤ) x : ℤ) ((0 : (a : 𝕜) → ℤ) x : ℤ)

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]

Premises used: meromorphicOrderAt_const, ite_eq_left_iff, imp_false, and_imp, Pi.zero_apply, ite_eq_right_iff, LinearOrderedAddCommGroupWithTop.top_ne_zero, Decidable.not_not, WithTop.zero_ne_top, WithTop.untop₀_eq_zero, MeromorphicOn.divisor_def, Function.locallyFinsuppWithin.coe_zero
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
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

Tactic:
tauto
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)
h₁ : ∀ (x : 𝕜), MeromorphicOn.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U → x ∈ U → ¬e = 0 ∨ e = 0
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) U) 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

Premises used: meromorphicOrderAt_const, ite_eq_left_iff, imp_false, and_imp, Pi.zero_apply, ite_eq_right_iff, LinearOrderedAddCommGroupWithTop.top_ne_zero, Decidable.not_not, WithTop.zero_ne_top, WithTop.untop₀_eq_zero, MeromorphicOn.divisor_def, Function.locallyFinsuppWithin.coe_zero
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
n : ℤ
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (↑n : 𝕜 → 𝕜) U) 0

Tactic:
divisor_const (n : 𝕜)

Premises used: Int.cast, MeromorphicOn.divisor_const
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
n : ℕ
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (↑n : 𝕜 → 𝕜) U) 0

Tactic:
divisor_const (n : 𝕜)

Premises used: MeromorphicOn.divisor_const, Nat.cast
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
n : ℕ
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ (↑n : 𝕜)) U) 0

Tactic:
divisor_const (n : 𝕜)

Premises used: MeromorphicOn.divisor_const, Nat.cast
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
n : ℕ
h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) ((OfNat.ofNat n : 𝕜 → 𝕜) x) (↑n : 𝕜)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (OfNat.ofNat n) U) 0

Tactic:
convert! divisor_const (n : 𝕜)

Premises used: MeromorphicOn.divisor_const, Nat.cast
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
n : ℕ
x : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (OfNat.ofNat n x) (↑n : 𝕜)

Tactic:
simp [Semiring.toGrindSemiring_ofNat 𝕜 n]

Premises used: Semiring.toGrindSemiring_ofNat
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)
neg :
  ∀ (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 : ℤ)

Tactic:
by_cases! hz : z ∉ U
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
neg : min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
⊢ LE.le (α := ℤ) (min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z) : ℤ)
    ((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
rw [divisor_apply hf₁ hz, divisor_apply hf₂ hz, divisor_apply (hf₁.add hf₂) hz]

Premises used: MeromorphicOn.add, MeromorphicOn.divisor_apply
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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₀
neg :
  ∀ (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₀

Tactic:
by_cases h₁ : meromorphicOrderAt f₁ z = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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₀

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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₀
neg :
  ∀ (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₀

Tactic:
by_cases h₂ : meromorphicOrderAt f₂ z = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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₀

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 = ⊤
neg : (min (meromorphicOrderAt f₁ z) (meromorphicOrderAt f₂ z)).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

Tactic:
rw [← WithTop.untop₀_min h₁ h₂]

Premises used: WithTop.untop₀_min
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 = ⊤
neg : min (meromorphicOrderAt f₁ z) (meromorphicOrderAt f₂ z) ≤ meromorphicOrderAt (f₁ + f₂) z
⊢ (min (meromorphicOrderAt f₁ z) (meromorphicOrderAt f₂ z)).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

Tactic:
apply WithTop.untop₀_le_untop₀ h₃

Premises used: WithTop.untop₀_le_untop₀
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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) ≤ meromorphicOrderAt (f₁ + f₂) z

Tactic:
meromorphicOrderAt_add (hf₁ z hz) (hf₂ z hz)

Premises used: meromorphicOrderAt_add
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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) ≤ meromorphicOrderAt (f₁ + f₂) z

Tactic:
exact meromorphicOrderAt_add (hf₁ z hz) (hf₂ z hz)

Premises used: meromorphicOrderAt_add
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : 𝕜
pos :
  ∀ (hz : z ∉ U),
    LE.le (α := (fun (a : 𝕜) ↦ ℤ) z) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
      (((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
neg :
  ∀ (hz : z ∈ U),
    LE.le (α := (fun (a : 𝕜) ↦ ℤ) z) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
      (((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
⊢ 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
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : 𝕜
hz : z ∉ U
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) z) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
    (((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : 𝕜
hz : z ∈ U
pos :
  ∀ (hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤),
    LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
      (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
neg :
  ∀ (hf₁₂ : ¬meromorphicOrderAt (f₁ + f₂) z = ⊤),
    LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
      (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
⊢ LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)

Tactic:
by_cases hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤

Premises used: meromorphicOrderAt, HAdd.hAdd
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : 𝕜
hz : z ∈ U
hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤
⊢ LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)

Tactic:
simp [divisor_apply (hf₁.add hf₂) hz, hf₁₂, negPart_nonneg]

Premises used: MeromorphicOn.add, MeromorphicOn.divisor_apply, negPart_nonneg
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : 𝕜
hz : z ∈ U
hf₁₂ : ¬meromorphicOrderAt (f₁ + f₂) z = ⊤
neg :
  LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    ((min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z))⁻ : ℤ)
⊢ LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)

Tactic:
rw [← negPart_min]

Premises used: negPart_min
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : 𝕜
hz : z ∈ U
hf₁₂ : ¬meromorphicOrderAt (f₁ + f₂) z = ⊤
⊢ LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    ((min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z))⁻ : ℤ)

Tactic:
apply ((le_iff_posPart_negPart _ _).1 (min_divisor_le_divisor_add hf₁ hf₂ hz hf₁₂)).2

Premises used: le_iff_posPart_negPart, And.right, MeromorphicOn.min_divisor_le_divisor_add, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
⊢ LE.le (α := Function.locallyFinsuppWithin U ℤ) (divisor (f₁ + f₂) U)⁻ ((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻)

Tactic:
negPart_divisor_add_le_max hf₁ hf₂

Premises used: MeromorphicOn.negPart_divisor_add_le_max
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
pos :
  ∀ (h : LE.le (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻),
    (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤
      HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
neg :
  ∀ (h : ¬LE.le (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻),
    (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤
      HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻

Tactic:
by_cases h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻

Premises used: MeromorphicOn.divisor
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
h : LE.le (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻

Tactic:
simp_all [negPart_nonneg]

Premises used: negPart_nonneg
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
h : ¬LE.le (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻

Tactic:
simp_all [negPart_nonneg]

Premises used: negPart_nonneg
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
calc :
  (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
⊢ (divisor (f₁ + f₂) U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻

Tactic:
calc (divisor (f₁ + f₂) U)⁻
    _ ≤ max (divisor f₁ U)⁻ (divisor f₂ U)⁻ :=
      negPart_divisor_add_le_max hf₁ hf₂
    _ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻ := by
      by_cases h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
      <;> simp_all [negPart_nonneg]

Premises used: MeromorphicOn.divisor, HAdd.hAdd, Max.max, MeromorphicOn.negPart_divisor_add_le_max, NegPart.negPart
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f₁ • f₂) U = HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)

Tactic:
ext z
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
pos :
  ∀ (hz : z ∈ U),
    Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
neg :
  ∀ (hz : z ∉ U),
    Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
by_cases hz : z ∈ U
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
hz : z ∈ U
⊢ meromorphicOrderAt f₁ z ≠ ⊤

Tactic:
(h₂f₁ z hz)
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
hz : z ∈ U
pos :
  ∀ (a₁ : ℤ) (ha₁ : (↑a₁ : WithTop ℤ) = meromorphicOrderAt f₁ z),
    Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
lift meromorphicOrderAt f₁ z to ℤ using (h₂f₁ z hz) with a₁ ha₁

Premises used: meromorphicOrderAt