F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
⊢ H₁ = H₂
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
⊢ Subsingleton (FloorSemiring α)
refine' ⟨fun H₁ H₂ => _⟩
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
⊢ H₁ = H₂
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
⊢ H₁ = H₂
have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil.l_unique H₂.gc_ceil) fun n => rfl
case mk
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₂ : FloorSemiring α
floor✝ ceil✝ : α → ℕ
floor_of_neg✝ : ∀ {a : α}, a < 0 → floor✝ a = 0
gc_floor✝ : ∀ {a : α} {n : ℕ}, 0 ≤ a → (n ≤ floor✝ a ↔ ↑n ≤ a)
gc_ceil✝ : GaloisConnection ceil✝ Nat.cast
this✝ : FloorSemiring.ceil = FloorSemiring.ceil
this : FloorSemiring.floor = FloorSemiring.floor
⊢ { floor := floor✝, ceil := ceil✝, floor_of_neg := floor_of_neg✝, gc_floor := gc_floor✝, gc_ceil := gc_ceil✝ } = H₂
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this✝ : FloorSemiring.ceil = FloorSemiring.ceil
this : FloorSemiring.floor = FloorSemiring.floor
⊢ H₁ = H₂
cases H₁
case mk.mk
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
floor✝¹ ceil✝¹ : α → ℕ
floor_of_neg✝¹ : ∀ {a : α}, a < 0 → floor✝¹ a = 0
gc_floor✝¹ : ∀ {a : α} {n : ℕ}, 0 ≤ a → (n ≤ floor✝¹ a ↔ ↑n ≤ a)
gc_ceil✝¹ : GaloisConnection ceil✝¹ Nat.cast
floor✝ ceil✝ : α → ℕ
floor_of_neg✝ : ∀ {a : α}, a < 0 → floor✝ a = 0
gc_floor✝ : ∀ {a : α} {n : ℕ}, 0 ≤ a → (n ≤ floor✝ a ↔ ↑n ≤ a)
gc_ceil✝ : GaloisConnection ceil✝ Nat.cast
this✝ : FloorSemiring.ceil = FloorSemiring.ceil
this : FloorSemiring.floor = FloorSemiring.floor
⊢ { floor := floor✝¹, ceil := ceil✝¹, floor_of_neg := floor_of_neg✝¹, gc_floor := gc_floor✝¹, gc_ceil := gc_ceil✝¹ } =
    { floor := floor✝, ceil := ceil✝, floor_of_neg := floor_of_neg✝, gc_floor := gc_floor✝, gc_ceil := gc_ceil✝ }
case mk
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₂ : FloorSemiring α
floor✝ ceil✝ : α → ℕ
floor_of_neg✝ : ∀ {a : α}, a < 0 → floor✝ a = 0
gc_floor✝ : ∀ {a : α} {n : ℕ}, 0 ≤ a → (n ≤ floor✝ a ↔ ↑n ≤ a)
gc_ceil✝ : GaloisConnection ceil✝ Nat.cast
this✝ : FloorSemiring.ceil = FloorSemiring.ceil
this : FloorSemiring.floor = FloorSemiring.floor
⊢ { floor := floor✝, ceil := ceil✝, floor_of_neg := floor_of_neg✝, gc_floor := gc_floor✝, gc_ceil := gc_ceil✝ } = H₂
cases H₂
no goals
case mk.mk
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
floor✝¹ ceil✝¹ : α → ℕ
floor_of_neg✝¹ : ∀ {a : α}, a < 0 → floor✝¹ a = 0
gc_floor✝¹ : ∀ {a : α} {n : ℕ}, 0 ≤ a → (n ≤ floor✝¹ a ↔ ↑n ≤ a)
gc_ceil✝¹ : GaloisConnection ceil✝¹ Nat.cast
floor✝ ceil✝ : α → ℕ
floor_of_neg✝ : ∀ {a : α}, a < 0 → floor✝ a = 0
gc_floor✝ : ∀ {a : α} {n : ℕ}, 0 ≤ a → (n ≤ floor✝ a ↔ ↑n ≤ a)
gc_ceil✝ : GaloisConnection ceil✝ Nat.cast
this✝ : FloorSemiring.ceil = FloorSemiring.ceil
this : FloorSemiring.floor = FloorSemiring.floor
⊢ { floor := floor✝¹, ceil := ceil✝¹, floor_of_neg := floor_of_neg✝¹, gc_floor := gc_floor✝¹, gc_ceil := gc_ceil✝¹ } =
    { floor := floor✝, ceil := ceil✝, floor_of_neg := floor_of_neg✝, gc_floor := gc_floor✝, gc_ceil := gc_ceil✝ }
congr
case h
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
⊢ FloorSemiring.floor a = FloorSemiring.floor a
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
⊢ FloorSemiring.floor = FloorSemiring.floor
ext a
case h.inl
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : a < 0
⊢ FloorSemiring.floor a = FloorSemiring.floor a

case h.inr
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : 0 ≤ a
⊢ FloorSemiring.floor a = FloorSemiring.floor a
case h
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
⊢ FloorSemiring.floor a = FloorSemiring.floor a
cases' lt_or_le a 0 with h h
no goals
case h.inl
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : a < 0
⊢ FloorSemiring.floor a = FloorSemiring.floor a
rw [H₁.floor_of_neg, H₂.floor_of_neg] <;> exact h
case h.inr
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : 0 ≤ a
n : ℕ
⊢ n ≤ FloorSemiring.floor a ↔ n ≤ FloorSemiring.floor a
case h.inr
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : 0 ≤ a
⊢ FloorSemiring.floor a = FloorSemiring.floor a
refine' eq_of_forall_le_iff fun n => _
no goals
case h.inr
F : Type ?u.99218
α✝ : Type ?u.99221
β : Type ?u.99224
α : Type u_1
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : 0 ≤ a
n : ℕ
⊢ n ≤ FloorSemiring.floor a ↔ n ≤ FloorSemiring.floor a
rw [H₁.gc_floor, H₂.gc_floor] <;> exact h