-- Mathlib/NumberTheory/LSeries/Positivity.lean
/-- If all values of `a : ℕ → ℂ` are nonnegative reals and `a 1`
is positive, and the L-series of `a` agrees with an entire function `f` on some open
right half-plane where it converges, then `f` is real and positive on `ℝ`. -/
lemma positive_of_differentiable_of_eqOn {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {f : ℂ → ℂ}
    (hf : Differentiable ℂ f) {x : ℝ} (hx : abscissaOfAbsConv a ≤ x)
    (hf' : {s | x < s.re}.EqOn f (LSeries a)) (y : ℝ) :
    0 < f y

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
⊢ 0 < f (↑(x ⊔ y) + 1)

Tactic:
simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'

Result:
no goals

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
⊢ ↑(x ⊔ y) + 1 ∈ {s | x < s.re}

Tactic:
simp only [Set.mem_setOf_eq, add_re, ofReal_re, one_re, hxy]

Result:
no goals

Proof state:
case refine_2
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(x ⊔ y) + 1)
⊢ ↑y ≤ ↑(x ⊔ y) + 1

Tactic:
exact_mod_cast (le_max_right x y).trans (lt_add_one _).le

Result:
no goals

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
⊢ 0 < f ↑y

Tactic:
have hfx : 0 < f (max x y + 1) := by
  simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'

Result:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(x ⊔ y) + 1)
⊢ 0 < f ↑y

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
⊢ 0 < f ↑y

Tactic:
have hys : (max x y + 1 : ℂ) ∈ {s | x < s.re} := by
  simp only [Set.mem_setOf_eq, add_re, ofReal_re, one_re, hxy]

Result:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
⊢ 0 < f ↑y

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
⊢ 0 < f ↑y

Tactic:
have hxy' : abscissaOfAbsConv a < max x y + 1 := hx.trans_lt <| mod_cast hxy

Result:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
⊢ 0 < f ↑y

Proof state:
case refine_1
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(x ⊔ y) + 1)
n : ℕ
x✝ : n ≠ 0
hs : IsOpen {s | x < s.re}
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n f (↑(x ⊔ y) + 1)

Tactic:
simpa only [hf'.iteratedDeriv_of_isOpen hs n hys, ofReal_add, ofReal_one] using
  iteratedDeriv_alternating ha₀ hxy' n

Result:
no goals

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
⊢ 0 < f ↑y

Tactic:
have hxy : x < max x y + 1 := (le_max_left x y).trans_lt (lt_add_one _)

Result:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
⊢ 0 < f ↑y

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(x ⊔ y) + 1)
⊢ 0 < f ↑y

Tactic:
refine (hfx.trans_le <| hf.apply_le_of_iteratedDeriv_alternating (fun n _ ↦ ?_) ?_)

Result:
case refine_1
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(x ⊔ y) + 1)
n : ℕ
x✝ : n ≠ 0
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n f (↑(x ⊔ y) + 1)

case refine_2
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(x ⊔ y) + 1)
⊢ ↑y ≤ ↑(x ⊔ y) + 1

Proof state:
case refine_1
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(x ⊔ y) + 1)
n : ℕ
x✝ : n ≠ 0
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n f (↑(x ⊔ y) + 1)

Tactic:
have hs : IsOpen {s : ℂ | x < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi

Result:
case refine_1
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < x ⊔ y + 1
hxy' : abscissaOfAbsConv a < ↑(x ⊔ y) + 1
hys : ↑(x ⊔ y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(x ⊔ y) + 1)
n : ℕ
x✝ : n ≠ 0
hs : IsOpen {s | x < s.re}
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n f (↑(x ⊔ y) + 1)