awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : (z : 𝕜') → F := fun (z : 𝕜') ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
⊢ AnalyticAt.{u_1, u_1, u_4} 𝕜 (F := F) (fun (i : 𝕜) ↦ (h i)⁻¹ ^ r • j (g i)) x

Tactic:
have : AnalyticAt 𝕜 (fun i ↦ (h i)⁻¹ ^ r • j (g i)) x :=
      ((han.fun_inv hne).fun_pow r).fun_smul (hr.restrictScalars.comp' hg)
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : (z : 𝕜') → F := fun (z : 𝕜') ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt.{u_1, u_1, u_4} 𝕜 (F := F) (fun (i : 𝕜) ↦ (h i)⁻¹ ^ r • j (g i)) x
⊢ MeromorphicAt (f ∘ g) x

Tactic:
⟨n * r, this.congr ?_⟩

Premises used: HMul.hMul, Exists.intro, AnalyticAt.congr, MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : (z : 𝕜') → F := fun (z : 𝕜') ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt.{u_1, u_1, u_4} 𝕜 (F := F) (fun (i : 𝕜) ↦ (h i)⁻¹ ^ r • j (g i)) x
neg :
  EventuallyEq.{u_1, u_4} (β := F) (𝓝 x) (fun (i : 𝕜) ↦ (h i)⁻¹ ^ r • j (g i)) fun (z : 𝕜) ↦
    (z - x) ^ (n * r) • (f ∘ g) z
⊢ MeromorphicAt (f ∘ g) x

Tactic:
refine ⟨n * r, this.congr ?_⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : (z : 𝕜') → F := fun (z : 𝕜') ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt.{u_1, u_1, u_4} 𝕜 (F := F) (fun (i : 𝕜) ↦ (h i)⁻¹ ^ r • j (g i)) x
h₁ :
  ∀ (z : 𝕜) (hz : g z - g x = (z - x) ^ n • h z) (hzne : h z ≠ 0), (h z)⁻¹ ^ r • j (g z) = (z - x) ^ (n * r) • (f ∘ g) z
⊢ EventuallyEq.{u_1, u_4} (β := F) (𝓝 x) (fun (i : 𝕜) ↦ (h i)⁻¹ ^ r • j (g i)) fun (z : 𝕜) ↦
    (z - x) ^ (n * r) • (f ∘ g) z

Tactic:
filter_upwards [heq, han.continuousAt.tendsto.eventually_ne hne] with z hz hzne

Premises used: Filter.Tendsto.eventually_ne, ContinuousAt.tendsto, AnalyticAt.continuousAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : (z : 𝕜') → F := fun (z : 𝕜') ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt.{u_1, u_1, u_4} 𝕜 (F := F) (fun (i : 𝕜) ↦ (h i)⁻¹ ^ r • j (g i)) x
z : 𝕜
hz : g z - g x = (z - x) ^ n • h z
hzne : h z ≠ 0
h₁ : (g z - g x) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)
⊢ (h z)⁻¹ ^ r • j (g z) = (z - x) ^ (n * r) • (f ∘ g) z

Tactic:
simp only [j, inv_pow, Function.comp_apply, inv_smul_eq_iff₀ (pow_ne_zero r hzne)]

Premises used: pow_ne_zero, inv_pow, inv_smul_eq_iff₀, Function.comp_apply
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : (z : 𝕜') → F := fun (z : 𝕜') ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt.{u_1, u_1, u_4} 𝕜 (F := F) (fun (i : 𝕜) ↦ (h i)⁻¹ ^ r • j (g i)) x
z : 𝕜
hz : g z - g x = (z - x) ^ n • h z
hzne : h z ≠ 0
h₁ : ((z - x) ^ n • h z) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)
h₂ : ((z - x) ^ n • h z) ^ r • f (g z) = (z - x) ^ (n * r) • h z ^ r • f (g z)
h₃ : ((z - x) ^ n • h z) ^ r • f (g z) = ((z - x) ^ (n * r) • h z ^ r) • f (g z)
h₄ : ((z - x) ^ n • h z) ^ r • f (g z) = (((z - x) ^ n) ^ r • h z ^ r) • f (g z)
h₅ h₆ : (((z - x) ^ n) ^ r • h z ^ r) • f (g z) = (((z - x) ^ n) ^ r • h z ^ r) • f (g z)
⊢ (g z - g x) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)

