awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hg : AnalyticWithinAt 𝕜 g s x
⊢ AnalyticWithinAt 𝕜 (f + g) s x

Tactic:
let ⟨_, hpf⟩ := hf
  let ⟨_, hqf⟩ := hg
  (hpf.add hqf).analyticWithinAt

Premises used: HasFPowerSeriesWithinAt.analyticWithinAt, AnalyticWithinAt, _private.0.AnalyticWithinAt.add.match_1, HAdd.hAdd, HasFPowerSeriesWithinAt.add
-- 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
f g : E → F
x : E
hf : AnalyticAt 𝕜 f x
hg : AnalyticAt 𝕜 g x
⊢ AnalyticAt 𝕜 (f + g) x

Tactic:
let ⟨_, hpf⟩ := hf
  let ⟨_, hqf⟩ := hg
  (hpf.add hqf).analyticAt

Premises used: HasFPowerSeriesAt.add, HAdd.hAdd, AnalyticAt, HasFPowerSeriesAt.analyticAt, _private.0.AnalyticAt.add.match_1
-- 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
f g : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
hg : AnalyticOn 𝕜 g s
⊢ AnalyticOn 𝕜 (f + g) s

Tactic:
fun z hz => (hf z hz).add (hg z hz)

Premises used: AnalyticOn, AnalyticWithinAt.add
-- 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
f g : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
hg : AnalyticOnNhd 𝕜 g s
⊢ AnalyticOnNhd 𝕜 (f + g) s

Tactic:
fun z hz => (hf z hz).add (hg z hz)

Premises used: AnalyticOnNhd, AnalyticAt.add
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
rw : r ≤ pf.radius
⊢ r ≤ (-pf).radius

Tactic:
rw [pf.radius_neg]

Premises used: FormalMultilinearSeries.radius_neg
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ pf.radius

Tactic:
hf.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ pf.radius

Tactic:
exact hf.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
rw : r ≤ pf.radius
⊢ r ≤ (-pf).radius

Tactic:
rw [pf.radius_neg]

Premises used: FormalMultilinearSeries.radius_neg
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ pf.radius

Tactic:
hf.r_le

Premises used: HasFPowerSeriesOnBall.r_le
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ pf.radius

Tactic:
exact hf.r_le

Premises used: HasFPowerSeriesOnBall.r_le
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
⊢ HasFPowerSeriesWithinAt (-f) (-pf) s x

Tactic:
let ⟨_, hrf⟩ := hf
  hrf.neg.hasFPowerSeriesWithinAt

Premises used: _private.0.HasFPowerSeriesWithinAt.neg.match_1, HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt, HasFPowerSeriesWithinAt, HasFPowerSeriesWithinOnBall.neg, Neg.neg
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
⊢ HasFPowerSeriesAt (-f) (-pf) x

Tactic:
let ⟨_, hrf⟩ := hf
  hrf.neg.hasFPowerSeriesAt

Premises used: HasFPowerSeriesOnBall.neg, HasFPowerSeriesOnBall.hasFPowerSeriesAt, HasFPowerSeriesAt, _private.0.HasFPowerSeriesAt.neg.match_1, Neg.neg
-- 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
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 (-f) s x

Tactic:
let ⟨_, hpf⟩ := hf
  hpf.neg.analyticWithinAt

Premises used: HasFPowerSeriesWithinAt.analyticWithinAt, AnalyticWithinAt, _private.0.AnalyticWithinAt.add.match_1, HasFPowerSeriesWithinAt.neg, Neg.neg
-- 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
f : E → F
x : E
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (-f) x

Tactic:
let ⟨_, hpf⟩ := hf
  hpf.neg.analyticAt

Premises used: HasFPowerSeriesAt.neg, AnalyticAt, Neg.neg, HasFPowerSeriesAt.analyticAt, _private.0.AnalyticAt.add.match_1
-- 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
f : E → F
x : E
hf : AnalyticAt 𝕜 (-f) x
⊢ AnalyticAt 𝕜 f x

Tactic:
simpa using hf.neg

Premises used: AnalyticAt.neg
-- 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
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
⊢ AnalyticOn 𝕜 (-f) s

Tactic:
fun z hz ↦ (hf z hz).neg

Premises used: AnalyticOn, AnalyticWithinAt.neg
-- 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
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (-f) s

