use max (2 * C') c, (by simp [Cpos])
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)
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)