awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → 𝕝
s : Set E
x : E
fa : AnalyticWithinAt 𝕜 f s x
ga : AnalyticWithinAt 𝕜 g s x
g0 : g x ≠ 0
simp_rw : AnalyticWithinAt.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x * (g x)⁻¹) s x
⊢ AnalyticWithinAt.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x / g x) s x

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_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 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

Tactic:
fa.mul (ga.inv g0)

Premises used: AnalyticWithinAt.inv, AnalyticWithinAt.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 → 𝕝
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

Tactic:
exact fa.mul (ga.inv g0)

Premises used: AnalyticWithinAt.inv, AnalyticWithinAt.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 → 𝕝
x : E
fa : AnalyticAt 𝕜 f x
ga : AnalyticAt 𝕜 g x
g0 : g x ≠ 0
simp_rw : AnalyticAt 𝕜 (f * g⁻¹) x
⊢ AnalyticAt 𝕜 (f / g) x

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_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 g : E → 𝕝
x : E
fa : AnalyticAt 𝕜 f x
ga : AnalyticAt 𝕜 g x
g0 : g x ≠ 0
⊢ AnalyticAt 𝕜 (f * g⁻¹) x

Tactic:
fa.mul (ga.inv g0)

Premises used: AnalyticAt.mul, 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 g : E → 𝕝
x : E
fa : AnalyticAt 𝕜 f x
ga : AnalyticAt 𝕜 g x
g0 : g x ≠ 0
⊢ AnalyticAt 𝕜 (f * g⁻¹) x

Tactic:
exact fa.mul (ga.inv g0)

Premises used: AnalyticAt.mul, 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 g : E → 𝕝
s : Set E
fa : AnalyticOn 𝕜 f s
ga : AnalyticOn 𝕜 g s
g0 : ∀ x ∈ s, g x ≠ 0
⊢ AnalyticOn.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x / g x) s

Tactic:
fun x m ↦
  (fa x m).div (ga x m) (g0 x m)

Premises used: AnalyticOn, AnalyticWithinAt.div
-- 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 → 𝕝
s : Set E
fa : AnalyticOnNhd 𝕜 f s
ga : AnalyticOnNhd 𝕜 g s
g0 : ∀ x ∈ s, g x ≠ 0
⊢ AnalyticOnNhd.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x / g x) s

Tactic:
fun x m ↦
  (fa x m).div (ga x m) (g0 x m)

Premises used: AnalyticOnNhd, AnalyticAt.div
-- Module: Mathlib.Analysis.Analytic.Constructions
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
empty : AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) 0 s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ ∅, f n) s c

Tactic:
simp only [Finset.sum_empty]

Premises used: Finset.sum_empty
-- Module: Mathlib.Analysis.Analytic.Constructions
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) 0 s c

Tactic:
analyticWithinAt_const

Premises used: analyticWithinAt_const
-- Module: Mathlib.Analysis.Analytic.Constructions
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) 0 s c

Tactic:
exact analyticWithinAt_const

Premises used: analyticWithinAt_const
-- Module: Mathlib.Analysis.Analytic.Constructions
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.insert a B, AnalyticWithinAt 𝕜 (f n) s c
insert : AnalyticWithinAt 𝕜 (f a + ∑ n ∈ B, f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ Insert.insert a B, f n) s c

Tactic:
simp_rw [Finset.sum_insert aB]

Premises used: Finset.sum_insert
-- Module: Mathlib.Analysis.Analytic.Constructions
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
⊢ ∀ (n : α), n = a ∨ n ∈ B → AnalyticWithinAt 𝕜 (f n) s c

Tactic:
simp only [Finset.mem_insert] at h

Premises used: Finset.mem_insert
-- Module: Mathlib.Analysis.Analytic.Constructions
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 : α), n = a ∨ n ∈ B → AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (f a + ∑ n ∈ B, f n) s c

Tactic:
(h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))

Premises used: AnalyticWithinAt.add, Or.inl, Or.inr, rfl
-- Module: Mathlib.Analysis.Analytic.Constructions
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 : α), n = a ∨ n ∈ B → AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (f a + ∑ n ∈ B, f n) s c

Tactic:
exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))

Premises used: AnalyticWithinAt.add, Or.inl, Or.inr, rfl
-- Module: Mathlib.Analysis.Analytic.Constructions
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
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.insert a B, AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ Insert.insert a B, f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ 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))

Premises used: analyticWithinAt_const, Insert.insert, Finset.mem_insert, Finset.sum_empty
-- Module: Mathlib.Analysis.Analytic.Constructions
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
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.insert a B, AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ Insert.insert a B, f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ 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))

Premises used: analyticWithinAt_const, Insert.insert, Finset.mem_insert, Finset.sum_empty
-- Module: Mathlib.Analysis.Analytic.Constructions
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
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
⊢ AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) c

Tactic:
simp_rw [← analyticWithinAt_univ] at h ⊢

Premises used: analyticWithinAt_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
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, AnalyticWithinAt 𝕜 (f n) Set.univ c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) Set.univ c

Tactic:
N.analyticWithinAt_sum h

