Calculational proof with pattern matching

Stream: lean4

[rambip]

I would like to prove that the set of numbers below 2 is in bijection with itself.

My code is pretty complicated, but I did it that way as a smallest reproducible example of a similar problem

In the following, I want to prove that f composed with g reduces to identity.

without changing the definitions of f and g, how can I do it ?

structure Bijection (E: Type u) (F: Type u) where
  f: E -> F
  g: F -> E
  prop: ∀ x: F, f (g x) = x

structure Range (N: Nat) where
  n: Nat
  prop: n < N

example: Bijection (Range 2) (Range 2) :=
  let r₁: Range 2 := Range.mk 0 (Nat.lt.step (Nat.lt.base 0))
  let r₂ : Range 2:= Range.mk 1 (Nat.lt.base 1)

  let f (r: Range 2) := match r.n, r.prop with
    | 0, _ => r₁
    | 1, _ => r₂

  let g (r: Range 2) := match r.n, r.prop with
    | 0, _ => r₂
    | 1, _ => r₂

  have bij (r: Range 2): (f (g r)) = r :=
    match r.n, r.prop with
    |0, _ => rfl -- error
    |1, _ => rfl -- error

  Bijection.mk f g bij

[Reid Barton]

You should match on r, not on its fields.

[Reid Barton]

  have bij (r: Range 2): (f (g r)) = r :=
    match r with
    |⟨0, _⟩ => _
    |⟨1, _⟩ => rfl

[Dan Velleman]

Did you mean for g to map 0 to r₁, not r₂?