awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
z : 𝕝
hz : z ≠ 0
⊢ AnalyticAt 𝕜 Inv.inv z
have h : Eq.{u_8 + 1} (α := 𝕝 → 𝕝) Inv.inv Ring.inverse
Tactic: convert! analyticAt_inverse (𝕜 := 𝕜) (Units.mk0 _ hz)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z
have pos : ∀ (hn : 0 ≤ n), AnalyticWithinAt 𝕜 (f ^ n) s z
Tactic: by_cases hn : 0 ≤ n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
pos : ∀ (hn : 0 ≤ n), AnalyticWithinAt 𝕜 (f ^ n) s z
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z
have neg : ∀ (hn : ¬0 ≤ n), AnalyticWithinAt 𝕜 (f ^ n) s z
Tactic: by_cases hn : 0 ≤ n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z
have neg : AnalyticWithinAt 𝕜 (f ^ (- -n)) s z
Tactic: rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
| AnalyticWithinAt 𝕜 (f ^ (- -n)) s z
have arg : f ^ (- -n)
Tactic: arg 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
x : E
| (f ^ (- -n)) x
have h : (f ^ (-n))⁻¹ x
Tactic: rw [zpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
| AnalyticWithinAt 𝕜 (f ^ (- -n)) s z
have h : ∀ (x : E), (f ^ (-n))⁻¹ x
Tactic: arg 2; intro x; rw [zpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticWithinAt 𝕜 (f ^ (- -n)) s z
have neg : AnalyticWithinAt 𝕜 (f ^ (-n))⁻¹ s z
Tactic: conv => arg 2; intro x; rw [zpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ 0 ≤ -n
have linarith : -n < 0 → HMul.hMul (α := ℤ) 2 (-1) + (n + 1 - 0) + (-n + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
linarith : -n < 0 → HMul.hMul (α := ℤ) 2 (-1) + (n + 1 - 0) + (-n + 1 - 0) = 0
⊢ 0 ≤ -n
have linarith₁ : -n < 0 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
⊢ AnalyticAt 𝕜 (f ^ n) z
have pos : ∀ (hn : 0 ≤ n), AnalyticAt 𝕜 (f ^ n) z
Tactic: by_cases hn : 0 ≤ n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
pos : ∀ (hn : 0 ≤ n), AnalyticAt 𝕜 (f ^ n) z
⊢ AnalyticAt 𝕜 (f ^ n) z
have neg : ∀ (hn : ¬0 ≤ n), AnalyticAt 𝕜 (f ^ n) z
Tactic: by_cases hn : 0 ≤ n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ n) z
have neg : AnalyticAt 𝕜 (f ^ (- -n)) z
Tactic: rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
| AnalyticAt 𝕜 (f ^ (- -n)) z
have arg : f ^ (- -n)
Tactic: arg 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
x : E
| (f ^ (- -n)) x
have h : (f ^ (-n))⁻¹ x
Tactic: rw [zpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
| AnalyticAt 𝕜 (f ^ (- -n)) z
have h : ∀ (x : E), (f ^ (-n))⁻¹ x
Tactic: arg 2; intro x; rw [zpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ (- -n)) z
have neg : AnalyticAt 𝕜 (f ^ (-n))⁻¹ z
Tactic: conv => arg 2; intro x; rw [zpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ 0 ≤ -n
have linarith : -n < 0 → HMul.hMul (α := ℤ) 2 (-1) + (n + 1 - 0) + (-n + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
linarith : -n < 0 → HMul.hMul (α := ℤ) 2 (-1) + (n + 1 - 0) + (-n + 1 - 0) = 0
⊢ 0 ≤ -n
have linarith₁ : -n < 0 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕝 : Type u_8
inst_5 : NormedDivisionRing 𝕝
inst_6 : NormedAlgebra 𝕜 𝕝
inst_7 : Module 𝕝 F
inst_8 : IsBoundedSMul 𝕝 F
inst_9 : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
⊢ AnalyticAt 𝕜 g z ↔ AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z
have mp : AnalyticAt 𝕜 g z → AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕝 : Type u_8
inst_5 : NormedDivisionRing 𝕝
inst_6 : NormedAlgebra 𝕜 𝕝
inst_7 : Module 𝕝 F
inst_8 : IsBoundedSMul 𝕝 F
inst_9 : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
mp : AnalyticAt 𝕜 g z → AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z
⊢ AnalyticAt 𝕜 g z ↔ AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z
have mpr : AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z → AnalyticAt 𝕜 g z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕝 : Type u_8
inst_5 : NormedDivisionRing 𝕝
inst_6 : NormedAlgebra 𝕜 𝕝
inst_7 : Module 𝕝 F
inst_8 : IsBoundedSMul 𝕝 F
inst_9 : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z
⊢ AnalyticAt 𝕜 g z
have mpr : AnalyticAt 𝕜 (f⁻¹ • f • g) z
Tactic: rw [analyticAt_congr (g := (f⁻¹ • f) • g), smul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕝 : Type u_8
inst_5 : NormedDivisionRing 𝕝
inst_6 : NormedAlgebra 𝕜 𝕝
inst_7 : Module 𝕝 F
inst_8 : IsBoundedSMul 𝕝 F
inst_9 : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z
mpr : AnalyticAt 𝕜 (f⁻¹ • f • g) z
⊢ AnalyticAt 𝕜 g z
have mpr₁ : g =ᶠ[𝓝 z] (f⁻¹ • f) • g
Tactic: rw [analyticAt_congr (g := (f⁻¹ • f) • g), smul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕝 : Type u_8
inst_5 : NormedDivisionRing 𝕝
inst_6 : NormedAlgebra 𝕜 𝕝
inst_7 : Module 𝕝 F
inst_8 : IsBoundedSMul 𝕝 F
inst_9 : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z
⊢ g =ᶠ[𝓝 z] (f⁻¹ • f) • g
have h : ∀ a ∈ f ⁻¹' {0}ᶜ, g a = ((f⁻¹ • f) • g) a
Tactic: filter_upwards [h₁f.continuousAt.preimage_mem_nhds (compl_singleton_mem_nhds_iff.2 h₂f)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕝 : Type u_8
inst_5 : NormedDivisionRing 𝕝
inst_6 : NormedAlgebra 𝕜 𝕝
inst_7 : Module 𝕝 F
inst_8 : IsBoundedSMul 𝕝 F
inst_9 : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z
y : E
hy : y ∈ f ⁻¹' {0}ᶜ
⊢ g y = ((f⁻¹ • f) • g) y
have hy₁ : ¬f y = 0
Tactic: rw [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
⊢ AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z
have simp_rw : AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f • g) z
Tactic: simp_rw [← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
s : Set E
x : E
fa : AnalyticWithinAt 𝕜 f s x
ga : AnalyticWithinAt 𝕜 g s x
g0 : g x ≠ 0
⊢ AnalyticWithinAt.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x / g x) s x
have simp_rw : AnalyticWithinAt.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x * (g x)⁻¹) s x
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
x : E
fa : AnalyticAt 𝕜 f x
ga : AnalyticAt 𝕜 g x
g0 : g x ≠ 0
⊢ AnalyticAt 𝕜 (f / g) x
have simp_rw : AnalyticAt 𝕜 (f * g⁻¹) x
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ ∅, f n) s c
have empty : AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) 0 s c
Tactic: simp only [Finset.sum_empty]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB : ∀ (h : ∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c), AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ B, f n) s c
h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ insert a B, f n) s c
have insert : AnalyticWithinAt 𝕜 (f a + ∑ n ∈ B, f n) s c
Tactic: simp_rw [Finset.sum_insert aB]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB : ∀ (h : ∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c), AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ B, f n) s c
h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (f a + ∑ n ∈ B, f n) s c
have h₁ : ∀ (n : α), n = a ∨ n ∈ B → AnalyticWithinAt 𝕜 (f n) s c
Tactic: simp only [Finset.mem_insert] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) s c
have empty : ∀ (h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c),
  AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ ∅, f n) s c
Tactic: induction N using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.sum_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
empty :
  ∀ (h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ ∅, f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) s c
have insert : ∀ (a : α) (B : Finset α) (aB : a ∉ B)
  (hB : ∀ (h : ∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c), AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ B, f n) s c)
  (h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c),
  AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ insert a B, f n) s c
