awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
inl : ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0), (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
⊢ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
have inr : ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0), (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
Tactic: rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
⊢ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
have h : ∀ (a : 𝕜) (ha : ∀ᶠ (x : 𝕜) in 𝓝 a, f x = 0), a ∈ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ
Tactic: filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁f.eventually_nhds] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
⊢ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
have h : ∀ (a : 𝕜) (ha : f a ≠ 0), a ∈ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ
Tactic: filter_upwards [h₁f] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
x : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : f x ≠ 0
hx : x ∈ U
hU : IsConnected U
⊢ f ⁻¹' {0}ᶜ ∈ codiscreteWithin U
have h : ∀ (a : 𝕜) (ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤) (h₂a : a ∈ U), a ∈ f ⁻¹' {0}ᶜ
Tactic: filter_upwards [h₁f.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top,
    self_mem_codiscreteWithin U] with a ha h₂a
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
x : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : f x ≠ 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
⊢ a ∈ f ⁻¹' {0}ᶜ
have h : ∀ (h₂f : analyticOrderAt f x = 0) (hx : x ∈ U) (hU : IsConnected U) (a : 𝕜)
  (ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤) (h₂a : a ∈ U), a ∈ f ⁻¹' {0}ᶜ
Tactic: rw [← (h₁f x hx).analyticOrderAt_eq_zero] at h₂f
Cleared hypotheses: h₂f, hx, hU, a, ha, h₂a
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
x : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : analyticOrderAt f x = 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
u : (↑U : Type u_1)
⊢ analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have a₁ : ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: apply (h₁f.exists_analyticOrderAt_ne_top_iff_forall hU).1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
x : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : analyticOrderAt f x = 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
u : (↑U : Type u_1)
⊢ ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have h : analyticOrderAt f (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) x hx) : 𝕜) ≠ ⊤
Tactic: use ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
x : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : analyticOrderAt f x = 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
⊢ a ∈ f ⁻¹' {0}ᶜ
have this : ∀ {u : (↑U : Type u_1)}, analyticOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: have {u : U} : analyticOrderAt f u ≠ ⊤ := by
    apply (h₁f.exists_analyticOrderAt_ne_top_iff_forall hU).1
    use ⟨x, hx⟩
    simp_all
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z = ⊤ ↔ f = 0
have refine : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0), EqOn f 0 univ
Tactic: refine analyticOrderAt_eq_top.trans ⟨fun h ↦ eqOn_univ .. |>.mp ?_, by simp +contextual⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0
⊢ EqOn f 0 univ
have apply : ∃ᶠ (z : 𝕜) in 𝓝[≠] z, f z = 0
Tactic: apply eqOn_zero_of_preconnected_of_frequently_eq_zero (fun z _ ↦ hf z) isPreconnected_univ trivial
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
⊢ (∀ z ∈ s, analyticOrderAt f z = ⊤) ↔ EqOn f 0 s
have refine : ∀ (hzero : EqOn f 0 s) (z : 𝕜) (hz : z ∈ s), analyticOrderAt f z = ⊤
Tactic: refine ⟨(EventuallyEq.eq_of_nhds <| analyticOrderAt_eq_top.mp <| · · ·), fun hzero z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
hzero : EqOn f 0 s
z : 𝕜
hz : z ∈ s
⊢ analyticOrderAt f z = ⊤
have apply : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0
Tactic: apply analyticOrderAt_eq_top.mpr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
hzero : EqOn f 0 s
z : 𝕜
hz : z ∈ s
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0
have h : ∀ a ∈ s, f a = 0
Tactic: filter_upwards [hs.mem_nhds hz]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p : A[X]
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z
have refine_1 : ∀ (k : A),
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) k : A[X])) s z
Tactic: refine p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p : A[X]
refine_1 :
  ∀ (k : A),
    AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
      (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) k : A[X])) s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z
have refine_2 : ∀ (p q : A[X]) (hp : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z)
  (hq : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) q) s z),
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) (p + q)) s z
Tactic: refine p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p : A[X]
refine_1 :
  ∀ (k : A),
    AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
      (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) k : A[X])) s z
refine_2 :
  ∀ (p q : A[X]) (hp : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z)
    (hq : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) q) s z),
    AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) (p + q)) s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z
have refine_3 : ∀ (p : ℕ) (i : A)
  (hp :
    AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
      (fun (x : E) ↦
        (aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)))
      s z),
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))))
    s z
Tactic: refine p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p : A[X]
k : A
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) k : A[X])) s z
have refine_1 : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (algebraMap A B : (a : A) → B) k) s z
Tactic: simp_rw [aeval_C]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 p q : A[X]
hp : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z
hq : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) q) s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) (p + q)) s z
have refine_2 : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
  (fun (x : E) ↦
    HAdd.hAdd (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) p : B) ((aeval (f x) : (a : A[X]) → B) q : B))
  s z
