awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
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 : ℂ)
refine_1 : ∀ (g' : ℤ[X]) (hg' : p = q * g'), Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
obtain ⟨g', hg'⟩ := hq
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
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
refine_1₃ refine_1₄ : Eq (α := ℂ) 0 0
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
rw [hg', aeval_mul, hz, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.aeval_mul
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
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 : ℂ)
refine_2 : ∀ (g' : ℤ[X]) (hg' : p.mirror = q * g'), Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)

Tactic:
obtain ⟨g', hg'⟩ := hq'
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
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
refine_2₃ refine_2₄ : Eq (α := ℂ) 0 0
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)

Tactic:
rw [hg', aeval_mul, hz, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.aeval_mul
-- Module: Mathlib.Analysis.Complex.Positivity
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
⊢ ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
have H := taylorSeries_eq_on_ball' hz₂ hf
-- Module: Mathlib.Analysis.Complex.Positivity
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 ≤ z - c

Tactic:
rw [← sub_nonneg] at hz₁

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.Complex.Positivity
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
hz₃ : 0 ≤ z - c
⊢ z ∈ Metric.ball c r

Tactic:
rw [← sub_nonneg] at hz₁

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.Complex.Positivity
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
hz₃ : 0 ≤ z - c
hz₄ : z ∈ Metric.ball c r
⊢ ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
rw [← sub_nonneg] at hz₁

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.Complex.Positivity
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
⊢ z - c = (↑(z - c).re : ℂ)

Tactic:
have hz' := eq_re_of_ofReal_le hz₁
-- Module: Mathlib.Analysis.Complex.Positivity
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 ≤ (↑(z - c).re : ℂ)

Tactic:
rw [hz'] at hz₁ H
-- Module: Mathlib.Analysis.Complex.Positivity
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 : ℂ)
⊢ z ∈ Metric.ball c r

Tactic:
rw [hz'] at hz₁ H
-- Module: Mathlib.Analysis.Complex.Positivity
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
⊢ ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n = f z

Tactic:
rw [hz'] at hz₁ H
-- Module: Mathlib.Analysis.Complex.Positivity
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
H₁ : ∑' (n : ℕ), (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n = f z
⊢ z - c = (↑(z - c).re : ℂ)

Tactic:
rw [hz'] at hz₁ H
-- Module: Mathlib.Analysis.Complex.Positivity
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

Tactic:
H ▸ tsum_nonneg fun n ↦ ?_

Premises used: Eq.rec, tsum_nonneg
-- Module: Mathlib.Analysis.Complex.Positivity
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 : ℂ)
refine : ∀ (n : ℕ), 0 ≤ (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n
⊢ 0 ≤ f z

Tactic:
refine H ▸ tsum_nonneg fun n ↦ ?_
-- Module: Mathlib.Analysis.Complex.Positivity
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 : ℕ
rw : 0 ≤ (↑((↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n) : ℂ)
⊢ 0 ≤ (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n f c * (↑(z - c).re : ℂ) ^ n

Tactic:
rw [← ofReal_natCast, ← ofReal_pow, ← ofReal_inv, eq_re_of_ofReal_le (h n), ← ofReal_mul,
    ← ofReal_mul]

Premises used: Complex.eq_re_of_ofReal_le, Complex.ofReal_natCast, Complex.ofReal_pow, Complex.ofReal_inv, Complex.ofReal_mul
-- Module: Mathlib.Analysis.Complex.Positivity
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 : ℕ
norm_cast : ∀ (hz₁ : 0 ≤ (z - c).re), 0 ≤ (↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n
⊢ 0 ≤ (↑((↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n) : ℂ)

Tactic:
norm_cast at hz₁ ⊢
-- Module: Mathlib.Analysis.Complex.Positivity
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
positivity positivity₁ positivity₂ positivity₃ :
  0 ≤ (iteratedDeriv n f c).re → 0 ≤ (↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n
⊢ 0 ≤ (↑n.factorial : ℝ)⁻¹ * (iteratedDeriv n f c).re * (z - c).re ^ n

Tactic:
positivity [zero_re ▸ (Complex.le_def.mp (h n)).1]
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ 0 ≤ f z

Tactic:
hf.differentiableOn.nonneg_of_iteratedDeriv_nonneg (r := (z - c).re + 1) h hz ?_

Premises used: DifferentiableOn.nonneg_of_iteratedDeriv_nonneg, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
refine : z ∈ Metric.ball c ((z - c).re + 1)
⊢ 0 ≤ f z

Tactic:
refine hf.differentiableOn.nonneg_of_iteratedDeriv_nonneg (r := (z - c).re + 1) h hz ?_

Premises used: DifferentiableOn.nonneg_of_iteratedDeriv_nonneg, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ 0 ≤ z - c

Tactic:
rw [← sub_nonneg] at hz

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
rw : ‖(↑(z - c).re : ℂ)‖ < (↑(z - c).re : ℂ).re + 1
⊢ z ∈ Metric.ball c ((z - c).re + 1)

Tactic:
rw [Metric.mem_ball, dist_eq, eq_re_of_ofReal_le hz]

Premises used: Complex.eq_re_of_ofReal_le, Metric.mem_ball, Complex.dist_eq
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ ‖(↑(z - c).re : ℂ)‖ < (↑(z - c).re : ℂ).re + 1

Tactic:
simpa only [Complex.norm_of_nonneg (nonneg_iff.mp hz).1] using lt_add_one _

Premises used: lt_add_one, Complex.norm_of_nonneg, And.left, Iff.mp, Complex.nonneg_iff
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ LE.le (α := ℂ) 0 (iteratedDeriv 0 (fun (x : ℂ) ↦ f x - f c) c)

Tactic:
simp only [iteratedDeriv_zero, sub_self, le_refl]

Premises used: iteratedDeriv_zero, le_refl, sub_self
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
n : ℕ
⊢ 0 ≤ iteratedDeriv (n + 1) f c

Tactic:
specialize h (n + 1) n.succ_ne_zero

Premises used: Nat.succ_ne_zero, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
z : ℂ
hz : c ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv (n + 1) f c
succ : ∀ (h : 0 ≤ iteratedDeriv n (deriv f) c), LE.le (α := ℂ) 0 (iteratedDeriv n (deriv fun (x : ℂ) ↦ f x - f c) c)
⊢ LE.le (α := ℂ) 0 (iteratedDeriv (n + 1) (fun (x : ℂ) ↦ f x - f c) c)

Tactic:
rw [iteratedDeriv_succ'] at h ⊢

Premises used: iteratedDeriv_succ'
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
z : ℂ
hz : c ≤ z
n : ℕ
h succ succ₁ succ₂ succ₃ : 0 ≤ iteratedDeriv n (deriv f) c
⊢ LE.le (α := ℂ) 0 (iteratedDeriv n (deriv fun (x : ℂ) ↦ f x - f c) c)

Tactic:
rwa [funext fun x ↦ deriv_sub_const (f := f) (x := x) (f c)]

Premises used: funext, deriv_sub_const
-- Module: Mathlib.Analysis.Complex.Positivity
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)
succ : ∀ (n : ℕ), LE.le (α := ℂ) 0 (iteratedDeriv (n + 1) (fun (x : ℂ) ↦ f x - f c) c)
⊢ LE.le (α := ℂ) 0 (iteratedDeriv n (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)]

Premises used: iteratedDeriv_zero, le_refl, sub_self, iteratedDeriv_succ', funext, deriv_sub_const, Nat.succ_ne_zero, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Positivity
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)

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)]
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
h' : ∀ (n : ℕ), LE.le (α := ℂ) 0 (iteratedDeriv n (fun (x : ℂ) ↦ f x - f c) c)
⊢ f c ≤ f z

Tactic:
sub_nonneg.mp <| nonneg_of_iteratedDeriv_nonneg (hf.sub_const _) h' hz

Premises used: Differentiable.nonneg_of_iteratedDeriv_nonneg, Iff.mp, Differentiable.sub_const, sub_nonneg
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
h' : ∀ (n : ℕ), LE.le (α := ℂ) 0 (iteratedDeriv n (fun (x : ℂ) ↦ f x - f c) c)
⊢ f c ≤ f z

Tactic:
exact sub_nonneg.mp <| nonneg_of_iteratedDeriv_nonneg (hf.sub_const _) h' hz

Premises used: Differentiable.nonneg_of_iteratedDeriv_nonneg, Iff.mp, Differentiable.sub_const, sub_nonneg
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ LE.le (α := ℂ) ((fun (z : ℂ) ↦ f (-z)) (-c)) ((fun (z : ℂ) ↦ f (-z)) (-z))

Tactic:
apply_le_of_iteratedDeriv_nonneg (f := fun z ↦ f (-z)) (hf.comp <| differentiable_neg)
      (fun n hn ↦ ?_) (neg_le_neg_iff.mpr hz)

Premises used: Iff.mpr, differentiable_neg, Differentiable.apply_le_of_iteratedDeriv_nonneg, Differentiable.comp, neg_le_neg_iff
-- Module: Mathlib.Analysis.Complex.Positivity
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)
apply_le_of_iteratedDeriv_nonneg :
  ∀ (n : ℕ) (hn : n ≠ 0), LE.le (α := ℂ) 0 (iteratedDeriv n (fun (z : ℂ) ↦ f (-z)) (-c))
⊢ f c ≤ 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

Premises used: Iff.mpr, differentiable_neg, Differentiable.apply_le_of_iteratedDeriv_nonneg, Differentiable.comp, neg_le_neg_iff
-- Module: Mathlib.Analysis.Complex.Positivity
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 (- -c)

Tactic:
simp only [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f z = f (- -z)

Tactic:
simp only [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.Analysis.Complex.Positivity
Goal:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
n : ℕ
hn : n ≠ 0
⊢ LE.le (α := ℂ) 0 (iteratedDeriv n (fun (z : ℂ) ↦ f (-z)) (-c))

Tactic:
simpa only [iteratedDeriv_comp_neg, neg_neg, smul_eq_mul] using h n hn

Premises used: neg_neg, iteratedDeriv_comp_neg, smul_eq_mul
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
⊢ IsHomeomorphicTrivialFiberBundle ℝ re

Tactic:
⟨equivRealProdCLM.toHomeomorph, fun _ => rfl⟩

Premises used: Complex.equivRealProdCLM, IsHomeomorphicTrivialFiberBundle, Exists.intro, ContinuousLinearEquiv.toHomeomorph, rfl
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
⊢ IsHomeomorphicTrivialFiberBundle ℝ im

Tactic:
⟨equivRealProdCLM.toHomeomorph.trans (Homeomorph.prodComm ℝ ℝ), fun _ => rfl⟩

Premises used: Real, Homeomorph.prodComm, Complex.equivRealProdCLM, IsHomeomorphicTrivialFiberBundle, Exists.intro, Homeomorph.trans, ContinuousLinearEquiv.toHomeomorph, rfl
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
⊢ IsOpenMap re

Tactic:
isHomeomorphicTrivialFiberBundle_re.isOpenMap_proj

Premises used: Complex.isHomeomorphicTrivialFiberBundle_re, IsHomeomorphicTrivialFiberBundle.isOpenMap_proj
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
⊢ IsOpenMap im

Tactic:
isHomeomorphicTrivialFiberBundle_im.isOpenMap_proj

Premises used: IsHomeomorphicTrivialFiberBundle.isOpenMap_proj, Complex.isHomeomorphicTrivialFiberBundle_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
⊢ IsQuotientMap re

Tactic:
isHomeomorphicTrivialFiberBundle_re.isQuotientMap_proj

Premises used: Complex.isHomeomorphicTrivialFiberBundle_re, IsHomeomorphicTrivialFiberBundle.isQuotientMap_proj
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
⊢ IsQuotientMap im

Tactic:
isHomeomorphicTrivialFiberBundle_im.isQuotientMap_proj

Premises used: IsHomeomorphicTrivialFiberBundle.isQuotientMap_proj, Complex.isHomeomorphicTrivialFiberBundle_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s : Set ℝ
⊢ interior (re ⁻¹' s) = re ⁻¹' interior s

Tactic:
(isOpenMap_re.preimage_interior_eq_interior_preimage continuous_re _).symm

Premises used: Complex.continuous_re, IsOpenMap.preimage_interior_eq_interior_preimage, Eq.symm, Complex.isOpenMap_re
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s : Set ℝ
⊢ interior (im ⁻¹' s) = im ⁻¹' interior s

Tactic:
(isOpenMap_im.preimage_interior_eq_interior_preimage continuous_im _).symm

Premises used: Complex.isOpenMap_im, IsOpenMap.preimage_interior_eq_interior_preimage, Eq.symm, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s : Set ℝ
⊢ closure (re ⁻¹' s) = re ⁻¹' closure s

Tactic:
(isOpenMap_re.preimage_closure_eq_closure_preimage continuous_re _).symm

Premises used: IsOpenMap.preimage_closure_eq_closure_preimage, Complex.continuous_re, Eq.symm, Complex.isOpenMap_re
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s : Set ℝ
⊢ closure (im ⁻¹' s) = im ⁻¹' closure s

Tactic:
(isOpenMap_im.preimage_closure_eq_closure_preimage continuous_im _).symm

Premises used: Complex.isOpenMap_im, IsOpenMap.preimage_closure_eq_closure_preimage, Eq.symm, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s : Set ℝ
⊢ frontier (re ⁻¹' s) = re ⁻¹' frontier s

Tactic:
(isOpenMap_re.preimage_frontier_eq_frontier_preimage continuous_re _).symm

Premises used: Complex.continuous_re, Eq.symm, Complex.isOpenMap_re, IsOpenMap.preimage_frontier_eq_frontier_preimage
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s : Set ℝ
⊢ frontier (im ⁻¹' s) = im ⁻¹' frontier s

Tactic:
(isOpenMap_im.preimage_frontier_eq_frontier_preimage continuous_im _).symm

Premises used: Complex.isOpenMap_im, Eq.symm, IsOpenMap.preimage_frontier_eq_frontier_preimage, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (interior {z : ℂ | z.re ≤ a}) {z : ℂ | z.re < a}

Tactic:
simpa only [interior_Iic] using interior_preimage_re (Iic a)

Premises used: Complex.interior_preimage_re, Set.Iic, interior_Iic
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (interior {z : ℂ | z.im ≤ a}) {z : ℂ | z.im < a}

Tactic:
simpa only [interior_Iic] using interior_preimage_im (Iic a)

Premises used: Complex.interior_preimage_im, Set.Iic, interior_Iic
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (interior {z : ℂ | a ≤ z.re}) {z : ℂ | a < z.re}

Tactic:
simpa only [interior_Ici] using interior_preimage_re (Ici a)

Premises used: interior_Ici, Set.Ici, Complex.interior_preimage_re
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (interior {z : ℂ | a ≤ z.im}) {z : ℂ | a < z.im}

Tactic:
simpa only [interior_Ici] using interior_preimage_im (Ici a)

Premises used: interior_Ici, Set.Ici, Complex.interior_preimage_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (closure {z : ℂ | z.re < a}) {z : ℂ | z.re ≤ a}

Tactic:
simpa only [closure_Iio] using closure_preimage_re (Iio a)

Premises used: Complex.closure_preimage_re, closure_Iio, Set.Iio
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (closure {z : ℂ | z.im < a}) {z : ℂ | z.im ≤ a}

Tactic:
simpa only [closure_Iio] using closure_preimage_im (Iio a)

Premises used: Complex.closure_preimage_im, closure_Iio, Set.Iio
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (closure {z : ℂ | a < z.re}) {z : ℂ | a ≤ z.re}

Tactic:
simpa only [closure_Ioi] using closure_preimage_re (Ioi a)

Premises used: Set.Ioi, Complex.closure_preimage_re, closure_Ioi
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (closure {z : ℂ | a < z.im}) {z : ℂ | a ≤ z.im}

Tactic:
simpa only [closure_Ioi] using closure_preimage_im (Ioi a)

Premises used: Set.Ioi, Complex.closure_preimage_im, closure_Ioi
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | z.re ≤ a}) {z : ℂ | z.re = a}

Tactic:
simpa only [frontier_Iic] using frontier_preimage_re (Iic a)

Premises used: Complex.frontier_preimage_re, frontier_Iic, Set.Iic
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | z.im ≤ a}) {z : ℂ | z.im = a}

Tactic:
simpa only [frontier_Iic] using frontier_preimage_im (Iic a)

Premises used: Complex.frontier_preimage_im, frontier_Iic, Set.Iic
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | a ≤ z.re}) {z : ℂ | z.re = a}

Tactic:
simpa only [frontier_Ici] using frontier_preimage_re (Ici a)

Premises used: Set.Ici, Complex.frontier_preimage_re, frontier_Ici
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | a ≤ z.im}) {z : ℂ | z.im = a}

Tactic:
simpa only [frontier_Ici] using frontier_preimage_im (Ici a)

Premises used: Set.Ici, frontier_Ici, Complex.frontier_preimage_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | z.re < a}) {z : ℂ | z.re = a}

Tactic:
simpa only [frontier_Iio] using frontier_preimage_re (Iio a)

Premises used: Complex.frontier_preimage_re, frontier_Iio, Set.Iio
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | z.im < a}) {z : ℂ | z.im = a}

Tactic:
simpa only [frontier_Iio] using frontier_preimage_im (Iio a)

Premises used: Complex.frontier_preimage_im, frontier_Iio, Set.Iio
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | a < z.re}) {z : ℂ | z.re = a}

Tactic:
simpa only [frontier_Ioi] using frontier_preimage_re (Ioi a)

Premises used: Set.Ioi, Complex.frontier_preimage_re, frontier_Ioi