feat(data/equiv/encodable): add a few lemmas (#11497)

* add `simp` lemmas `encodable.encode_inj` and
  `encodable.decode₂_encode`;
* add `encodable.decode₂_eq_some`;
* avoid non-final `simp` in the proof of `encodable.Union_decode₂_disjoint_on`.

src/data/equiv/encodable/basic.lean

@@ -50,14 +50,17 @@ universe u
 theorem encode_injective [encodable α] : function.injective (@encode α _)
 | x y e := option.some.inj $ by rw [← encodek, e, encodek]
 
+@[simp] lemma encode_inj [encodable α] {a b : α} : encode a = encode b ↔ a = b :=
+encode_injective.eq_iff
+
 lemma surjective_decode_iget (α : Type*) [encodable α] [inhabited α] :
   surjective (λ n, (encodable.decode α n).iget) :=
 λ x, ⟨encodable.encode x, by simp_rw [encodable.encodek]⟩
 
 /-- An encodable type has decidable equality. Not set as an instance because this is usually not the
 best way to infer decidability. -/
 def decidable_eq_of_encodable (α) [encodable α] : decidable_eq α
-| a b := decidable_of_iff _ encode_injective.eq_iff
+| a b := decidable_of_iff _ encode_inj
 
 /-- If `α` is encodable and there is an injection `f : β → α`, then `β` is encodable as well. -/
 def of_left_injection [encodable α]
@@ -91,7 +94,7 @@ instance empty : encodable empty :=
 ⟨λ a, a.rec _, λ n, none, λ a, a.rec _⟩
 
 instance unit : encodable punit :=
-⟨λ_, zero, λ n, nat.cases_on n (some punit.star) (λ _, none), λ _, by simp⟩
+⟨λ_, 0, λ n, nat.cases_on n (some punit.star) (λ _, none), λ _, by simp⟩
 
 @[simp] theorem encode_star : encode punit.star = 0 := rfl
 
@@ -127,13 +130,22 @@ theorem mem_decode₂ [encodable α] {n : ℕ} {a : α} :
   a ∈ decode₂ α n ↔ encode a = n :=
 mem_decode₂'.trans (and_iff_right_of_imp $ λ e, e ▸ encodek _)
 
+theorem decode₂_eq_some [encodable α] {n : ℕ} {a : α} :
+  decode₂ α n = some a ↔ encode a = n :=
+mem_decode₂
+
+@[simp] lemma decode₂_encode [encodable α] (a : α) :
+  decode₂ α (encode a) = some a :=
+by { ext, simp [mem_decode₂, eq_comm] }
+
 theorem decode₂_ne_none_iff [encodable α] {n : ℕ} :
   decode₂ α n ≠ none ↔ n ∈ set.range (encode : α → ℕ) :=
 by simp_rw [set.range, set.mem_set_of_eq, ne.def, option.eq_none_iff_forall_not_mem,
   encodable.mem_decode₂, not_forall, not_not]
 
 theorem decode₂_is_partial_inv [encodable α] : is_partial_inv encode (decode₂ α) :=
 λ a n, mem_decode₂
+
 theorem decode₂_inj [encodable α] {n : ℕ} {a₁ a₂ : α}
   (h₁ : a₁ ∈ decode₂ α n) (h₂ : a₂ ∈ decode₂ α n) : a₁ = a₂ :=
 encode_injective $ (mem_decode₂.1 h₁).trans (mem_decode₂.1 h₂).symm

src/data/equiv/encodable/lattice.lean

@@ -44,13 +44,10 @@ end
 theorem Union_decode₂_disjoint_on {f : β → set α} (hd : pairwise (disjoint on f)) :
   pairwise (disjoint on λ i, ⋃ b ∈ decode₂ β i, f b) :=
 begin
-  rintro i j ij x ⟨h₁, h₂⟩,
-  revert h₁ h₂,
-  simp, intros b₁ e₁ h₁ b₂ e₂ h₂,
-  refine hd _ _ _ ⟨h₁, h₂⟩,
-  cases encodable.mem_decode₂.1 e₁,
-  cases encodable.mem_decode₂.1 e₂,
-  exact mt (congr_arg _) ij
+  rintro i j ij x,
+  suffices : ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b, by simpa [decode₂_eq_some],
+  rintro a rfl ha b rfl hb,
+  exact hd a b (mt (congr_arg encode) ij) ⟨ha, hb⟩
 end
 
 end encodable