Tactic: induction N using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.sum_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) s c
have empty : ∀ (h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c),
  AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ ∅, f n) s c
Tactic: classical
  induction N using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.sum_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
empty :
  ∀ (h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ ∅, f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) s c
have insert : ∀ (a : α) (B : Finset α) (aB : a ∉ B)
  (hB : ∀ (h : ∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c), AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ B, f n) s c)
  (h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c),
  AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ insert a B, f n) s c
Tactic: classical
  induction N using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.sum_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : α → E → F
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
⊢ AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) c
have simp_rw : ∀ (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) Set.univ c),
  AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) Set.univ c
Tactic: simp_rw [← analyticWithinAt_univ] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ ∅, f n z) s c
have empty : AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ 1) s c
Tactic: simp only [Finset.prod_empty]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB :
  ∀ (h : ∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ B, f n z) s c
h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ insert a B, f n z) s c
have insert : AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ f a z * ∏ n ∈ B, f n z) s c
Tactic: simp_rw [Finset.prod_insert aB]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB :
  ∀ (h : ∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ B, f n z) s c
h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ f a z * ∏ n ∈ B, f n z) s c
have h₁ : ∀ (n : α), n = a ∨ n ∈ B → AnalyticWithinAt 𝕜 (f n) s c
Tactic: simp only [Finset.mem_insert] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) s c
have empty : ∀ (h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c),
  AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ ∅, f n z) s c
Tactic: induction N using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.prod_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))
Cleared hypotheses: N, h