Tactic: simp_rw [aeval_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 : A[X]
p : ℕ
i : A
hp :
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)))
    s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))))
    s z
have h : ∀ (x : E),
  (aeval (f x) : (a : A[X]) → B)
      (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))) =
    HMul.hMul (α := B)
      ((aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
        B)
      (f x)
Tactic: convert! hp.mul hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 : A[X]
p : ℕ
i : A
hp :
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)))
    s z
x : E
⊢ (aeval (f x) : (a : A[X]) → B)
      (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))) =
    HMul.hMul (α := B)
      ((aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
        B)
      (f x)
have h : (aeval (f x) : (a : A[X]) → B) (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p * X)) =
  HMul.hMul (α := B)
    ((aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
      B)
    (f x)
Tactic: simp_rw [pow_succ, aeval_mul, ← mul_assoc, aeval_X]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 : A[X]
p : ℕ
i : A
hp :
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)))
    s z
x : E
h :
  (aeval (f x) : (a : A[X]) → B)
      (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p * X)) =
    HMul.hMul (α := B)
      ((aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
        B)
      (f x)
⊢ (aeval (f x) : (a : A[X]) → B)
      (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))) =
    HMul.hMul (α := B)
      ((aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
        B)
      (f x)
have h₁ : HMul.hMul (α := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
    (HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B)
      ((aeval (f x) : (a : A[X]) → B) X : B)) =
  HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
      ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B) *
    f x
Tactic: simp_rw [pow_succ, aeval_mul, ← mul_assoc, aeval_X]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 : A[X]
p : ℕ
i : A
hp :
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)))
    s z
x : E
h :
  (aeval (f x) : (a : A[X]) → B)
      (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p * X)) =
    HMul.hMul (α := B)
      ((aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
        B)
      (f x)
h₁ :
  HMul.hMul (α := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
      (HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B)
        ((aeval (f x) : (a : A[X]) → B) X : B)) =
    HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
        ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B) *
      f x
⊢ (aeval (f x) : (a : A[X]) → B)
      (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))) =
    HMul.hMul (α := B)
      ((aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
        B)
      (f x)
have h₂ : HMul.hMul (β := B)
    (HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
      ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B))
    ((aeval (f x) : (a : A[X]) → B) X : B) =
  HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
      ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B) *
    f x
Tactic: simp_rw [pow_succ, aeval_mul, ← mul_assoc, aeval_X]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticAt 𝕜 f z
p : A[X]
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) z
have rw : ∀ (hf : AnalyticWithinAt 𝕜 f Set.univ z) (p : A[X]),
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) Set.univ z
Tactic: rw [← analyticWithinAt_univ] at hf ⊢
Cleared hypotheses: hf, p
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p : MvPolynomial σ A
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
have apply : ∀ (k : A),
  AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) ((C : (a : A) → MvPolynomial σ A) k : MvPolynomial σ A)) z
Tactic: apply p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p : MvPolynomial σ A
apply :
  ∀ (k : A),
    AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
      (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) ((C : (a : A) → MvPolynomial σ A) k : MvPolynomial σ A))
      z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
have apply₁ : ∀ (p q : MvPolynomial σ A)
  (hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z)
  (hq : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) q) z),
  AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) (p + q)) z
Tactic: apply p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p : MvPolynomial σ A
apply :
  ∀ (k : A),
    AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
      (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) ((C : (a : A) → MvPolynomial σ A) k : MvPolynomial σ A))
      z
apply₁ :
  ∀ (p q : MvPolynomial σ A)
    (hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z)
    (hq : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) q) z),
    AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) (p + q)) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
have apply₂ : ∀ (p : MvPolynomial σ A) (i : σ)
  (hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z),
  AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) (p * X i)) z
Tactic: apply p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p : MvPolynomial σ A
k : A
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) ((C : (a : A) → MvPolynomial σ A) k : MvPolynomial σ A)) z
have simp_rw : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (algebraMap A B : (a : A) → B) k) z
Tactic: simp_rw [aeval_C]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p_1 p q : MvPolynomial σ A
hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
hq : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) q) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) (p + q)) z
have simp_rw : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
  (fun (x : E) ↦
    HAdd.hAdd (α := B) (β := B) ((aeval (f x) : (a : MvPolynomial σ A) → B) p : B)
      ((aeval (f x) : (a : MvPolynomial σ A) → B) q : B))
  z
Tactic: simp_rw [map_add]