Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg (EulerProducts/Auxiliary.lean)

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Tactic:
let D : ℕ → ℝ := fun n ↦ (iteratedDeriv n f 0).re
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Tactic:
have hD (n : ℕ) : iteratedDeriv n f 0 = D n := by
  refine Complex.ext rfl ?_
  simp only [ofReal_im]
  exact (le_def.mp (h n)).2.symm
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Tactic:
obtain ⟨F, hFd, hF⟩ := realValued_of_iteratedDeriv_real hf hD
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Tactic:
rw [hF]
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
⊢ MonotoneOn (ofReal' ∘ F) (Set.Ici 0)

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
⊢ MonotoneOn (ofReal' ∘ F) (Set.Ici 0)
Tactic:
refine monotone_ofReal.comp_monotoneOn <| monotoneOn_of_deriv_nonneg (convex_Ici 0)
  hFd.continuous.continuousOn hFd.differentiableOn fun x hx ↦ ?_
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
⊢ 0 ≤ deriv F x

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
⊢ 0 ≤ deriv F x
Tactic:
have hD' (n : ℕ) : 0 ≤ iteratedDeriv n (deriv f) 0 := by
  rw [← iteratedDeriv_succ']
  exact h (n + 1)
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
⊢ 0 ≤ deriv F x

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
⊢ 0 ≤ deriv F x
Tactic:
have hf' := (contDiff_succ_iff_deriv.mp <| hf.contDiff (n := 2)).2.differentiable rfl.le
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ deriv F x

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ deriv F x
Tactic:
have hx : (0 : ℂ) ≤ x := by
  norm_cast
  simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx
  exact hx.le
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
⊢ 0 ≤ deriv F x

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
⊢ 0 ≤ deriv F x
Tactic:
have H := nonneg_of_iteratedDeriv_nonneg hf' hD' hx
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv f ↑x
⊢ 0 ≤ deriv F x

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv f ↑x
⊢ 0 ≤ deriv F x
Tactic:
rw [← deriv.comp_ofReal hf.differentiableAt] at H
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv (fun x => f ↑x) x
⊢ 0 ≤ deriv F x

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv (fun x => f ↑x) x
⊢ 0 ≤ deriv F x
Tactic:
change 0 ≤ deriv (f ∘ ofReal') x at H
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv (f ∘ ofReal') x
⊢ 0 ≤ deriv F x

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv (f ∘ ofReal') x
⊢ 0 ≤ deriv F x
Tactic:
erw [hF, deriv.ofReal_comp] at H
State after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ ↑(deriv (fun y => F y) x)
⊢ 0 ≤ deriv F x

State before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ ↑(deriv (fun y => F y) x)
⊢ 0 ≤ deriv F x
Tactic:
norm_cast at H
State after:
no goals

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ iteratedDeriv n f 0 = ↑(D n)
Tactic:
refine Complex.ext rfl ?_
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ (iteratedDeriv n f 0).im = (↑(D n)).im

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ (iteratedDeriv n f 0).im = (↑(D n)).im
Tactic:
simp only [ofReal_im]
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ (iteratedDeriv n f 0).im = 0

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ (iteratedDeriv n f 0).im = 0
Tactic:
exact (le_def.mp (h n)).2.symm
State after:
no goals

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
n : ℕ
⊢ 0 ≤ iteratedDeriv n (deriv f) 0
Tactic:
rw [← iteratedDeriv_succ']
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
n : ℕ
⊢ 0 ≤ iteratedDeriv (n + 1) f 0

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
n : ℕ
⊢ 0 ≤ iteratedDeriv (n + 1) f 0
Tactic:
exact h (n + 1)
State after:
no goals

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ ↑x
Tactic:
norm_cast
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ x

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ x
Tactic:
simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 < x
⊢ 0 ≤ x

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 < x
⊢ 0 ≤ x
Tactic:
exact hx.le
State after:
no goals