Data-carrying pendant to Nontrivial

Stream: Is there code for X?

[Tom Kranz]

Basically what Inhabited is to Nonempty.
This came up here: https://github.com/leanprover-community/mathlib4/pull/15651#discussion_r1729005216
Mathlib.Data.TwoPointing does not look like it ever wanted to be a class. I've implemented the parts mentioned in the PR with TwoPointing as a class and it's really awkward to use:

import Mathlib.Computability.NFA
/-- Two-pointing of a type. This is a Type-valued termed `Nontrivial`. -/
@[ext]
class TwoPointing (α : Type*) extends α × α where
  /-- `fst` and `snd` are distinct terms -/
  fst_ne_snd : fst ≠ snd
  deriving DecidableEq

initialize_simps_projections TwoPointing (+toProd, -fst, -snd)
universe u v w
variable {α : Type u} {σ : Type v} {σ' : Type w} (M : NFA α σ)

open NFA
def char' [TwoPointing σ] (a : α) : NFA α σ :=
  ⟨fun p c q ↦ p = ‹TwoPointing σ›.fst ∧ a = c ∧ q = ‹TwoPointing σ›.snd, (· = ‹TwoPointing σ›.fst), (· = ‹TwoPointing σ›.snd)⟩

@[simp]
theorem char_correct' [TwoPointing σ] (a : α) :
    (char' a : NFA α (σ)).accepts = {[a]} := by
  ext x
  constructor
  · rintro ⟨q, accept, eval⟩
    rcases x.eq_nil_or_concat with rfl | ⟨as, c, rfl⟩
    · cases eval; cases TwoPointing.fst_ne_snd accept
    rw [List.concat_eq_append, eval_append_singleton, mem_stepSet] at eval
    rcases eval with ⟨p, mem, step⟩
    rcases Classical.em (p = ‹TwoPointing σ›.fst) with h | h; rotate_left
    · cases h step.left
    rcases as.eq_nil_or_concat with rfl | ⟨_, _, rfl⟩
    · rcases step with ⟨_, rfl, _⟩; exact rfl
    rw [List.concat_eq_append, eval_append_singleton, mem_stepSet] at mem
    rcases mem with ⟨_, _, _, _, rfl⟩
    cases TwoPointing.fst_ne_snd.symm h
  · rintro rfl
    refine ⟨‹TwoPointing σ›.snd, by simp[char',Set.mem_def], ?_⟩
    rw [← List.nil_append [a], eval_append_singleton, mem_stepSet]
    exact ⟨‹TwoPointing σ›.fst, by repeat fconstructor⟩

[Kevin Buzzard]

Can you really have a class extending something which isn't a class? I'm surprised this doesn't barf! Does it even make sense?

[Matthew Ballard]

Eg: Algebra extends RingHom

[Matthew Ballard]

Although Algebra is the leading contributor to typeclass work

[Kevin Buzzard]

docs#Algebra

[Tom Kranz]

I guess one more reason to think that docs#TwoPointing was never intended to be a class.