F : Type ?u.292175
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : LinearOrderedSemiring β
inst✝² : FloorSemiring α
inst✝¹ : FloorSemiring β
inst✝ : RingHomClass F α β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊
F : Type ?u.292175
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : LinearOrderedSemiring β
inst✝² : FloorSemiring α
inst✝¹ : FloorSemiring β
inst✝ : RingHomClass F α β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊
have h₀ : 0 ≤ a ↔ 0 ≤ b := by simpa only [cast_zero] using h 0
case inl
F : Type ?u.292175
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : LinearOrderedSemiring β
inst✝² : FloorSemiring α
inst✝¹ : FloorSemiring β
inst✝ : RingHomClass F α β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ ⌊a⌋₊ = ⌊b⌋₊

case inr
F : Type ?u.292175
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : LinearOrderedSemiring β
inst✝² : FloorSemiring α
inst✝¹ : FloorSemiring β
inst✝ : RingHomClass F α β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ = ⌊b⌋₊
F : Type ?u.292175
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : LinearOrderedSemiring β
inst✝² : FloorSemiring α
inst✝¹ : FloorSemiring β
inst✝ : RingHomClass F α β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊
obtain ha | ha := lt_or_le a 0
no goals
case inr
F : Type ?u.292175
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : LinearOrderedSemiring β
inst✝² : FloorSemiring α
inst✝¹ : FloorSemiring β
inst✝ : RingHomClass F α β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ = ⌊b⌋₊
exact (le_floor <| (h _).1 <| floor_le ha).antisymm (le_floor <| (h _).2 <| floor_le <| h₀.1 ha)
no goals
F : Type ?u.292175
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : LinearOrderedSemiring β
inst✝² : FloorSemiring α
inst✝¹ : FloorSemiring β
inst✝ : RingHomClass F α β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
⊢ 0 ≤ a ↔ 0 ≤ b
simpa only [cast_zero] using h 0
no goals
case inl
F : Type ?u.292175
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : LinearOrderedSemiring β
inst✝² : FloorSemiring α
inst✝¹ : FloorSemiring β
inst✝ : RingHomClass F α β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ ⌊a⌋₊ = ⌊b⌋₊
rw [floor_of_nonpos ha.le, floor_of_nonpos (le_of_not_le <| h₀.not.mp ha.not_le)]