feat(logic/basic, logic/function/basic): make cast the simp-normal form of eq.mp and eq.mpr, add lemmas (#6834)

This adds the fact that `eq.rec`, `eq.mp`, `eq.mpr`, and `cast` are bijective, as well as some simp lemmas that follow from their injectivity.

Author: eric-wieser

src/data/fin.lean

@@ -1282,15 +1282,15 @@ begin
       { have : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y, by simp,
         convert this,
         { exact h'.symm },
-        { exact heq_of_eq_mp (congr_arg α (eq.symm h')) rfl } },
+        { exact heq_of_cast_eq (congr_arg α (eq.symm h')) rfl } },
       have C2 : α i.cast_succ = α (cast_succ (cast_lt j h)),
         by rw [cast_succ_cast_lt, h'],
       have E2 : update p i y (cast_lt j h) = _root_.cast C2 y,
       { have : update p (cast_lt j h) (_root_.cast C2 y) (cast_lt j h) = _root_.cast C2 y,
           by simp,
         convert this,
         { simp [h, h'] },
-        { exact heq_of_eq_mp C2 rfl } },
+        { exact heq_of_cast_eq C2 rfl } },
       rw [E1, E2],
       exact eq_rec_compose _ _ _ },
     { have : ¬(cast_lt j h = i),

src/data/padics/ring_homs.lean

@@ -267,7 +267,7 @@ begin
   dsimp [to_zmod, to_zmod_hom],
   unfreezingI { rcases (exists_eq_add_of_lt (hp_prime.1.pos)) with ⟨p', rfl⟩ },
   change ↑(zmod.val _) = _,
-  simp only [zmod.val_nat_cast, add_zero, add_def, cast_inj, zero_add],
+  simp only [zmod.val_nat_cast, add_zero, add_def, nat.cast_inj, zero_add],
   apply mod_eq_of_lt,
   simpa only [zero_add] using zmod_repr_lt_p z,
 end

src/data/real/irrational.lean

@@ -105,7 +105,7 @@ then iff_of_false (not_not_intro ⟨rat.sqrt q,
          sqrt_eq, abs_of_nonneg (rat.sqrt_nonneg q)]⟩) (λ h, h.1 H1)
 else if H2 : 0 ≤ q
 then iff_of_true (λ ⟨r, hr⟩, H1 $ (exists_mul_self _).1 ⟨r,
-  by rwa [eq_comm, sqrt_eq_iff_mul_self_eq (cast_nonneg.2 H2), ← cast_mul, cast_inj] at hr;
+  by rwa [eq_comm, sqrt_eq_iff_mul_self_eq (cast_nonneg.2 H2), ← cast_mul, rat.cast_inj] at hr;
   rw [← hr]; exact real.sqrt_nonneg _⟩) ⟨H1, H2⟩
 else iff_of_false (not_not_intro ⟨0,
   by rw cast_zero; exact (sqrt_eq_zero_of_nonpos (rat.cast_nonpos.2 $ le_of_not_le H2)).symm⟩)

src/logic/basic.lean

@@ -30,7 +30,7 @@ attribute [inline] and.decidable or.decidable decidable.false xor.decidable iff.
   decidable.true implies.decidable not.decidable ne.decidable
   bool.decidable_eq decidable.to_bool
 
-attribute [simp] cast_eq
+attribute [simp] cast_eq cast_heq
 
 variables {α : Type*} {β : Type*}
 
@@ -655,10 +655,15 @@ lemma eq_rec_constant {α : Sort*} {a a' : α} {β : Sort*} (y : β) (h : a = a'
 by { cases h, refl, }
 
 @[simp]
-lemma eq_mp_rfl {α : Sort*} {a : α} : eq.mp (eq.refl α) a = a := rfl
+lemma eq_mp_eq_cast {α β : Sort*} (h : α = β) : eq.mp h = cast h := rfl
 
 @[simp]
-lemma eq_mpr_rfl {α : Sort*} {a : α} : eq.mpr (eq.refl α) a = a := rfl
+lemma eq_mpr_eq_cast {α β : Sort*} (h : α = β) : eq.mpr h = cast h.symm := rfl
+
+@[simp]
+lemma cast_cast : ∀ {α β γ : Sort*} (ha : α = β) (hb : β = γ) (a : α),
+  cast hb (cast ha a) = cast (ha.trans hb) a
+| _ _ _ rfl rfl a := rfl
 
 @[simp] lemma congr_refl_left {α β : Sort*} (f : α → β) {a b : α} (h : a = b) :
   congr (eq.refl f) h = congr_arg f h :=
@@ -680,17 +685,14 @@ rfl
   congr_fun (congr_arg f p) b = congr_arg (λ a, f a b) p :=
 rfl
 
-lemma heq_of_eq_mp :
-  ∀ {α β : Sort*} {a : α} {a' : β} (e : α = β) (h₂ : (eq.mp e a) = a'), a == a'
+lemma heq_of_cast_eq :
+  ∀ {α β : Sort*} {a : α} {a' : β} (e : α = β) (h₂ : cast e a = a'), a == a'
 | α ._ a a' rfl h := eq.rec_on h (heq.refl _)
 
 lemma rec_heq_of_heq {β} {C : α → Sort*} {x : C a} {y : β} (eq : a = b) (h : x == y) :
   @eq.rec α a C x b eq == y :=
 by subst eq; exact h
 
-@[simp] lemma {u} eq_mpr_heq {α β : Sort u} (h : β = α) (x : α) : eq.mpr h x == x :=
-by subst h; refl
-
 protected lemma eq.congr {x₁ x₂ y₁ y₂ : α} (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) :
   (x₁ = x₂) ↔ (y₁ = y₂) :=
 by { subst h₁, subst h₂ }

src/logic/function/basic.lean

@@ -610,6 +610,33 @@ def set.piecewise {α : Type u} {β : α → Sort v} (s : set α) (f g : Πi, β
   Πi, β i :=
 λi, if i ∈ s then f i else g i
 
+/-! ### Bijectivity of `eq.rec`, `eq.mp`, `eq.mpr`, and `cast` -/
+
+lemma eq_rec_on_bijective {α : Sort*} {C : α → Sort*} :
+  ∀ {a a' : α} (h : a = a'), function.bijective (@eq.rec_on _ _ C _ h)
+| _ _ rfl := ⟨λ x y, id, λ x, ⟨x, rfl⟩⟩
+
+lemma eq_mp_bijective {α β : Sort*} (h : α = β) : function.bijective (eq.mp h) :=
+eq_rec_on_bijective h
+
+lemma eq_mpr_bijective {α β : Sort*} (h : α = β) : function.bijective (eq.mpr h) :=
+eq_rec_on_bijective h.symm
+
+lemma cast_bijective {α β : Sort*} (h : α = β) : function.bijective (cast h) :=
+eq_rec_on_bijective h
+
+/-! Note these lemmas apply to `Type*` not `Sort*`, as the latter interferes with `simp`, and
+is trivial anyway.-/
+
+@[simp]
+lemma eq_rec_inj {α : Sort*} {a a' : α} (h : a = a') {C : α → Type*} (x y : C a) :
+  (eq.rec x h : C a') = eq.rec y h ↔ x = y :=
+(eq_rec_on_bijective h).injective.eq_iff
+
+@[simp]
+lemma cast_inj {α β : Type*} (h : α = β) {x y : α} : cast h x = cast h y ↔ x = y :=
+(cast_bijective h).injective.eq_iff
+
 /-- A set of functions "separates points"
 if for each pair of distinct points there is a function taking different values on them. -/
 def separates_points {α β : Type*} (A : set (α → β)) : Prop :=

src/tactic/interactive.lean

@@ -595,7 +595,7 @@ do let (e,n) := arg,
         tactic.clear h' ),
    when h.is_some (do
      (to_expr ``(heq_of_eq_rec_left %%eq_h %%asm)
-       <|> to_expr ``(heq_of_eq_mp %%eq_h %%asm))
+       <|> to_expr ``(heq_of_cast_eq %%eq_h %%asm))
      >>= note h' none >> pure ()),
    tactic.clear asm,
    when rev.is_some (interactive.revert [n])

src/tactic/transport.lean

@@ -27,7 +27,8 @@ It's probably best not to adjust it without understanding the algorithm used by
 
 attribute [transport_simps]
   eq_rec_constant
-  eq_mpr_rfl
+  eq_mp_eq_cast
+  cast_eq
   equiv.to_fun_as_coe
   equiv.arrow_congr'_apply
   equiv.symm_apply_apply

test/equiv_rw.lean

@@ -287,7 +287,7 @@ mk_simp_attribute transport_simps "simps useful inside `transport`"
 
 attribute [transport_simps]
   eq_rec_constant
-  eq_mpr_rfl
+  cast_eq
   equiv.to_fun_as_coe
   equiv.arrow_congr'_apply
   equiv.symm_apply_apply