awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
⊢ AnalyticOnNhd.{u_2, u_7, u_7} 𝕜 (E := A) Ring.inverse {x : A | IsUnit x}

Tactic:
fun _ hx ↦ analyticAt_inverse (IsUnit.unit hx)

Premises used: AnalyticOnNhd, IsUnit.unit, analyticAt_inverse
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
⊢ HasFPowerSeriesOnBall.{u_2, u_8, u_8} (𝕜 := 𝕜) (F := 𝕝) (fun (x : 𝕝) ↦ (1 - x)⁻¹ʳ)
    (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1

Tactic:
hasFPowerSeriesOnBall_inverse_one_sub 𝕜 𝕝

Premises used: hasFPowerSeriesOnBall_inverse_one_sub
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
h : ∀ (x : 𝕝), Eq.{u_8 + 1} (α := 𝕝 → 𝕝) Inv.inv Ring.inverse
⊢ HasFPowerSeriesOnBall.{u_2, u_8, u_8} (𝕜 := 𝕜) (F := 𝕝) (fun (x : 𝕝) ↦ (1 - x)⁻¹)
    (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1

Tactic:
convert! hasFPowerSeriesOnBall_inverse_one_sub 𝕜 𝕝

Premises used: hasFPowerSeriesOnBall_inverse_one_sub
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
x : 𝕝
⊢ Eq.{u_8 + 1} (α := 𝕝 → 𝕝) Inv.inv Ring.inverse

Tactic:
Ring.inverse_eq_inv'.symm

Premises used: Ring.inverse_eq_inv', Eq.symm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
x : 𝕝
⊢ Eq.{u_8 + 1} (α := 𝕝 → 𝕝) Inv.inv Ring.inverse

Tactic:
exact Ring.inverse_eq_inv'.symm

Premises used: Ring.inverse_eq_inv', Eq.symm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
⊢ AnalyticAt 𝕜 (F := 𝕝) (fun (x : 𝕝) ↦ (1 - x)⁻¹) 0

Tactic:
⟨_, ⟨_, hasFPowerSeriesOnBall_inv_one_sub 𝕜 𝕝⟩⟩

Premises used: hasFPowerSeriesOnBall_inv_one_sub, AnalyticAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
z : 𝕝
hz : z ≠ 0
⊢ AnalyticAt 𝕜 Ring.inverse (↑(Units.mk0 z hz : 𝕝ˣ) : 𝕝)

Tactic:
analyticAt_inverse (𝕜 := 𝕜) (Units.mk0 _ hz)

Premises used: Units.mk0, analyticAt_inverse
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
z : 𝕝
hz : z ≠ 0
h : Eq.{u_8 + 1} (α := 𝕝 → 𝕝) Inv.inv Ring.inverse
⊢ AnalyticAt 𝕜 Inv.inv z

Tactic:
convert! analyticAt_inverse (𝕜 := 𝕜) (Units.mk0 _ hz)

Premises used: Units.mk0, analyticAt_inverse
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
z : 𝕝
hz : z ≠ 0
⊢ Eq.{u_8 + 1} (α := 𝕝 → 𝕝) Inv.inv Ring.inverse

Tactic:
Ring.inverse_eq_inv'.symm

Premises used: Ring.inverse_eq_inv', Eq.symm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
z : 𝕝
hz : z ≠ 0
⊢ Eq.{u_8 + 1} (α := 𝕝 → 𝕝) Inv.inv Ring.inverse

Tactic:
exact Ring.inverse_eq_inv'.symm

Premises used: Ring.inverse_eq_inv', Eq.symm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
z : 𝕝
m : Membership.mem (γ := Set 𝕝) {z : 𝕝 | z ≠ 0} z
⊢ AnalyticAt 𝕜 (F := 𝕝) (fun (z : 𝕝) ↦ z⁻¹) z

Tactic:
analyticAt_inv m

Premises used: analyticAt_inv
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
z : 𝕝
m : Membership.mem (γ := Set 𝕝) {z : 𝕝 | z ≠ 0} z
⊢ AnalyticAt 𝕜 (F := 𝕝) (fun (z : 𝕝) ↦ z⁻¹) z

Tactic:
exact analyticAt_inv m

Premises used: analyticAt_inv
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
⊢ AnalyticOn 𝕜 (F := 𝕝) (fun (z : 𝕝) ↦ z⁻¹) {z : 𝕝 | z ≠ 0}

Tactic:
analyticOnNhd_inv.analyticOn

Premises used: AnalyticOnNhd.analyticOn, analyticOnNhd_inv
-- Module: Mathlib.Analysis.Analytic.Constructions
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 → 𝕝
x : E
s : Set E
fa : AnalyticWithinAt 𝕜 f s x
f0 : f x ≠ 0
⊢ AnalyticWithinAt 𝕜 f⁻¹ s x

Tactic:
(analyticAt_inv f0).comp_analyticWithinAt fa

Premises used: AnalyticAt.comp_analyticWithinAt, analyticAt_inv
-- Module: Mathlib.Analysis.Analytic.Constructions
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 → 𝕝
x : E
fa : AnalyticAt 𝕜 f x
f0 : f x ≠ 0
⊢ AnalyticAt 𝕜 f⁻¹ x

Tactic:
(analyticAt_inv f0).comp fa

Premises used: analyticAt_inv, AnalyticAt.comp
-- Module: Mathlib.Analysis.Analytic.Constructions
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 → 𝕝
s : Set E
fa : AnalyticOn 𝕜 f s
f0 : ∀ x ∈ s, f x ≠ 0
⊢ AnalyticOn 𝕜 f⁻¹ s

Tactic:
fun x m ↦ (fa x m).inv (f0 x m)

Premises used: AnalyticOn, AnalyticWithinAt.inv
-- Module: Mathlib.Analysis.Analytic.Constructions
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 → 𝕝
s : Set E
fa : AnalyticOnNhd 𝕜 f s
f0 : ∀ x ∈ s, f x ≠ 0
⊢ AnalyticOnNhd 𝕜 f⁻¹ s

Tactic:
fun x m ↦ (fa x m).inv (f0 x m)

Premises used: AnalyticOnNhd, AnalyticAt.inv
-- Module: Mathlib.Analysis.Analytic.Constructions
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
neg : ∀ (hn : ¬0 ≤ n), AnalyticWithinAt 𝕜 (f ^ n) s z
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z

Tactic:
by_cases hn : 0 ≤ n
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
zpow_nonneg h₁f hn

Premises used: AnalyticWithinAt.zpow_nonneg
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
exact zpow_nonneg h₁f hn

Premises used: AnalyticWithinAt.zpow_nonneg
-- Module: Mathlib.Analysis.Analytic.Constructions
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
neg : AnalyticWithinAt 𝕜 (f ^ (- -n)) s z
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z

Tactic:
rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]

Premises used: Int.eq_neg_comm, Iff.mp, rfl
-- Module: Mathlib.Analysis.Analytic.Constructions
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
arg : f ^ (- -n)
| AnalyticWithinAt 𝕜 (f ^ (- -n)) s z

Tactic:
arg 2
-- Module: Mathlib.Analysis.Analytic.Constructions
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
h : (f ^ (-n))⁻¹ x
| (f ^ (- -n)) x

Tactic:
rw [zpow_neg]

Premises used: zpow_neg
-- Module: Mathlib.Analysis.Analytic.Constructions
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
h : ∀ (x : E), (f ^ (-n))⁻¹ x
| AnalyticWithinAt 𝕜 (f ^ (- -n)) s z

Tactic:
arg 2; intro x; rw [zpow_neg]

Premises used: zpow_neg
-- Module: Mathlib.Analysis.Analytic.Constructions
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
neg : AnalyticWithinAt 𝕜 (f ^ (-n))⁻¹ s z
⊢ AnalyticWithinAt 𝕜 (f ^ (- -n)) s z

Tactic:
conv => arg 2; intro x; rw [zpow_neg]

Premises used: zpow_neg
-- Module: Mathlib.Analysis.Analytic.Constructions
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
linarith₁ : -n < 0 → GT.gt (α := ℤ) 2 0
⊢ 0 ≤ -n

Tactic:
linarith
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)