Tactic:
rw [hz, smul_comm, ← smul_assoc, pow_mul, smul_pow]

Premises used: smul_assoc, pow_mul, smul_pow, SMulCommClass.smul_comm
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
⊢ MeromorphicAt f (g x) → MeromorphicAt (f ∘ g) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
refine : ∀ (hf : MeromorphicAt (f ∘ g) x), MeromorphicAt f (g x)
⊢ MeromorphicAt (f ∘ g) x ↔ MeromorphicAt f (g x)

Tactic:
refine ⟨fun hf ↦ ?_, by fun_prop⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
hf : MeromorphicAt (f ∘ g) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
⊢ AnalyticAt 𝕜 r (g x)

Tactic:
have hra : AnalyticAt 𝕜 r (g x) := hg.analyticAt_localInverse hg'
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
hf : MeromorphicAt (f ∘ g) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hra : AnalyticAt 𝕜 r (g x)
⊢ r (g x) = x

Tactic:
have : r (g x) = x := HasStrictFDerivAt.localInverse_apply_image ..
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
hf : MeromorphicAt (f ∘ g) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hra : AnalyticAt 𝕜 r (g x)
this : r (g x) = x
⊢ MeromorphicAt (f ∘ g) (r (g x))

Tactic:
rw [← this] at hf
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
hf : MeromorphicAt (f ∘ g) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hra : AnalyticAt 𝕜 r (g x)
this : r (g x) = x
hf₁ : MeromorphicAt (f ∘ g) (r (g x))
⊢ AnalyticAt 𝕜 r (g x)

Tactic:
rw [← this] at hf
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
hf : MeromorphicAt (f ∘ g) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hra : AnalyticAt 𝕜 r (g x)
this : r (g x) = x
hf₁ : MeromorphicAt (f ∘ g) (r (g x))
hra₁ : AnalyticAt 𝕜 r (g x)
⊢ r (g x) = x

Tactic:
rw [← this] at hf
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hf : MeromorphicAt (f ∘ g) (r (g x))
hra : AnalyticAt 𝕜 r (g x)
this : r (g x) = x
⊢ MeromorphicAt f (g x)

Tactic:
(hf.comp_analyticAt hra).congr (.filter_mono ?_ nhdsWithin_le_nhds)

Premises used: Filter.EventuallyEq.filter_mono, MeromorphicAt.comp_analyticAt, nhdsWithin_le_nhds, MeromorphicAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hf : MeromorphicAt (f ∘ g) (r (g x))
hra : AnalyticAt 𝕜 r (g x)
this : r (g x) = x
refine : (f ∘ g) ∘ r =ᶠ[𝓝 (g x)] f
⊢ MeromorphicAt f (g x)

Tactic:
refine (hf.comp_analyticAt hra).congr (.filter_mono ?_ nhdsWithin_le_nhds)

Premises used: Filter.EventuallyEq.filter_mono, MeromorphicAt.comp_analyticAt, nhdsWithin_le_nhds, MeromorphicAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hf : MeromorphicAt (f ∘ g) (r (g x))
hra : AnalyticAt 𝕜 r (g x)
this : r (g x) = x
⊢ (f ∘ g) ∘ r =ᶠ[𝓝 (g x)] f

Tactic:
EventuallyEq.fun_comp (HasStrictDerivAt.eventually_right_inverse ..) f

