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
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
neg :
  f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0)
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      z ^ n • (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0)
have neg₁ : z ^ n ≠ 0
Tactic: rw [smul_inv_smul₀]
-- 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 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ z ^ n ≠ 0
have neg : ∀ (hz : z ^ n = 0), z ∈ U
Tactic: contrapose hz
Cleared hypotheses: 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
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
have obtain : ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
  (hF :
    ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z),
  ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
Tactic: classical
  obtain ⟨F, hFa, hF⟩ := hf.exists_eventuallyEq_sum_add_pow_mul n
  obtain ⟨U, hU0, hU'⟩ := by rwa [eventually_iff_exists_mem] at hF
  refine ⟨fun z ↦ if z ∈ U then F z else (z ^ n)⁻¹ • (f z
      - (∑ i ∈ .range n, (z ^ i / i.factorial) • iteratedDeriv i f 0)), ?_, fun z ↦ ?_⟩
  · exact hFa.congr (by filter_upwards [hU0] using by simp +contextual)
  · by_cases hz : z ∈ U
    · simpa [hz] using hU' z hz
    · simp only [if_neg hz]
      rw [smul_inv_smul₀]
      · module
      · contrapose hz
        exact (pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0
-- 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 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
obtain :
  ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
    (hF :
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z),
    ∃ (F : 𝕜 → E),
      AnalyticAt 𝕜 F 0 ∧
        ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
have obtain₁ : ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
  (hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z)
  (U : Set 𝕜) (hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U)
  (hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y),
  ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
Tactic: classical
  obtain ⟨F, hFa, hF⟩ := hf.exists_eventuallyEq_sum_add_pow_mul n
  obtain ⟨U, hU0, hU'⟩ := by rwa [eventually_iff_exists_mem] at hF
  refine ⟨fun z ↦ if z ∈ U then F z else (z ^ n)⁻¹ • (f z
      - (∑ i ∈ .range n, (z ^ i / i.factorial) • iteratedDeriv i f 0)), ?_, fun z ↦ ?_⟩
  · exact hFa.congr (by filter_upwards [hU0] using by simp +contextual)
  · by_cases hz : z ∈ U
    · simpa [hz] using hU' z hz
    · simp only [if_neg hz]
      rw [smul_inv_smul₀]
      · module
      · contrapose hz
        exact (pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0
-- 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 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
obtain :
  ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
    (hF :
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z),
    ∃ (F : 𝕜 → E),
      AnalyticAt 𝕜 F 0 ∧
        ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
obtain₁ :
  ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
    (hF :
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z)
    (U : Set 𝕜) (hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U)
    (hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y),
    ∃ (F : 𝕜 → E),
      AnalyticAt 𝕜 F 0 ∧
        ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
have refine_1 : ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
  (hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z)
  (U : Set 𝕜) (hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U)
  (hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y),
  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
    (fun (z : 𝕜) ↦
      if z ∈ U then F z
      else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
    0
Tactic: classical
  obtain ⟨F, hFa, hF⟩ := hf.exists_eventuallyEq_sum_add_pow_mul n
  obtain ⟨U, hU0, hU'⟩ := by rwa [eventually_iff_exists_mem] at hF
  refine ⟨fun z ↦ if z ∈ U then F z else (z ^ n)⁻¹ • (f z
      - (∑ i ∈ .range n, (z ^ i / i.factorial) • iteratedDeriv i f 0)), ?_, fun z ↦ ?_⟩
  · exact hFa.congr (by filter_upwards [hU0] using by simp +contextual)
  · by_cases hz : z ∈ U
    · simpa [hz] using hU' z hz
    · simp only [if_neg hz]
      rw [smul_inv_smul₀]
      · module
      · contrapose hz
        exact (pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0
-- 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 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
obtain :
  ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
    (hF :
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z),
    ∃ (F : 𝕜 → E),
      AnalyticAt 𝕜 F 0 ∧
        ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
obtain₁ :
  ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
    (hF :
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z)
    (U : Set 𝕜) (hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U)
    (hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y),
    ∃ (F : 𝕜 → E),
      AnalyticAt 𝕜 F 0 ∧
        ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
refine_1 :
  ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
    (hF :
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z)
    (U : Set 𝕜) (hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U)
    (hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y),
    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
      (fun (z : 𝕜) ↦
        if z ∈ U then F z
        else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
      0
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
have refine_2 : ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
  (hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z)
  (U : Set 𝕜) (hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U)
  (hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y) (z : 𝕜),
  f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      HSMul.hSMul (β := E) (z ^ n)
        ((fun (z : 𝕜) ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
          z)
Tactic: classical
  obtain ⟨F, hFa, hF⟩ := hf.exists_eventuallyEq_sum_add_pow_mul n
  obtain ⟨U, hU0, hU'⟩ := by rwa [eventually_iff_exists_mem] at hF
  refine ⟨fun z ↦ if z ∈ U then F z else (z ^ n)⁻¹ • (f z
      - (∑ i ∈ .range n, (z ^ i / i.factorial) • iteratedDeriv i f 0)), ?_, fun z ↦ ?_⟩
  · exact hFa.congr (by filter_upwards [hU0] using by simp +contextual)
  · by_cases hz : z ∈ U
    · simpa [hz] using hU' z hz
    · simp only [if_neg hz]
      rw [smul_inv_smul₀]
      · module
      · contrapose hz
        exact (pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
⊢ analyticOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z₀) n) z₀ = (↑n : ℕ∞)
have rw : ∃ (g : 𝕜 → 𝕜),
  AnalyticAt 𝕜 g z₀ ∧
    g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z₀) n z = (z - z₀) ^ n • g z
Tactic: rw [AnalyticAt.analyticOrderAt_eq_natCast (by fun_prop)]
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have pos : ∀ (hg_nc : EventuallyConst g (𝓝 z₀)),
  analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
Tactic: by_cases hg_nc : EventuallyConst g (𝓝 z₀)
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
pos :
  ∀ (hg_nc : EventuallyConst g (𝓝 z₀)),
    analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have neg : ∀ (hg_nc : ¬EventuallyConst g (𝓝 z₀)),
  analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
Tactic: by_cases hg_nc : EventuallyConst g (𝓝 z₀)
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have this : EventuallyConst (f ∘ g) (𝓝 z₀)
Tactic: have := hg_nc.comp f
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
this : EventuallyConst (f ∘ g) (𝓝 z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have hg_nc₁ : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
Tactic: rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc this
Cleared hypotheses: hg_nc, this
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
this : EventuallyConst (f ∘ g) (𝓝 z₀)
hg_nc₁ : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have this₁ : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
Tactic: rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc this
Cleared hypotheses: hg_nc, this
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have pos : analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
Tactic: rw [hg_nc]
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
have pos : ∀ (hf' : f (g z₀) = 0), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
Tactic: by_cases hf' : f (g z₀) = 0
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
pos : ∀ (hf' : f (g z₀) = 0), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
have neg : ∀ (hf' : ¬f (g z₀) = 0), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
Tactic: by_cases hf' : f (g z₀) = 0
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : ¬f (g z₀) = 0
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
have neg : analyticOrderAt (f ∘ g) z₀ = 0
Tactic: rw [show analyticOrderAt f (g z₀) = 0 from ?_, zero_mul]
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : ¬f (g z₀) = 0
neg : analyticOrderAt (f ∘ g) z₀ = 0
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
have rw : analyticOrderAt f (g z₀) = 0
Tactic: rw [show analyticOrderAt f (g z₀) = 0 from ?_, zero_mul]
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have pos : ∀ (hf' : analyticOrderAt f (g z₀) = ⊤),
  analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
Tactic: by_cases hf' : analyticOrderAt f (g z₀) = ⊤
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
pos :
  ∀ (hf' : analyticOrderAt f (g z₀) = ⊤),
    analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have neg : ∀ (hf' : ¬analyticOrderAt f (g z₀) = ⊤),
  analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
Tactic: by_cases hf' : analyticOrderAt f (g z₀) = ⊤
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have pos : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ ≠ 0
Tactic: rw [hf', analyticOrderAt_eq_top.mpr
      (EventuallyEq.comp_tendsto (analyticOrderAt_eq_top.mp hf') hg.continuousAt), ENat.top_mul]
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ ≠ 0
have pos : g z₀ - g z₀ = 0
Tactic: rw [AnalyticAt.analyticOrderAt_ne_zero (by fun_prop), sub_eq_zero]
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
pos : g z₀ - g z₀ = 0
⊢ analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ ≠ 0
have pos₁ : g z₀ = g z₀
Tactic: rw [AnalyticAt.analyticOrderAt_ne_zero (by fun_prop), sub_eq_zero]
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : ¬analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have hg_nc₁ : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
Tactic: rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc
Cleared hypotheses: hg_nc, hf'
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have neg : ∀ (r : ℕ) (hr : (↑r : ℕ∞) = analyticOrderAt f (g z₀)),
  analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
Tactic: obtain ⟨r, hr⟩ := ENat.ne_top_iff_exists.mp hf'
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : (↑r : ℕ∞) = analyticOrderAt f (g z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have neg : ∀ (s : ℕ) (hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀),
  analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
Tactic: obtain ⟨s, hs⟩ := ENat.ne_top_iff_exists.mp hg_nc
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : (↑r : ℕ∞) = analyticOrderAt f (g z₀)
s : ℕ
hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
have neg : ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
Tactic: rw [← hr, ← hs, ← ENat.coe_mul, (hf.comp hg).analyticOrderAt_eq_natCast]
-- 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : (↑r : ℕ∞) = analyticOrderAt f (g z₀)
s : ℕ
hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
have neg : ∀
  (hr :
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g z₀) ∧ g_1 (g z₀) ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • g_1 z)
  (s : ℕ) (hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀),
  ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
Tactic: rw [Eq.comm, hf.analyticOrderAt_eq_natCast] at hr
Cleared hypotheses: hr, s, hs