awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
inl : ∀ (hlt : min a b < c), ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
⊢ ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
have inr : ∀ (hlt : c < max a b), ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
Tactic: rcases (min_lt_max.2 hne).gt_or_lt c with hlt | hlt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
have inl : [[a, b]] \ {c} ∈ 𝓝[<] c
Tactic: refine ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ [[a, b]] \ {c} ∈ 𝓝[<] c
have inl : [[a, b]] \ {c} ∈ 𝓝[Iic c \ {c}] c
Tactic: rw [← Iic_diff_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
have inr : [[a, b]] \ {c} ∈ 𝓝[>] c
Tactic: refine ⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ [[a, b]] \ {c} ∈ 𝓝[>] c
have inr : [[a, b]] \ {c} ∈ 𝓝[Ici c \ {c}] c
Tactic: rw [← Ici_diff_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
⊢ ¬IntervalIntegrable g volume a b
have obtain : ∀ (l : Filter ℝ) (hl : TendstoIxxClass Icc l l) (hl' : l.NeBot) (hle : l ≤ 𝓝 c) (hmem : [[a, b]] \ {c} ∈ l),
  ¬IntervalIntegrable g volume a b
Tactic: obtain ⟨l, hl, hl', hle, hmem⟩ :
    ∃ l : Filter ℝ, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l := by
    rcases (min_lt_max.2 hne).gt_or_lt c with hlt | hlt
    · refine ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, ?_⟩
      rw [← Iic_diff_right]
      exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsLE_of_mem ⟨hlt, hc.2⟩) _
    · refine ⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, ?_⟩
      rw [← Ici_diff_left]
      exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsGE_of_mem ⟨hc.1, hlt⟩) _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : l.NeBot
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
⊢ ¬IntervalIntegrable g volume a b
have this : l ≤ 𝓝[[[a, b]] \ {c}] c
Tactic: have : l ≤ 𝓝[[[a, b]] \ {c}] c := le_inf hle (le_principal_iff.2 hmem)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
have h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) {c}ᶜ x), HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
Tactic: filter_upwards [self_mem_nhdsWithin] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ¬IntervalIntegrable f volume a b
have A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
Tactic: have A : ∀ᶠ x in 𝓝[≠] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x := by
    filter_upwards [self_mem_nhdsWithin] with x hx
    simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log (x - c)‖) (𝓝[≠] c) atTop
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x - c) (𝓝[≠] c) (𝓝[≠] 0)
Tactic: refine tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsNE_zero.comp ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x - c) (𝓝[≠] c) (𝓝[≠] 0)
have rw : Tendsto (fun (x : ℝ) ↦ x - c) (𝓝[≠] c) (𝓝[≠] (c - c))
Tactic: rw [← sub_self c]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ ¬IntervalIntegrable f volume a b
have B : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log (x - c)‖) (𝓝[≠] c) atTop
Tactic: have B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[≠] c) atTop := by
    refine tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsNE_zero.comp ?_)
    rw [← sub_self c]
    exact ((hasDerivAt_id c).sub_const c).tendsto_nhdsNE one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
a b c : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b ↔ a = b ∨ c ∉ [[a, b]]
have mp : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b → a = b ∨ c ∉ [[a, b]]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
a b c : ℝ
mp : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b → a = b ∨ c ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b ↔ a = b ∨ c ∉ [[a, b]]
have mpr : a = b ∨ c ∉ [[a, b]] → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
a b c : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b → a = b ∨ c ∉ [[a, b]]
have mp : ∀ (h : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b) (hne : ¬a = b) (hc : c ∈ [[a, b]]), False
Tactic: refine fun h => or_iff_not_imp_left.2 fun hne hc => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
a b c : ℝ
h₀ : c ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b
have mpr : ∀ x ∈ [[a, b]], x - c ≠ 0
Tactic: refine ((continuous_sub_right c).continuousOn.inv₀ ?_).intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
a : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) (Ioi 0) x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x) x} x}
    a
Tactic: filter_upwards [Ioi_mem_atTop 0] with x hx using Real.hasDerivAt_log (ne_of_gt hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
Goal:
a : ℝ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Ioi 0) x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x) x} x}
      a
⊢ ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x
have h₁ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) a → HasDerivAt (fun (x : ℝ) ↦ Real.log x) a⁻¹ a
Tactic: filter_upwards [Ioi_mem_atTop 0] with x hx using Real.hasDerivAt_log (ne_of_gt hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
Goal:
a : ℝ
⊢ ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ici a) volume
have A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x
Tactic: have A : ∀ᶠ x in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x := by
    filter_upwards [Ioi_mem_atTop 0] with x hx using Real.hasDerivAt_log (ne_of_gt hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
Goal:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x
⊢ ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ici a) volume
have B : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log x‖) atTop atTop
Tactic: have B : Tendsto (fun x => ‖Real.log x‖) atTop atTop :=
    tendsto_norm_atTop_atTop.comp Real.tendsto_log_atTop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
