-- Mathlib/Algebra/Order/Floor.lean
theorem subsingleton_floorSemiring {α} [LinearOrderedSemiring α] :
    Subsingleton (FloorSemiring α)

Proof state:
case h
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Tactic:
rcases lt_or_le a 0 with h | h

Result:
case h.inl
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : a < 0
⊢ FloorSemiring.floor a = FloorSemiring.floor a

case h.inr
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : 0 ≤ a
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Proof state:
case mk
α : Type u_4
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₂

Tactic:
cases H₂

Result:
case mk.mk
α : Type u_4
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✝ }

Proof state:
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
⊢ FloorSemiring.floor = FloorSemiring.floor

Tactic:
ext a

Result:
case h
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Proof state:
case h.inr
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : 0 ≤ a
n : ℕ
⊢ n ≤ FloorSemiring.floor a ↔ n ≤ FloorSemiring.floor a

Tactic:
rw [H₁.gc_floor, H₂.gc_floor] <;> exact h

Result:
no goals

Proof state:
case h.inr
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : 0 ≤ a
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Tactic:
refine eq_of_forall_le_iff fun n => ?_

Result:
case h.inr
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : 0 ≤ a
n : ℕ
⊢ n ≤ FloorSemiring.floor a ↔ n ≤ FloorSemiring.floor a

Proof state:
case mk.mk
α : Type u_4
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✝ }

Tactic:
congr

Result:
no goals

Proof state:
case h.inl
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
a : α
h : a < 0
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Tactic:
rw [H₁.floor_of_neg, H₂.floor_of_neg] <;> exact h

Result:
no goals

Proof state:
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
⊢ H₁ = H₂

Tactic:
have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil.l_unique H₂.gc_ceil) fun n => rfl

Result:
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this : FloorSemiring.ceil = FloorSemiring.ceil
⊢ H₁ = H₂

Proof state:
α : Type u_4
inst✝ : LinearOrderedSemiring α
⊢ Subsingleton (FloorSemiring α)

Tactic:
refine ⟨fun H₁ H₂ => ?_⟩

Result:
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
⊢ H₁ = H₂

Proof state:
α : Type u_4
inst✝ : LinearOrderedSemiring α
H₁ H₂ : FloorSemiring α
this✝ : FloorSemiring.ceil = FloorSemiring.ceil
this : FloorSemiring.floor = FloorSemiring.floor
⊢ H₁ = H₂

Tactic:
cases H₁

Result:
case mk
α : Type u_4
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₂