Tactic:
fun z hz ↦ (hf z hz).neg

Premises used: AnalyticOnNhd, AnalyticAt.neg
-- 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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
hg : HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: sub_eq_add_neg, HasFPowerSeriesWithinOnBall.neg, HasFPowerSeriesWithinOnBall.add
-- 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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
hg : HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesOnBall (f - g) (pf - pg) x r

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: HasFPowerSeriesOnBall.add, sub_eq_add_neg, HasFPowerSeriesOnBall.neg
-- 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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
hg : HasFPowerSeriesWithinAt g pg s x
⊢ HasFPowerSeriesWithinAt (f - g) (pf - pg) s x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: sub_eq_add_neg, HasFPowerSeriesWithinAt.neg, HasFPowerSeriesWithinAt.add
-- 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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
⊢ HasFPowerSeriesAt (f - g) (pf - pg) x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: HasFPowerSeriesAt.neg, HasFPowerSeriesAt.add, sub_eq_add_neg
-- 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
f g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hg : AnalyticWithinAt 𝕜 g s x
⊢ AnalyticWithinAt 𝕜 (f - g) s x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: sub_eq_add_neg, AnalyticWithinAt.add, AnalyticWithinAt.neg
-- 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
f g : E → F
x : E
hf : AnalyticAt 𝕜 f x
hg : AnalyticAt 𝕜 g x
⊢ AnalyticAt 𝕜 (f - g) x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: sub_eq_add_neg, AnalyticAt.add, AnalyticAt.neg
-- 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
f g : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
hg : AnalyticOn 𝕜 g s
⊢ AnalyticOn 𝕜 (f - g) s

Tactic:
fun z hz => (hf z hz).sub (hg z hz)

Premises used: AnalyticWithinAt.sub, AnalyticOn
-- 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
f g : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
hg : AnalyticOnNhd 𝕜 g s
⊢ AnalyticOnNhd 𝕜 (f - g) s

Tactic:
fun z hz => (hf z hz).sub (hg z hz)

Premises used: AnalyticOnNhd, AnalyticAt.sub
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
R : Type u_9
inst_5 : NormedRing R
inst_6 : Module R F
inst_7 : IsBoundedSMul R F
inst_8 : SMulCommClass 𝕜 R F
c : R
hf : HasFPowerSeriesWithinAt f pf s x
⊢ HasFPowerSeriesWithinAt (c • f) (c • pf) s x

Tactic:
let ⟨_, hrf⟩ := hf
  hrf.const_smul.hasFPowerSeriesWithinAt

Premises used: _private.0.HasFPowerSeriesWithinAt.neg.match_1, HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt, HasFPowerSeriesWithinOnBall.const_smul, HasFPowerSeriesWithinAt, HSMul.hSMul
-- 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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
R : Type u_9
inst_5 : NormedRing R
inst_6 : Module R F
inst_7 : IsBoundedSMul R F
inst_8 : SMulCommClass 𝕜 R F
c : R
hf : HasFPowerSeriesAt f pf x
⊢ HasFPowerSeriesAt (c • f) (c • pf) x

Tactic:
let ⟨_, hrf⟩ := hf
  hrf.const_smul.hasFPowerSeriesAt

Premises used: HasFPowerSeriesOnBall.const_smul, HSMul.hSMul, HasFPowerSeriesOnBall.hasFPowerSeriesAt, HasFPowerSeriesAt, _private.0.HasFPowerSeriesAt.neg.match_1
-- 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
f : E → F
s : Set E
x : E
R : Type u_9
inst_5 : NormedRing R
inst_6 : Module R F
inst_7 : IsBoundedSMul R F
inst_8 : SMulCommClass 𝕜 R F
c : R
hf : AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 (c • f) s x

Tactic:
let ⟨_, hpf⟩ := hf
  hpf.const_smul.analyticWithinAt

Premises used: HasFPowerSeriesWithinAt.const_smul, HasFPowerSeriesWithinAt.analyticWithinAt, AnalyticWithinAt, _private.0.AnalyticWithinAt.add.match_1, HSMul.hSMul
-- 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
f : E → F
x : E
R : Type u_9
inst_5 : NormedRing R
inst_6 : Module R F
inst_7 : IsBoundedSMul R F
inst_8 : SMulCommClass 𝕜 R F
c : R
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (c • f) x