n : ℕ
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) =
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
have rw : ((ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c) n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) =
  ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
      (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
    x ^ n
Tactic: rw [ordinaryHypergeometricSeries, ofScalars_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
n : ℕ
rw :
  ((ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c) n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) =
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) =
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
have rw₁ : ordinaryHypergeometricCoefficient a b c n • x ^ n =
  ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
      (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
    x ^ n
Tactic: rw [ordinaryHypergeometricSeries, ofScalars_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
⊢ Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸)
    (fun (n : ℕ) ↦ (ordinaryHypergeometricSeries 𝔸 a b c n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
    fun (n : ℕ) ↦
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
have rw : Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸)
  (fun (n : ℕ) ↦
    (ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c) n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
  fun (n : ℕ) ↦
  ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
      (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
    x ^ n
Tactic: rw [ordinaryHypergeometricSeries, ofScalars_apply_eq']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
rw :
  Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸)
    (fun (n : ℕ) ↦
      (ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c) n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
    fun (n : ℕ) ↦
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
⊢ Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸)
    (fun (n : ℕ) ↦ (ordinaryHypergeometricSeries 𝔸 a b c n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
    fun (n : ℕ) ↦
    ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
have rw₁ : Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸) (fun (n : ℕ) ↦ ordinaryHypergeometricCoefficient a b c n • x ^ n) fun (n : ℕ) ↦
  ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
      (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
    x ^ n
Tactic: rw [ordinaryHypergeometricSeries, ofScalars_apply_eq']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ Eq (α := 𝔸) ((ordinaryHypergeometricSeries 𝔸 a b c n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x : Fin n) ↦ 0 : 𝔸)
    (Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n : 𝔸)
have rw : ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
      (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
    HPow.hPow (α := 𝔸) 0 n =
  Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n
Tactic: rw [ordinaryHypergeometricSeries, ofScalars_apply_eq, ordinaryHypergeometricCoefficient]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      HPow.hPow (α := 𝔸) 0 n =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n
have zero : ((↑0! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 0) * Polynomial.eval b (ascPochhammer 𝕂 0) *
      (Polynomial.eval c (ascPochhammer 𝕂 0))⁻¹) •
    HPow.hPow (α := 𝔸) (β := ℕ) 0 0 =
  Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
zero :
  ((↑0! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 0) * Polynomial.eval b (ascPochhammer 𝕂 0) *
        (Polynomial.eval c (ascPochhammer 𝕂 0))⁻¹) •
      HPow.hPow (α := 𝔸) (β := ℕ) 0 0 =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 0
⊢ ((↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      HPow.hPow (α := 𝔸) 0 n =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n
have succ : ∀ (n : ℕ),
  ((↑(n + 1)! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 (n + 1)) * Polynomial.eval b (ascPochhammer 𝕂 (n + 1)) *
        (Polynomial.eval c (ascPochhammer 𝕂 (n + 1)))⁻¹) •
      HPow.hPow (α := 𝔸) 0 (n + 1) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸) (ordinaryHypergeometricSeries 𝔸 a b c : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ordinaryHypergeometricSeries 𝔸 b a c : FormalMultilinearSeries 𝕂 𝔸 𝔸)
have unfold : Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸)
  (ofScalars 𝔸 fun (n : ℕ) ↦
      (↑n ! : 𝕂)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹ :
    FormalMultilinearSeries 𝕂 𝔸 𝔸)
  (ofScalars 𝔸 fun (n : ℕ) ↦
      (↑n ! : 𝕂)⁻¹ * Polynomial.eval b (ascPochhammer 𝕂 n) * Polynomial.eval a (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹ :
    FormalMultilinearSeries 𝕂 𝔸 𝔸)
Tactic: unfold ordinaryHypergeometricSeries ordinaryHypergeometricCoefficient
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
hk : k < n
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0
have inl : ∀ (h : (↑k : 𝕂) = -a),
  HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0
Tactic: rcases habc with h | h | h
Cleared hypotheses: habc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
hk : k < n
inl :
  ∀ (h : (↑k : 𝕂) = -a),
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
      0
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0
have inr : ∀ (h : (↑k : 𝕂) = -b),
  HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0
Tactic: rcases habc with h | h | h
Cleared hypotheses: habc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : (↑k : 𝕂) = -a ∨ (↑k : 𝕂) = -b ∨ (↑k : 𝕂) = -c
hk : k < n
inl :
  ∀ (h : (↑k : 𝕂) = -a),
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
      0
inr :
  ∀ (h : (↑k : 𝕂) = -b),
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
      0
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0
have inr₁ : ∀ (h : (↑k : 𝕂) = -c),
  HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0
Tactic: rcases habc with h | h | h
Cleared hypotheses: habc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : (↑k : 𝕂) = -a
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0
have inl : ∀ (x : (i : Fin n) → 𝔸),
  Eq (α := 𝔸)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) :
          (a : (i : Fin n) → 𝔸) → 𝔸)
        x :
      𝔸)
    ((0 : (a : (i : Fin n) → 𝔸) → 𝔸) x : 𝔸)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : (↑k : 𝕂) = -b
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0
have inr : ∀ (x : (i : Fin n) → 𝔸),
  Eq (α := 𝔸)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) :
          (a : (i : Fin n) → 𝔸) → 𝔸)
        x :
      𝔸)
    ((0 : (a : (i : Fin n) → 𝔸) → 𝔸) x : 𝔸)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : (↑k : 𝕂) = -c
⊢ HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    0
have inr : ∀ (x : (i : Fin n) → 𝔸),
  Eq (α := 𝔸)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (ordinaryHypergeometricCoefficient a b c n)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) :
          (a : (i : Fin n) → 𝔸) → 𝔸)
        x :
      𝔸)
    ((0 : (a : (i : Fin n) → 𝔸) → 𝔸) x : 𝔸)
Tactic: ext