awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
g' : ℤ[X]
hg' : p = q * g'
refine_1 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * g') : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
have refine_1₁ : HMul.hMul (α := ℂ) (β := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
Tactic: rw [hg', aeval_mul, hz, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
g' : ℤ[X]
hg' : p = q * g'
refine_1 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * g') : ℂ) (0 : ℂ)
refine_1₁ : HMul.hMul (α := ℂ) (β := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
have refine_1₂ : HMul.hMul (α := ℂ) (β := ℂ) (0 : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
Tactic: rw [hg', aeval_mul, hz, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
g' : ℤ[X]
hg' : p = q * g'
refine_1 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * g') : ℂ) (0 : ℂ)
refine_1₁ : HMul.hMul (α := ℂ) (β := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
refine_1₂ : HMul.hMul (α := ℂ) (β := ℂ) (0 : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
have refine_1₃ : Eq (α := ℂ) 0 0
Tactic: rw [hg', aeval_mul, hz, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)
have refine_2 : ∀ (g' : ℤ[X]) (hg' : p.mirror = q * g'), Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)
Tactic: obtain ⟨g', hg'⟩ := hq'
Cleared hypotheses: hq'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
g' : ℤ[X]
hg' : p.mirror = q * g'
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)
have refine_2 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * g') : ℂ) (0 : ℂ)
Tactic: rw [hg', aeval_mul, hz, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
g' : ℤ[X]
hg' : p.mirror = q * g'
refine_2 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * g') : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)
have refine_2₁ : HMul.hMul (α := ℂ) (β := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
Tactic: rw [hg', aeval_mul, hz, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
g' : ℤ[X]
hg' : p.mirror = q * g'
refine_2 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * g') : ℂ) (0 : ℂ)
refine_2₁ : HMul.hMul (α := ℂ) (β := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)
have refine_2₂ : HMul.hMul (α := ℂ) (β := ℂ) (0 : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
Tactic: rw [hg', aeval_mul, hz, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
g' : ℤ[X]
hg' : p.mirror = q * g'
refine_2 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * g') : ℂ) (0 : ℂ)
refine_2₁ : HMul.hMul (α := ℂ) (β := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
refine_2₂ : HMul.hMul (α := ℂ) (β := ℂ) (0 : ℂ) ((aeval z : (a : ℤ[X]) → ℂ) g' : ℂ) = 0
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)
have refine_2₃ : Eq (α := ℂ) 0 0
Tactic: rw [hg', aeval_mul, hz, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (hypothesis)
Goal:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : c ≤ z
hz₂ : z ∈ Metric.ball c r
⊢ 0 ≤ f z
have H : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
Tactic: have H := taylorSeries_eq_on_ball' hz₂ hf
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (hypothesis)
Goal:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : c ≤ z
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
⊢ 0 ≤ f z
have hz₃ : 0 ≤ z - c
Tactic: rw [← sub_nonneg] at hz₁
Cleared hypotheses: hz₁, hz₂, H
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (hypothesis)
Goal:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ z - c
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
⊢ 0 ≤ f z
have hz' : z - c = (↑(z - c).re : ℂ)
Tactic: have hz' := eq_re_of_ofReal_le hz₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (hypothesis)
Goal:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ z - c
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
hz' : z - c = (↑(z - c).re : ℂ)
⊢ 0 ≤ f z
have hz₃ : 0 ≤ (↑(z - c).re : ℂ)
Tactic: rw [hz'] at hz₁ H
Cleared hypotheses: hz₁, hz₂, H, hz'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (hypothesis)
Goal:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ z - c
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
hz' : z - c = (↑(z - c).re : ℂ)
hz₃ : 0 ≤ (↑(z - c).re : ℂ)
hz₄ : z ∈ Metric.ball c r
⊢ 0 ≤ f z
have H₁ : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n = f z
Tactic: rw [hz'] at hz₁ H
Cleared hypotheses: hz₁, hz₂, H, hz'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ (↑(z - c).re : ℂ)
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n = f z
hz' : z - c = (↑(z - c).re : ℂ)
⊢ 0 ≤ f z
have refine : ∀ (n : ℕ), 0 ≤ (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n
Tactic: refine H ▸ tsum_nonneg fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ (↑(z - c).re : ℂ)
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n = f z
hz' : z - c = (↑(z - c).re : ℂ)
n : ℕ
⊢ 0 ≤ (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n
have rw : 0 ≤ (↑((↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n) : ℂ)
Tactic: rw [← ofReal_natCast, ← ofReal_pow, ← ofReal_inv, eq_re_of_ofReal_le (h n), ← ofReal_mul,
    ← ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ (↑(z - c).re : ℂ)
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n = f z
hz' : z - c = (↑(z - c).re : ℂ)
n : ℕ
⊢ 0 ≤ (↑((↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n) : ℂ)
have norm_cast : ∀ (hz₁ : 0 ≤ (z - c).re), 0 ≤ (↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n
Tactic: norm_cast at hz₁ ⊢
Cleared hypotheses: hz₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n = f z
hz' : z - c = (↑(z - c).re : ℂ)
n : ℕ
hz₁ : 0 ≤ (z - c).re
⊢ 0 ≤ (↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n
have positivity : 0 ≤ (iteratedDeriv n f c).re → 0 ≤ (↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n
Tactic: positivity [zero_re ▸ (Complex.le_def.mp (h n)).1]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ 0 ≤ f z
have refine : z ∈ Metric.ball c ((z - c).re + 1)
Tactic: refine hf.differentiableOn.nonneg_of_iteratedDeriv_nonneg (r := (z - c).re + 1) h hz ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (hypothesis)
Goal:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ z ∈ Metric.ball c ((z - c).re + 1)
have hz₁ : 0 ≤ z - c
Tactic: rw [← sub_nonneg] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ z ∈ Metric.ball c ((z - c).re + 1)
have rw : ‖(↑(z - c).re : ℂ)‖ < (↑(z - c).re : ℂ).re + 1
Tactic: rw [Metric.mem_ball, dist_eq, eq_re_of_ofReal_le hz]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (hypothesis)
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
n : ℕ
⊢ LE.le (α := ℂ) 0 (iteratedDeriv (n + 1) (fun (x : ℂ) ↦ f x - f c) c)
have h₁ : 0 ≤ iteratedDeriv (n + 1) f c
Tactic: specialize h (n + 1) n.succ_ne_zero
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
z : ℂ
hz : c ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv (n + 1) f c
⊢ LE.le (α := ℂ) 0 (iteratedDeriv (n + 1) (fun (x : ℂ) ↦ f x - f c) c)
have succ : ∀ (h : 0 ≤ iteratedDeriv n (deriv f) c), LE.le (α := ℂ) 0 (iteratedDeriv n (deriv fun (x : ℂ) ↦ f x - f c) c)
Tactic: rw [iteratedDeriv_succ'] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
n : ℕ
⊢ LE.le (α := ℂ) 0 (iteratedDeriv n (fun (x : ℂ) ↦ f x - f c) c)
have zero : LE.le (α := ℂ) 0 (iteratedDeriv 0 (fun (x : ℂ) ↦ f x - f c) c)
Tactic: cases n with
    | zero => simp only [iteratedDeriv_zero, sub_self, le_refl]
    | succ n =>
      specialize h (n + 1) n.succ_ne_zero
      rw [iteratedDeriv_succ'] at h ⊢
      rwa [funext fun x ↦ deriv_sub_const (f := f) (x := x) (f c)]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
n : ℕ
zero : LE.le (α := ℂ) 0 (iteratedDeriv 0 (fun (x : ℂ) ↦ f x - f c) c)
⊢ LE.le (α := ℂ) 0 (iteratedDeriv n (fun (x : ℂ) ↦ f x - f c) c)
have succ : ∀ (n : ℕ), LE.le (α := ℂ) 0 (iteratedDeriv (n + 1) (fun (x : ℂ) ↦ f x - f c) c)
Tactic: cases n with
    | zero => simp only [iteratedDeriv_zero, sub_self, le_refl]
    | succ n =>
      specialize h (n + 1) n.succ_ne_zero
      rw [iteratedDeriv_succ'] at h ⊢
      rwa [funext fun x ↦ deriv_sub_const (f := f) (x := x) (f c)]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (hypothesis)
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ f c ≤ f z
have h' : ∀ (n : ℕ), LE.le (α := ℂ) 0 (iteratedDeriv n (fun (x : ℂ) ↦ f x - f c) c)
Tactic: have h' (n : ℕ) : 0 ≤ iteratedDeriv n (f · - f c) c := by
    cases n with
    | zero => simp only [iteratedDeriv_zero, sub_self, le_refl]
    | succ n =>
      specialize h (n + 1) n.succ_ne_zero
      rw [iteratedDeriv_succ'] at h ⊢
      rwa [funext fun x ↦ deriv_sub_const (f := f) (x := x) (f c)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f c ≤ f z
have h₁ : f c = f (- -c)
Tactic: convert!
    apply_le_of_iteratedDeriv_nonneg (f := fun z ↦ f (-z)) (hf.comp <| differentiable_neg)
      (fun n hn ↦ ?_) (neg_le_neg_iff.mpr hz) using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
h₁ : f c = f (- -c)
⊢ f c ≤ f z
have h₂ : f z = f (- -z)
Tactic: convert!
    apply_le_of_iteratedDeriv_nonneg (f := fun z ↦ f (-z)) (hf.comp <| differentiable_neg)
      (fun n hn ↦ ?_) (neg_le_neg_iff.mpr hz) using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Positivity (goal)
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
h₁ : f c = f (- -c)
h₂ : f z = f (- -z)
⊢ f c ≤ f z
have apply_le_of_iteratedDeriv_nonneg : ∀ (n : ℕ) (hn : n ≠ 0), LE.le (α := ℂ) 0 (iteratedDeriv n (fun (z : ℂ) ↦ f (-z)) (-c))
Tactic: convert!
    apply_le_of_iteratedDeriv_nonneg (f := fun z ↦ f (-z)) (hf.comp <| differentiable_neg)
      (fun n hn ↦ ?_) (neg_le_neg_iff.mpr hz) using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.ReImTopology (goal)
Goal:
s t : Set ℝ
⊢ interior (s ×ℂ t) = interior s ×ℂ interior t
have rw : interior (re ⁻¹' s ∩ im ⁻¹' t) = interior s ×ℂ interior t
Tactic: rw [reProdIm, reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ReImTopology (goal)
Goal:
s t : Set ℝ
rw : interior (re ⁻¹' s ∩ im ⁻¹' t) = interior s ×ℂ interior t
⊢ interior (s ×ℂ t) = interior s ×ℂ interior t
have rw₁ : interior (re ⁻¹' s ∩ im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
Tactic: rw [reProdIm, reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ReImTopology (goal)
Goal:
s t : Set ℝ
rw : interior (re ⁻¹' s ∩ im ⁻¹' t) = interior s ×ℂ interior t
rw₁ : interior (re ⁻¹' s ∩ im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
⊢ interior (s ×ℂ t) = interior s ×ℂ interior t
have rw₂ : interior (re ⁻¹' s) ∩ interior (im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
Tactic: rw [reProdIm, reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ReImTopology (goal)
Goal:
s t : Set ℝ
rw : interior (re ⁻¹' s ∩ im ⁻¹' t) = interior s ×ℂ interior t
rw₁ : interior (re ⁻¹' s ∩ im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
rw₂ : interior (re ⁻¹' s) ∩ interior (im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
⊢ interior (s ×ℂ t) = interior s ×ℂ interior t
have rw₃ : re ⁻¹' interior s ∩ interior (im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
Tactic: rw [reProdIm, reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ReImTopology (goal)
Goal:
s t : Set ℝ
rw : interior (re ⁻¹' s ∩ im ⁻¹' t) = interior s ×ℂ interior t
rw₁ : interior (re ⁻¹' s ∩ im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
rw₂ : interior (re ⁻¹' s) ∩ interior (im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
rw₃ : re ⁻¹' interior s ∩ interior (im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
⊢ interior (s ×ℂ t) = interior s ×ℂ interior t
have rw₄ : re ⁻¹' interior s ∩ im ⁻¹' interior t = re ⁻¹' interior s ∩ im ⁻¹' interior t
Tactic: rw [reProdIm, reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RealDeriv (hypothesis)
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' (↑z : ℂ)
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) e'.re z
have A : HasStrictFDerivAt ofReal ofRealCLM z
Tactic: have A : HasStrictFDerivAt ((↑) : ℝ → ℂ) ofRealCLM z := ofRealCLM.hasStrictFDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.RealDeriv (hypothesis)
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' (↑z : ℂ)
A : HasStrictFDerivAt ofReal ofRealCLM z
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) e'.re z
have B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
  ((ofRealCLM : (a : ℝ) → ℂ) z)
Tactic: have B :
    HasStrictFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ)
      (ofRealCLM z) :=
    h.hasStrictFDerivAt.restrictScalars ℝ
-- Lean 4 proof step from Mathlib.Analysis.Complex.RealDeriv (hypothesis)
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' (↑z : ℂ)
A : HasStrictFDerivAt ofReal ofRealCLM z
B :
  HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
    ((ofRealCLM : (a : ℝ) → ℂ) z)
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) e'.re z
have C : HasStrictFDerivAt re reCLM (e ((ofRealCLM : (a : ℝ) → ℂ) z))
Tactic: have C : HasStrictFDerivAt re reCLM (e (ofRealCLM z)) := reCLM.hasStrictFDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.RealDeriv (hypothesis)
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' (↑z : ℂ)
⊢ HasDerivAt (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) e'.re z
have A : HasFDerivAt ofReal ofRealCLM z
Tactic: have A : HasFDerivAt ((↑) : ℝ → ℂ) ofRealCLM z := ofRealCLM.hasFDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.RealDeriv (hypothesis)
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' (↑z : ℂ)
A : HasFDerivAt ofReal ofRealCLM z
⊢ HasDerivAt (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) e'.re z
have B : HasFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
  ((ofRealCLM : (a : ℝ) → ℂ) z)
Tactic: have B :
    HasFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ)
      (ofRealCLM z) :=
    h.hasFDerivAt.restrictScalars ℝ
-- Lean 4 proof step from Mathlib.Analysis.Complex.RealDeriv (hypothesis)
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' (↑z : ℂ)
A : HasFDerivAt ofReal ofRealCLM z
B :
  HasFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
    ((ofRealCLM : (a : ℝ) → ℂ) z)
⊢ HasDerivAt (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) e'.re z
have C : HasFDerivAt re reCLM (e ((ofRealCLM : (a : ℝ) → ℂ) z))
Tactic: have C : HasFDerivAt re reCLM (e (ofRealCLM z)) := reCLM.hasFDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.RealDeriv (hypothesis)
Goal:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e (↑z : ℂ)
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) z
have A : ContDiffAt ℝ n ofReal z
Tactic: have A : ContDiffAt ℝ n ((↑) : ℝ → ℂ) z := ofRealCLM.contDiff.contDiffAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.RealDeriv (hypothesis)
Goal:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e (↑z : ℂ)
A : ContDiffAt ℝ n ofReal z
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) z
have B : ContDiffAt ℝ n e (↑z : ℂ)
Tactic: have B : ContDiffAt ℝ n e z := h.restrict_scalars ℝ
-- Lean 4 proof step from Mathlib.Analysis.Complex.RealDeriv (hypothesis)
Goal:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e (↑z : ℂ)
A : ContDiffAt ℝ n ofReal z
B : ContDiffAt ℝ n e (↑z : ℂ)
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) z
have C : ContDiffAt ℝ n re (e (↑z : ℂ))
Tactic: have C : ContDiffAt ℝ n re (e z) := reCLM.contDiff.contDiffAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
⊢ AnalyticAt ℂ f c
have rcases : ∀ (R : ℝ) (hR0 : 0 < R) (hRs : closedBall c R ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}),
  AnalyticAt ℂ f c
Tactic: rcases (nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1 hd with ⟨R, hR0, hRs⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ
hR0 : 0 < R
hRs : closedBall c R ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
⊢ AnalyticAt ℂ f c
have lift : ∀ (R : ℝ≥0) (hR0 : 0 < (↑R : ℝ))
  (hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}), AnalyticAt ℂ f c
Tactic: lift R to ℝ≥0 using hR0.le
Cleared hypotheses: R, hR0, hRs
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
⊢ ContinuousOn f (closedBall c (↑R : ℝ))
have refine : ∀ (z : ℂ) (hz : z ∈ closedBall c (↑R : ℝ)), ContinuousAt f z
Tactic: refine fun z hz => ContinuousAt.continuousWithinAt ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
z : ℂ
hz : z ∈ closedBall c (↑R : ℝ)
⊢ ContinuousAt f z
have inl : ∀ (hd : ∀ᶠ (z : ℂ) in 𝓝[≠] z, DifferentiableAt ℂ f z) (hc : ContinuousAt f z)
  (hRs : closedBall z (↑R : ℝ) ∩ {z}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x})
  (hz : z ∈ closedBall z (↑R : ℝ)), ContinuousAt f z
Tactic: rcases eq_or_ne z c with (rfl | hne)
Cleared hypotheses: c, hd, hc, hRs, hz