Premises used: Finset.analyticWithinAt_sum
-- Module: Mathlib.Analysis.Analytic.Constructions
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, AnalyticWithinAt 𝕜 (f n) Set.univ c
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) Set.univ c

Tactic:
exact N.analyticWithinAt_sum h

Premises used: Finset.analyticWithinAt_sum
-- Module: Mathlib.Analysis.Analytic.Constructions
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
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s
⊢ AnalyticOn.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) s

Tactic:
fun z zs ↦ N.analyticWithinAt_sum (fun n m ↦ h n m z zs)

Premises used: AnalyticOn, Finset.analyticWithinAt_sum
-- Module: Mathlib.Analysis.Analytic.Constructions
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
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s
⊢ AnalyticOnNhd.{u_2, u_3, u_4} 𝕜 (F := F) (∑ n ∈ N, f n) s

Tactic:
fun z zs ↦ N.analyticAt_sum (fun n m ↦ h n m z zs)

Premises used: AnalyticOnNhd, Finset.analyticAt_sum
-- Module: Mathlib.Analysis.Analytic.Constructions
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
empty : AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ 1) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ ∅, f n z) s c

Tactic:
simp only [Finset.prod_empty]

Premises used: Finset.prod_empty
-- Module: Mathlib.Analysis.Analytic.Constructions
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) ↦ 1) s c

Tactic:
analyticWithinAt_const

Premises used: analyticWithinAt_const
-- Module: Mathlib.Analysis.Analytic.Constructions
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) ↦ 1) s c

Tactic:
exact analyticWithinAt_const

Premises used: analyticWithinAt_const
-- Module: Mathlib.Analysis.Analytic.Constructions
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.insert a B, AnalyticWithinAt 𝕜 (f n) s c
insert : AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ f a z * ∏ n ∈ B, f n z) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ Insert.insert a B, f n z) s c

Tactic:
simp_rw [Finset.prod_insert aB]

Premises used: Finset.prod_insert
-- Module: Mathlib.Analysis.Analytic.Constructions
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
⊢ ∀ (n : α), n = a ∨ n ∈ B → AnalyticWithinAt 𝕜 (f n) s c

Tactic:
simp only [Finset.mem_insert] at h

Premises used: Finset.mem_insert
-- Module: Mathlib.Analysis.Analytic.Constructions
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 : α), n = a ∨ n ∈ 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

Tactic:
(h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))

Premises used: Or.inl, Or.inr, rfl, AnalyticWithinAt.mul
-- Module: Mathlib.Analysis.Analytic.Constructions
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 : α), n = a ∨ n ∈ 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

Tactic:
exact (h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))

Premises used: Or.inl, Or.inr, rfl, AnalyticWithinAt.mul
-- Module: Mathlib.Analysis.Analytic.Constructions
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
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
insert :
  ∀ (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.insert a B, AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ Insert.insert a B, f n z) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ 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))

Premises used: Finset.prod_empty, analyticWithinAt_const, Insert.insert, Finset.mem_insert
-- Module: Mathlib.Analysis.Analytic.Constructions
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
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
insert :
  ∀ (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.insert a B, AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ Insert.insert a B, f n z) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) s c

Tactic:
classical
  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))

Premises used: Finset.prod_empty, analyticWithinAt_const, Insert.insert, Finset.mem_insert
-- Module: Mathlib.Analysis.Analytic.Constructions
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

Tactic:
N.analyticWithinAt_fun_prod h

Premises used: Finset.analyticWithinAt_fun_prod
-- Module: Mathlib.Analysis.Analytic.Constructions
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
h₁ : ∀ (x : E), Eq.{u_9 + 1} (α := A) ((∏ n ∈ N, f n) x) (∏ n ∈ N, f n x)
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (∏ n ∈ N, f n) s c

Tactic:
convert! N.analyticWithinAt_fun_prod h

Premises used: Finset.analyticWithinAt_fun_prod
-- Module: Mathlib.Analysis.Analytic.Constructions
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
x : E
⊢ Eq.{u_9 + 1} (α := A) ((∏ n ∈ N, f n) x) (∏ n ∈ N, f n x)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
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
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
simp_rw :
  ∀ (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) Set.univ c),
    AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) Set.univ c
⊢ AnalyticAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) c

Tactic:
simp_rw [← analyticWithinAt_univ] at h ⊢

Premises used: analyticWithinAt_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
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
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) Set.univ c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) Set.univ c

Tactic:
N.analyticWithinAt_fun_prod h

Premises used: Finset.analyticWithinAt_fun_prod
-- Module: Mathlib.Analysis.Analytic.Constructions
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
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) Set.univ c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) Set.univ c

Tactic:
exact N.analyticWithinAt_fun_prod h

Premises used: Finset.analyticWithinAt_fun_prod
-- 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_9
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) c

Tactic:
N.analyticAt_fun_prod h

Premises used: Finset.analyticAt_fun_prod
-- 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_9
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
h₁ : ∀ (x : E), Eq.{u_10 + 1} (α := A) ((∏ n ∈ N, f n) x) (∏ n ∈ N, f n x)
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ n ∈ N, f n) c

Tactic:
convert! N.analyticAt_fun_prod h

Premises used: Finset.analyticAt_fun_prod