Premises used: AnalyticWithinAt.inv, AnalyticWithinAt.zpow_nonneg, zpow_ne_zero, Neg.neg
-- Module: Mathlib.Analysis.Analytic.Constructions
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
neg : ∀ (hn : ¬0 ≤ n), AnalyticAt 𝕜 (f ^ n) z
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
by_cases hn : 0 ≤ n
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
zpow_nonneg h₁f hn

Premises used: AnalyticAt.zpow_nonneg
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
exact zpow_nonneg h₁f hn

Premises used: AnalyticAt.zpow_nonneg
-- Module: Mathlib.Analysis.Analytic.Constructions
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
neg : AnalyticAt 𝕜 (f ^ (- -n)) z
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]

Premises used: Int.eq_neg_comm, Iff.mp, rfl
-- Module: Mathlib.Analysis.Analytic.Constructions
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
arg : f ^ (- -n)
| AnalyticAt 𝕜 (f ^ (- -n)) z

Tactic:
arg 2
-- Module: Mathlib.Analysis.Analytic.Constructions
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
h : (f ^ (-n))⁻¹ x
| (f ^ (- -n)) x

Tactic:
rw [zpow_neg]

Premises used: zpow_neg
-- Module: Mathlib.Analysis.Analytic.Constructions
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
h : ∀ (x : E), (f ^ (-n))⁻¹ x
| AnalyticAt 𝕜 (f ^ (- -n)) z

