α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this : (a : Prop) → Decidable a
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
haveI := Classical.propDecidable
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this : (a : Prop) → Decidable a
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
have : ∃ ub : ℤ, (ub : α) ≤ x ∧ ∀ z : ℤ, (z : α) ≤ x → z ≤ ub :=
  Int.exists_greatest_of_bdd
    (let ⟨n, hn⟩ := exists_int_gt x
    ⟨n, fun z h' => Int.cast_le.1 <| le_trans h' <| le_of_lt hn⟩)
    (let ⟨n, hn⟩ := exists_int_lt x
    ⟨n, le_of_lt hn⟩)
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl : ℤ
h : ↑fl ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
z : ℤ
⊢ z ≤ fl ↔ ↑z ≤ x
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
refine' this.imp fun fl h z => _
case intro
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl z : ℤ
h₁ : ↑fl ≤ x
h₂ : ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
⊢ z ≤ fl ↔ ↑z ≤ x
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl : ℤ
h : ↑fl ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
z : ℤ
⊢ z ≤ fl ↔ ↑z ≤ x
cases' h with h₁ h₂
no goals
case intro
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl z : ℤ
h₁ : ↑fl ≤ x
h₂ : ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
⊢ z ≤ fl ↔ ↑z ≤ x
exact ⟨fun h => le_trans (Int.cast_le.2 h) h₁, h₂ z⟩