Tactic:
let ⟨_, hpf⟩ := hf
  hpf.const_smul.analyticAt

Premises used: HasFPowerSeriesAt.const_smul, AnalyticAt, HSMul.hSMul, HasFPowerSeriesAt.analyticAt, _private.0.AnalyticAt.add.match_1
-- 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
f : E → F
s : Set E
R : Type u_9
inst_5 : NormedRing R
inst_6 : Module R F
inst_7 : IsBoundedSMul R F
inst_8 : SMulCommClass 𝕜 R F
c : R
hf : AnalyticOn 𝕜 f s
⊢ AnalyticOn 𝕜 (c • f) s

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

Premises used: AnalyticWithinAt.const_smul, AnalyticOn
-- 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
f : E → F
s : Set E
R : Type u_9
inst_5 : NormedRing R
inst_6 : Module R F
inst_7 : IsBoundedSMul R F
inst_8 : SMulCommClass 𝕜 R F
c : R
hf : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (c • f) s

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

Premises used: AnalyticOnNhd, AnalyticAt.const_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 𝕜 𝕝
s : Set E
x : E
f : E → 𝕝
hf : AnalyticWithinAt 𝕜 f s x
c : 𝕝
⊢ AnalyticWithinAt.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x / c) s x

Tactic:
simpa [div_eq_mul_inv] using hf.const_smul (R := 𝕝ᵐᵒᵖ)

Premises used: AnalyticWithinAt.const_smul, 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 𝕜 𝕝
x : E
f : E → 𝕝
hf : AnalyticAt 𝕜 f x
c : 𝕝
⊢ AnalyticAt.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x / c) x

Tactic:
simpa [div_eq_mul_inv] using hf.const_smul (R := 𝕝ᵐᵒᵖ)

Premises used: div_eq_mul_inv, AnalyticAt.const_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 𝕜 𝕝
s : Set E
f : E → 𝕝
hf : AnalyticOn 𝕜 f s
c : 𝕝
⊢ AnalyticOn.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x / c) s

Tactic:
simpa [div_eq_mul_inv] using hf.const_smul (R := 𝕝ᵐᵒᵖ)

Premises used: AnalyticOn.const_smul, 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 𝕜 𝕝
s : Set E
f : E → 𝕝
hf : AnalyticOnNhd 𝕜 f s
c : 𝕝
⊢ AnalyticOnNhd.{u_2, u_3, u_8} 𝕜 (F := 𝕝) (fun (x : E) ↦ f x / c) s

Tactic:
simpa [div_eq_mul_inv] using hf.const_smul (R := 𝕝ᵐᵒᵖ)

Premises used: div_eq_mul_inv, AnalyticOnNhd.const_smul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
a : (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G) ≤ min p.radius q.radius
a₁ : min p.radius q.radius ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
⊢ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G) = min p.radius q.radius

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
⊢ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G) ≤ min p.radius q.radius

Tactic:
ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
a :
  ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)), (↑r : ℝ≥0∞) ≤ min p.radius q.radius
⊢ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G) ≤ min p.radius q.radius

Tactic:
refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
a : (↑r : ℝ≥0∞) ≤ p.radius ∧ (↑r : ℝ≥0∞) ≤ q.radius
⊢ (↑r : ℝ≥0∞) ≤ min p.radius q.radius

Tactic:
rw [le_min_iff]

Premises used: le_min_iff
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1

Tactic:
have := (p.prod q).isLittleO_one_of_lt_radius hr
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
a : (↑r : ℝ≥0∞) ≤ p.radius
a₁ : (↑r : ℝ≥0∞) ≤ q.radius
⊢ (↑r : ℝ≥0∞) ≤ p.radius ∧ (↑r : ℝ≥0∞) ≤ q.radius

Tactic:
constructor
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1

Tactic:
(isBigO_of_le _ fun n ↦ ?_).trans this.isBigO

Premises used: Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
a : ∀ (n : ℕ), ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1

Tactic:
refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO

Premises used: Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
n : ℕ
a : ‖p n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖
⊢ ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖

Tactic:
rw [norm_mul, norm_norm, norm_mul, norm_norm]

Premises used: norm_mul, norm_norm