Theorem: ZetaNear1BndExact (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
have := ZetaNear1BndFilter
State after:
this : (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
this : (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
rw [Asymptotics.isBigO_iff] at this
State after:
this : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 1, ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
this : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 1, ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
obtain ⟨c, U, hU, V, hV, h⟩ := this
State after:
case intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
obtain ⟨T, hT, T_open, h1T⟩ := mem_nhds_iff.mp hU
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
obtain ⟨ε, εpos, hε⟩ := Metric.isOpen_iff.mp T_open 1 h1T
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Metric.ball 1 ε ⊆ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Metric.ball 1 ε ⊆ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
simp only [Metric.ball] at hε
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
replace hε : Ico 1 (1 + ε) ⊆ U := by
  refine subset_trans (subset_trans ?_ hε) hT
  intro x hx
  simp only [mem_Ico] at hx
  simp only [dist, abs_lt]
  exact ⟨by linarith, by linarith⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
let W := Icc (1 + ε) 2
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
have W_compact : IsCompact {ofReal' z | z ∈ W} :=
  IsCompact.image isCompact_Icc continuous_ofReal
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
have cont : ContinuousOn ζ {ofReal' z | z ∈ W} := by
  apply HasDerivAt.continuousOn (f' := deriv ζ)
  intro σ hσ
  exact (differentiableAt_riemannZeta (by contrapose! hσ; simp [W, hσ, εpos])).hasDerivAt
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
obtain ⟨C, hC⟩ := IsCompact.exists_bound_of_continuousOn W_compact cont
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
let C' := max (C + 1) 1
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
replace hC : ∀ (σ : ℝ), σ ∈ W → ‖ζ σ‖ < C' := by
  intro σ hσ
  simp only [lt_max_iff, C']
  have := hC σ
  simp only [mem_setOf_eq, ofReal_inj, exists_eq_right] at this
  exact Or.inl <| lt_of_le_of_lt (this hσ) (by norm_num)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
have Cpos : 0 < C' := by simp [C']
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
use max (2 * C') c, (by simp [Cpos])
State after:
case h
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
⊢ ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)

State before:
case h
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
⊢ ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
intro σ ⟨σ_ge, σ_le⟩
State after:
case h
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)

State before:
case h
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
by_cases hσ : σ ∈ U ∩ V
State after:
case pos
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ U ∩ V
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)

case neg
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∉ U ∩ V
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
⊢ Ico 1 (1 + ε) ⊆ U
Tactic:
refine subset_trans (subset_trans ?_ hε) hT
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
⊢ Ico 1 (1 + ε) ⊆ {y | dist y 1 < ε}

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
⊢ Ico 1 (1 + ε) ⊆ {y | dist y 1 < ε}
Tactic:
intro x hx
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
x : ℝ
hx : x ∈ Ico 1 (1 + ε)
⊢ x ∈ {y | dist y 1 < ε}

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
x : ℝ
hx : x ∈ Ico 1 (1 + ε)
⊢ x ∈ {y | dist y 1 < ε}
Tactic:
simp only [mem_Ico] at hx
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x ∈ {y | dist y 1 < ε}

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x ∈ {y | dist y 1 < ε}
Tactic:
simp only [dist, abs_lt]
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x ∈ {y | -ε < y - 1 ∧ y - 1 < ε}

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x ∈ {y | -ε < y - 1 ∧ y - 1 < ε}
Tactic:
exact ⟨by linarith, by linarith⟩
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ -ε < x - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x - 1 < ε
Tactic:
linarith
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
⊢ ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
Tactic:
apply HasDerivAt.continuousOn (f' := deriv ζ)
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
⊢ ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, HasDerivAt ζ (deriv ζ x) x

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
⊢ ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, HasDerivAt ζ (deriv ζ x) x
Tactic:
intro σ hσ
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
σ : ℂ
hσ : σ ∈ {x | ∃ z ∈ W, ↑z = x}
⊢ HasDerivAt ζ (deriv ζ σ) σ

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
σ : ℂ
hσ : σ ∈ {x | ∃ z ∈ W, ↑z = x}
⊢ HasDerivAt ζ (deriv ζ σ) σ
Tactic:
exact (differentiableAt_riemannZeta (by contrapose! hσ; simp [W, hσ, εpos])).hasDerivAt
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
σ : ℂ
hσ : σ ∈ {x | ∃ z ∈ W, ↑z = x}
⊢ σ ≠ 1
Tactic:
contrapose! hσ
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
σ : ℂ
hσ : σ = 1
⊢ σ ∉ {x | ∃ z ∈ W, ↑z = x}

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
σ : ℂ
hσ : σ = 1
⊢ σ ∉ {x | ∃ z ∈ W, ↑z = x}
Tactic:
simp [W, hσ, εpos]
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
⊢ ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Tactic:
intro σ hσ
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
σ : ℝ
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ < C'

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
σ : ℝ
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ < C'
Tactic:
simp only [lt_max_iff, C']
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
σ : ℝ
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
σ : ℝ
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1
Tactic:
have := hC σ
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
σ : ℝ
hσ : σ ∈ W
this : ↑σ ∈ {x | ∃ z ∈ W, ↑z = x} → ‖ζ ↑σ‖ ≤ C
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
σ : ℝ
hσ : σ ∈ W
this : ↑σ ∈ {x | ∃ z ∈ W, ↑z = x} → ‖ζ ↑σ‖ ≤ C
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1
Tactic:
simp only [mem_setOf_eq, ofReal_inj, exists_eq_right] at this
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
σ : ℝ
hσ : σ ∈ W
this : σ ∈ W → ‖ζ ↑σ‖ ≤ C
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
σ : ℝ
hσ : σ ∈ W
this : σ ∈ W → ‖ζ ↑σ‖ ≤ C
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1
Tactic:
exact Or.inl <| lt_of_le_of_lt (this hσ) (by norm_num)
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
σ : ℝ
hσ : σ ∈ W
this : σ ∈ W → ‖ζ ↑σ‖ ≤ C
⊢ C < C + 1
Tactic:
norm_num
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
⊢ 0 < C'
Tactic:
simp [C']
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
⊢ 0 < max (2 * C') c
Tactic:
simp [Cpos]
State after:
no goals

State before:
case pos
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ U ∩ V
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
simp only [← h, mem_setOf_eq] at hσ
State after:
case pos
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)

State before:
case pos
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
apply le_trans hσ ?_
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ c * ‖1 / (↑σ - 1)‖ ≤ max (2 * C') c / (σ - 1)

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ c * ‖1 / (↑σ - 1)‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
norm_cast
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ c * ‖↑(1 / (σ - 1))‖ ≤ max (2 * C') c / (σ - 1)

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ c * ‖↑(1 / (σ - 1))‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
have : 0 ≤ 1 / (σ - 1) := by apply one_div_nonneg.mpr; linarith
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c * ‖↑(1 / (σ - 1))‖ ≤ max (2 * C') c / (σ - 1)

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c * ‖↑(1 / (σ - 1))‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
simp only [norm_eq_abs, Complex.abs_ofReal, abs_eq_self.mpr this, mul_div, mul_one]
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c / (σ - 1) ≤ max (2 * C') c / (σ - 1)

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c / (σ - 1) ≤ max (2 * C') c / (σ - 1)
Tactic:
exact div_le_div (by simp [Cpos.le]) (by simp) (by linarith) (by rfl)
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ 0 ≤ 1 / (σ - 1)
Tactic:
apply one_div_nonneg.mpr
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ 0 ≤ σ - 1

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ 0 ≤ σ - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ 0 ≤ max (2 * C') c
Tactic:
simp [Cpos.le]
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c ≤ max (2 * C') c
Tactic:
simp
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ 0 < σ - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ σ - 1 ≤ σ - 1
Tactic:
rfl
State after:
no goals

State before:
case neg
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∉ U ∩ V
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
replace hσ : σ ∈ W := by
  simp only [mem_inter_iff, hV σ_ge, and_true] at hσ
  simp only [mem_Icc, σ_le, and_true, W]
  contrapose! hσ; exact hε ⟨σ_ge.le, hσ⟩
State after:
case neg
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)

State before:
case neg
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
apply le_trans (hC σ hσ).le ((le_div_iff (by linarith)).mpr ?_)
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ C' * (σ - 1) ≤ max (2 * C') c

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ C' * (σ - 1) ≤ max (2 * C') c
Tactic:
rw [le_max_iff, mul_comm 2]
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ C' * (σ - 1) ≤ C' * 2 ∨ C' * (σ - 1) ≤ c

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ C' * (σ - 1) ≤ C' * 2 ∨ C' * (σ - 1) ≤ c
Tactic:
exact Or.inl <| mul_le_mul_of_nonneg_left (by linarith) Cpos.le
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∉ U ∩ V
⊢ σ ∈ W
Tactic:
simp only [mem_inter_iff, hV σ_ge, and_true] at hσ
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∉ U
⊢ σ ∈ W

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∉ U
⊢ σ ∈ W
Tactic:
simp only [mem_Icc, σ_le, and_true, W]
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∉ U
⊢ 1 + ε ≤ σ

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∉ U
⊢ 1 + ε ≤ σ
Tactic:
contrapose! hσ
State after:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ < 1 + ε
⊢ σ ∈ U

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ < 1 + ε
⊢ σ ∈ U
Tactic:
exact hε ⟨σ_ge.le, hσ⟩
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ 0 < σ - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ σ - 1 ≤ 2
Tactic:
linarith
State after:
no goals