Tactic:
arg 2; intro x; rw [zpow_neg]

Premises used: zpow_neg
-- Module: Mathlib.Analysis.Analytic.Constructions
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
neg : AnalyticAt 𝕜 (f ^ (-n))⁻¹ z
⊢ AnalyticAt 𝕜 (f ^ (- -n)) z

Tactic:
conv => arg 2; intro x; rw [zpow_neg]

Premises used: zpow_neg
-- Module: Mathlib.Analysis.Analytic.Constructions
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
linarith₁ : -n < 0 → GT.gt (α := ℤ) 2 0
⊢ 0 ≤ -n

Tactic:
linarith
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)

Premises used: AnalyticAt.zpow_nonneg, zpow_ne_zero, AnalyticAt.inv, Neg.neg
-- Module: Mathlib.Analysis.Analytic.Constructions
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 → 𝕝
s : Set E
n : ℤ
h₁f : AnalyticOn 𝕜 f s
h₂f : ∀ z ∈ s, f z ≠ 0
⊢ AnalyticOn 𝕜 (f ^ n) s

Tactic:
fun z hz ↦ (h₁f z hz).zpow (h₂f z hz)

Premises used: AnalyticOn, AnalyticWithinAt.zpow
-- Module: Mathlib.Analysis.Analytic.Constructions
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 → 𝕝
s : Set E
n : ℤ
h₁f : AnalyticOnNhd 𝕜 f s
h₂f : ∀ z ∈ s, f z ≠ 0
⊢ AnalyticOnNhd 𝕜 (f ^ n) s

Tactic:
fun z hz ↦ (h₁f z hz).zpow (h₂f z hz)

Premises used: AnalyticOnNhd, AnalyticAt.zpow
-- Module: Mathlib.Analysis.Analytic.Constructions
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
mpr : AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z → AnalyticAt 𝕜 g z
⊢ AnalyticAt 𝕜 g z ↔ AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (z : E) ↦ f z • g z) z

Tactic:
constructor
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
fun a ↦ h₁f.smul a

Premises used: AnalyticAt.smul
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
exact fun a ↦ h₁f.smul a

Premises used: AnalyticAt.smul
-- Module: Mathlib.Analysis.Analytic.Constructions
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
mpr₁ : g =ᶠ[𝓝 z] (f⁻¹ • f) • g
⊢ AnalyticAt 𝕜 g z

Tactic:
rw [analyticAt_congr (g := (f⁻¹ • f) • g), smul_assoc]

Premises used: smul_assoc, analyticAt_congr
-- Module: Mathlib.Analysis.Analytic.Constructions
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 𝕜 (f⁻¹ • f • g) z

Tactic:
(h₁f.inv h₂f).fun_smul hprod

Premises used: AnalyticAt.fun_smul, AnalyticAt.inv
-- Module: Mathlib.Analysis.Analytic.Constructions
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 𝕜 (f⁻¹ • f • g) z

Tactic:
exact (h₁f.inv h₂f).fun_smul hprod

Premises used: AnalyticAt.fun_smul, AnalyticAt.inv
-- Module: Mathlib.Analysis.Analytic.Constructions
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
h : ∀ a ∈ f ⁻¹' {0}ᶜ, g a = ((f⁻¹ • f) • g) a
⊢ g =ᶠ[𝓝 z] (f⁻¹ • f) • g

Tactic:
filter_upwards [h₁f.continuousAt.preimage_mem_nhds (compl_singleton_mem_nhds_iff.2 h₂f)]

Premises used: Iff.mpr, ContinuousAt.preimage_mem_nhds, compl_singleton_mem_nhds_iff, AnalyticAt.continuousAt
-- Module: Mathlib.Analysis.Analytic.Constructions
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}ᶜ
⊢ ¬f y = 0

Tactic:
rw [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff] at hy

Premises used: Set.mem_singleton_iff, Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Analysis.Analytic.Constructions
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 : ¬f y = 0
⊢ g y = ((f⁻¹ • f) • g) y

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.Analytic.Constructions
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 𝕜 (f • g) z

Tactic:
analyticAt_iff_analytic_fun_smul h₁f h₂f

Premises used: analyticAt_iff_analytic_fun_smul
-- Module: Mathlib.Analysis.Analytic.Constructions
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
simp_rw : AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f • g) z
⊢ AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z

Tactic:
simp_rw [← smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
analyticAt_iff_analytic_smul h₁f h₂f

Premises used: analyticAt_iff_analytic_smul
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
exact analyticAt_iff_analytic_smul h₁f h₂f

Premises used: analyticAt_iff_analytic_smul