have := hC σ
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
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