Premises used: HasStrictDerivAt.eventually_right_inverse, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hf : MeromorphicAt (f ∘ g) (r (g x))
hra : AnalyticAt 𝕜 r (g x)
this : r (g x) = x
⊢ (f ∘ g) ∘ r =ᶠ[𝓝 (g x)] f

Tactic:
exact EventuallyEq.fun_comp (HasStrictDerivAt.eventually_right_inverse ..) f

Premises used: HasStrictDerivAt.eventually_right_inverse, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
⊢ MeromorphicOn f U

Tactic:
fun x hx ↦ (hf x hx).meromorphicAt

Premises used: MeromorphicOn, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : f =ᶠ[codiscreteWithin U] g
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
apply : f =ᶠ[𝓝[≠] x] g
⊢ MeromorphicAt g x

Tactic:
apply (hf x hx).congr

Premises used: MeromorphicAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : f =ᶠ[codiscreteWithin U] g
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
⊢ ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x

Tactic:
simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
    disjoint_principal_right] at h₁

Premises used: Filter.Eventually, Filter.EventuallyEq, mem_codiscreteWithin, Filter.disjoint_principal_right
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x
h : ∀ (a : 𝕜) (ha : a ∈ (U \ {x : 𝕜 | f x = g x})ᶜ), f a = g a
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
filter_upwards [h₁ x hx] with a ha
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x
a : 𝕜
ha : a ∈ (U \ {x : 𝕜 | f x = g x})ᶜ
⊢ a ∈ U → f a = g a

Tactic:
simp at ha
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x
a : 𝕜
ha : a ∈ U → f a = g a
h : ∀ (ha : a ∉ U), f a = g a
h₃ : ∀ (ha : f a = g a), f a = g a
h₄ : ∀ (ha : a ∉ U), f a = g a
h₅ : ∀ (ha : f a = g a), f a = g a
h₆ : ∀ (ha : a ∉ U), f a = g a
h₇ : ∀ (ha : f a = g a), f a = g a
h₈ h₉ h₁₀ h₁₁ h₁₂ : ∀ (ha : a ∉ U), f a = g a
⊢ f a = g a

Tactic:
tauto
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : f =ᶠ[codiscreteWithin U] g
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
apply : f =ᶠ[𝓝[≠] x] g
⊢ MeromorphicAt g x

Tactic:
apply (hf x hx).congr

Premises used: MeromorphicAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : f =ᶠ[codiscreteWithin U] g
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
⊢ ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x

Tactic:
simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
    disjoint_principal_right] at h₁

