Proving bijections in Lean

Stream: maths

[Anirudh Suresh]

I am trying to do a proof of the following:

import Mathlib

lemma l {y z x : ℕ} (h : z + y ≤ x) :
    2 ^ x= 2 ^ (z + y) * 2 ^ (x - (z + y)) := by
  sorry

theorem pad_cast_bij {y z x : ℕ} (h : z + y ≤ x) :
    Function.Bijective
      (Fin.cast (l h)) := by {

      }

What is the best way to do such proofs? I tried using cast_bijective but that does not work directly. Is there a better tactic or a better approach to do this?

[Aaron Liu]

import Mathlib

lemma l {y z x : ℕ} (h : z + y ≤ x) :
    2 ^ x = 2 ^ (z + y) * 2 ^ (x - (z + y)) := by
  rw [← Nat.pow_add, Nat.add_sub_cancel' h]

theorem pad_cast_bij {y z x : ℕ} (h : z + y ≤ x) :
    Function.Bijective (Fin.cast (l h)) :=
  (finCongr (l h)).bijective

[Terence Tao]

Strangely, one half docs#Fin.cast_injective of the claim is already in Mathlib, but not the other half. Perhaps the following two lemmas are worth adding to Mathlib?

import Mathlib

theorem Fin.cast_surjective {k l:ℕ} (h: k = l) : Function.Surjective (Fin.cast h) :=
  (rightInverse_cast h).surjective -- or `(finCongr h).surjective`

theorem Fin.cast_bijective {k l:ℕ} (h: k = l) : Function.Bijective (Fin.cast h) :=
  ⟨ cast_injective h, cast_surjective h ⟩ -- or `(finCongr h).bijective`