F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
⊢ H₁ = H₂
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
⊢ Subsingleton (FloorRing α)
refine' ⟨fun H₁ H₂ => _⟩
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
this : FloorRing.floor = FloorRing.floor
⊢ H₁ = H₂
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
⊢ H₁ = H₂
have : H₁.floor = H₂.floor :=
  funext fun a => (H₁.gc_coe_floor.u_unique H₂.gc_coe_floor) fun _ => rfl
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ H₁ = H₂
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
this : FloorRing.floor = FloorRing.floor
⊢ H₁ = H₂
have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil_coe.l_unique H₂.gc_ceil_coe) fun _ => rfl
case mk
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
H₂ : FloorRing α
floor✝ ceil✝ : α → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ } = H₂
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ H₁ = H₂
cases H₁
case mk.mk
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
floor✝¹ ceil✝¹ : α → ℤ
gc_coe_floor✝¹ : GaloisConnection Int.cast floor✝¹
gc_ceil_coe✝¹ : GaloisConnection ceil✝¹ Int.cast
floor✝ ceil✝ : α → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝¹, ceil := ceil✝¹, gc_coe_floor := gc_coe_floor✝¹, gc_ceil_coe := gc_ceil_coe✝¹ } =
    { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ }
case mk
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
H₂ : FloorRing α
floor✝ ceil✝ : α → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ } = H₂
cases H₂
no goals
case mk.mk
F : Type ?u.312400
α✝ : Type ?u.312403
β : Type ?u.312406
α : Type u_1
inst✝ : LinearOrderedRing α
floor✝¹ ceil✝¹ : α → ℤ
gc_coe_floor✝¹ : GaloisConnection Int.cast floor✝¹
gc_ceil_coe✝¹ : GaloisConnection ceil✝¹ Int.cast
floor✝ ceil✝ : α → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝¹, ceil := ceil✝¹, gc_coe_floor := gc_coe_floor✝¹, gc_ceil_coe := gc_ceil_coe✝¹ } =
    { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ }
congr