Premises used: Filter.Eventually, Filter.EventuallyEq, mem_codiscreteWithin, Filter.disjoint_principal_right
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x
apply : ∃ (u : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
⊢ U ∈ 𝓝[≠] x

Tactic:
apply mem_nhdsWithin.mpr

Premises used: Iff.mpr, mem_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x
w : Set 𝕜
left : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
left₁ : x ∈ U
right : U ∩ {x}ᶜ ⊆ U
⊢ ∃ (u : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U

Tactic:
use U, h₂, hx, Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x
⊢ U ∈ 𝓝[≠] x

Tactic:
have : U ∈ 𝓝[≠] x := by
    apply mem_nhdsWithin.mpr
    use U, h₂, hx, Set.inter_subset_left
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
h : ∀ (a : 𝕜) (h₁a : a ∈ U) (h₂a : a ∈ (U \ {x : 𝕜 | f x = g x})ᶜ), f a = g a
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
filter_upwards [this, h₁ x hx] with a h₁a h₂a
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
h₂a : a ∈ (U \ {x : 𝕜 | f x = g x})ᶜ
⊢ a ∈ U → ¬¬f a = g a

Tactic:
simp only [Set.mem_compl_iff, Set.mem_diff, Set.mem_setOf_eq, not_and] at h₂a

Premises used: Set.mem_setOf_eq, Set.mem_diff, not_and, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
h₂a : a ∈ U → ¬¬f a = g a
h : ∀ (h₂a : a ∉ U), f a = g a
h₃ h₄ h₅ : ∀ (h₂a : ¬¬f a = g a), f a = g a
h₆ h₇ h₈ : ∀ (h₂a : f a = g a), f a = g a
⊢ f a = g a

Tactic:
tauto
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
h₁ : f =ᶠ[codiscreteWithin U] g
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ MeromorphicOn f U ↔ MeromorphicOn g U

Tactic:
⟨(·.congr_codiscreteWithin h₁ h₂), (·.congr_codiscreteWithin h₁.symm h₂)⟩

Premises used: MeromorphicOn.congr_codiscreteWithin, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
⊢ MeromorphicOn _root_.id U

Tactic:
fun x _ ↦ .id x

Premises used: MeromorphicOn, MeromorphicAt.id
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
e : E
U : Set 𝕜
⊢ MeromorphicOn.{u_1, u_3} (E := E) (fun (x : 𝕜) ↦ e) U

Tactic:
fun x _ ↦ .const e x

Premises used: MeromorphicAt.const, MeromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
V : Set 𝕜
hv : V ⊆ U
⊢ MeromorphicOn f V

Tactic:
fun x hx ↦ hf x (hv hx)

Premises used: MeromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hg : MeromorphicOn g U
⊢ MeromorphicOn (f + g) U

Tactic:
fun x hx ↦ (hf x hx).add (hg x hx)

Premises used: MeromorphicOn, MeromorphicAt.add
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hg : MeromorphicOn g U
⊢ MeromorphicOn (f - g) U

Tactic:
fun x hx ↦ (hf x hx).sub (hg x hx)

Premises used: MeromorphicOn, MeromorphicAt.sub
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ MeromorphicOn (-f) U

Tactic:
fun x hx ↦ (hf x hx).neg

Premises used: MeromorphicOn, MeromorphicAt.neg
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicOn (-f) U
⊢ MeromorphicOn f U

Tactic:
simpa only [neg_neg] using h.neg

Premises used: neg_neg, MeromorphicOn.neg
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
s : 𝕜 → 𝕜
hs : MeromorphicOn s U
f : 𝕜 → E
hf : MeromorphicOn f U
⊢ MeromorphicOn (s • f) U

Tactic:
fun x hx ↦ (hs x hx).smul (hf x hx)

Premises used: MeromorphicOn, MeromorphicAt.smul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s t : 𝕜 → 𝕜'
U : Set 𝕜
hs : MeromorphicOn s U
ht : MeromorphicOn t U
⊢ MeromorphicOn (s * t) U

Tactic:
fun x hx ↦ (hs x hx).mul (ht x hx)

Premises used: MeromorphicAt.mul, MeromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_4
s : Finset ι
f : ι → 𝕜 → 𝕜'
h : ∀ σ ∈ s, MeromorphicOn (f σ) U
⊢ MeromorphicOn.{u_1, u_2} (E := 𝕜') (∏ n ∈ s, f n) U

Tactic:
fun z hz ↦ MeromorphicAt.prod (h · · z hz)

Premises used: MeromorphicOn, MeromorphicAt.prod
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_4
s : Finset ι
f : ι → 𝕜 → 𝕜'
h : ∀ σ ∈ s, MeromorphicOn (f σ) U
⊢ MeromorphicOn.{u_1, u_2} (E := 𝕜') (fun (z : 𝕜) ↦ ∏ n ∈ s, f n z) U

Tactic:
fun z hz ↦ MeromorphicAt.fun_prod (h · · z hz)

Premises used: MeromorphicOn, MeromorphicAt.fun_prod
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_4
f : ι → 𝕜 → 𝕜'
h : ∀ (σ : ι), MeromorphicOn (f σ) U
⊢ MeromorphicOn.{u_1, u_2} (E := 𝕜') (∏ᶠ (n : ι), f n) U

Tactic:
fun z hz ↦ MeromorphicAt.finprod (h · z hz)

Premises used: MeromorphicOn, MeromorphicAt.finprod