awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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 : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x
have neg : ∀ (n : ℕ) (hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x),
  MeromorphicAt (f ∘ g) x
Tactic: obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp hg'
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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 : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
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
⊢ MeromorphicAt (f ∘ g) x
have neg : ∀ (h : 𝕜 → 𝕜') (han : AnalyticAt 𝕜 h x) (hne : h x ≠ 0) (heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z),
  MeromorphicAt (f ∘ g) x
Tactic: obtain ⟨h, han, hne, heq⟩ := (hg.fun_sub analyticAt_const).analyticOrderAt_eq_natCast.mp hn.symm
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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)
⊢ MeromorphicAt (f ∘ g) x
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
have 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
Tactic: refine ⟨n * r, this.congr ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ EventuallyEq.{u_1, u_4} (β := F) (𝓝 x) (fun (i : 𝕜) ↦ (h i)⁻¹ ^ r • j (g i)) fun (z : 𝕜) ↦
    (z - x) ^ (n * r) • (f ∘ g) z
have 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
Tactic: filter_upwards [heq, han.continuousAt.tendsto.eventually_ne hne] with z hz hzne
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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)⁻¹ ^ r • j (g z) = (z - x) ^ (n * r) • (f ∘ g) z
have h₁ : (g z - g x) ^ r • f (g z) = h z ^ r • (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)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ (g z - g x) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)
have h₁ : ((z - x) ^ n • h z) ^ 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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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)
⊢ (g z - g x) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)
have h₂ : ((z - x) ^ n • h z) ^ r • f (g z) = (z - x) ^ (n * r) • h z ^ r • f (g z)
Tactic: rw [hz, smul_comm, ← smul_assoc, pow_mul, smul_pow]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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)
⊢ (g z - g x) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)
have h₃ : ((z - x) ^ n • h z) ^ r • f (g z) = ((z - x) ^ (n * r) • h z ^ r) • f (g z)
Tactic: rw [hz, smul_comm, ← smul_assoc, pow_mul, smul_pow]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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)
⊢ (g z - g x) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)
have h₄ : ((z - x) ^ n • h z) ^ r • f (g z) = (((z - x) ^ n) ^ r • h z ^ r) • f (g z)
Tactic: rw [hz, smul_comm, ← smul_assoc, pow_mul, smul_pow]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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)
⊢ (g z - g x) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)
have h₅ : (((z - x) ^ n) ^ r • h z ^ r) • f (g z) = (((z - x) ^ n) ^ r • h z ^ r) • f (g z)
Tactic: rw [hz, smul_comm, ← smul_assoc, pow_mul, smul_pow]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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)
have refine : ∀ (hf : MeromorphicAt (f ∘ g) x), MeromorphicAt f (g x)
Tactic: refine ⟨fun hf ↦ ?_, by fun_prop⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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'
⊢ MeromorphicAt f (g x)
have hra : AnalyticAt 𝕜 r (g x)
Tactic: have hra : AnalyticAt 𝕜 r (g x) := hg.analyticAt_localInverse hg'
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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)
⊢ MeromorphicAt f (g x)
have this : r (g x) = x
Tactic: have : r (g x) = x := HasStrictFDerivAt.localInverse_apply_image ..
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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 x)
have hf₁ : MeromorphicAt (f ∘ g) (r (g x))
Tactic: rw [← this] at hf
Cleared hypotheses: hf, hra, this
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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)
have refine : (f ∘ g) ∘ r =ᶠ[𝓝 (g x)] f
Tactic: refine (hf.comp_analyticAt hra).congr (.filter_mono ?_ nhdsWithin_le_nhds)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ MeromorphicAt g x
have apply : f =ᶠ[𝓝[≠] x] g
Tactic: apply (hf x hx).congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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
⊢ f =ᶠ[𝓝[≠] x] g
have h₃ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g 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.Basic (goal)
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
⊢ f =ᶠ[𝓝[≠] x] g
have h : ∀ (a : 𝕜) (ha : a ∈ (U \ {x : 𝕜 | f x = g x})ᶜ), f a = g a
Tactic: filter_upwards [h₁ x hx] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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})ᶜ
⊢ f a = g a
have ha₁ : a ∈ U → f a = g a
Tactic: simp at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ f a = g a
have h : ∀ (ha : a ∉ U), f a = g a
Tactic: tauto
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ f a = g a
have h₃ : ∀ (ha : f a = g a), f a = g a
Tactic: tauto
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ MeromorphicAt g x
have apply : f =ᶠ[𝓝[≠] x] g
Tactic: apply (hf x hx).congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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
⊢ f =ᶠ[𝓝[≠] x] g
have h₃ : ∀ x ∈ U, (U \ {x : 𝕜 | f x = g 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.Basic (goal)
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
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.Basic (goal)
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
⊢ ∃ (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.Basic (hypothesis)
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
⊢ f =ᶠ[𝓝[≠] x] g
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.Basic (goal)
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
⊢ f =ᶠ[𝓝[≠] x] g
have h : ∀ (a : 𝕜) (h₁a : a ∈ U) (h₂a : a ∈ (U \ {x : 𝕜 | f x = g x})ᶜ), f a = g a
Tactic: filter_upwards [this, h₁ x hx] with a h₁a h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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})ᶜ
⊢ f a = g a
have h₂a₁ : 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
Cleared hypotheses: h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ f a = g a
have h : ∀ (h₂a : a ∉ U), f a = g a
Tactic: tauto
Cleared hypotheses: h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ f a = g a
have h₃ : ∀ (h₂a : ¬¬f a = g a), f a = g a
Tactic: tauto
Cleared hypotheses: h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ f a = g a
have h₆ : ∀ (h₂a : f a = g a), f a = g a
Tactic: tauto
Cleared hypotheses: h₂a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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_eq : EqOn f g U
hu : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ MeromorphicOn g U
have refine : ∀ (x : 𝕜) (hx : x ∈ U), f =ᶠ[𝓝 x] g
Tactic: refine fun x hx ↦ (hf x hx).congr (EventuallyEq.filter_mono ?_ nhdsWithin_le_nhds)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
⊢ ∀ᶠ (y : 𝕜) in codiscreteWithin U, AnalyticAt 𝕜 f y
have rw : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ {x : 𝕜 | AnalyticAt 𝕜 f x}))
Tactic: rw [eventually_iff, mem_codiscreteWithin]