feat(*): add some missing coe_* lemmas (#6697)

* add `submonoid.coe_pow`, `submonoid.coe_list_prod`,
  `submonoid.coe_multiset_prod`, `submonoid.coe_finset_prod`,
  `subring.coe_pow`, `subring.coe_nat_cast`, `subring.coe_int_cast`;
* add `rat.num_div_denom`;
* add `inv_of_pow`.

Author: urkud

src/algebra/group_power/lemmas.lean

@@ -55,6 +55,10 @@ instance invertible_pow (m : M) [invertible m] (n : ℕ) : invertible (m ^ n) :=
   inv_of_mul_self := by rw [← (commute_inv_of m).symm.mul_pow, inv_of_mul_self, one_pow],
   mul_inv_of_self := by rw [← (commute_inv_of m).mul_pow, mul_inv_of_self, one_pow] }
 
+lemma inv_of_pow (m : M) [invertible m] (n : ℕ) [invertible (m ^ n)] :
+  ⅟(m ^ n) = ⅟m ^ n :=
+@invertible_unique M _ (m ^ n) (m ^ n) rfl ‹_› (invertible_pow m n)
+
 lemma is_unit.pow {m : M} (n : ℕ) : is_unit m → is_unit (m ^ n) :=
 λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩
 

src/data/rat/basic.lean

@@ -609,6 +609,9 @@ begin
   simp [division_def, coe_int_eq_mk, mul_def one_ne_zero d0]
 end
 
+theorem num_div_denom (r : ℚ) : (r.num / r.denom : ℚ) = r :=
+by rw [← int.cast_coe_nat, ← mk_eq_div, num_denom]
+
 lemma exists_eq_mul_div_num_and_eq_mul_div_denom {n d : ℤ} (n_ne_zero : n ≠ 0)
   (d_ne_zero : d ≠ 0) :
   ∃ (c : ℤ), n = c * ((n : ℚ) / d).num ∧ (d : ℤ) = c * ((n : ℚ) / d).denom :=

src/group_theory/submonoid/membership.lean

@@ -39,6 +39,21 @@ namespace submonoid
 
 variables (S : submonoid M)
 
+@[simp, norm_cast] theorem coe_pow (x : S) (n : ℕ) : ↑(x ^ n) = (x ^ n : M) :=
+S.subtype.map_pow x n
+
+@[simp, norm_cast] theorem coe_list_prod (l : list S) : (l.prod : M) = (l.map coe).prod :=
+S.subtype.map_list_prod l
+
+@[simp, norm_cast] theorem coe_multiset_prod {M} [comm_monoid M] (S : submonoid M)
+  (m : multiset S) : (m.prod : M) = (m.map coe).prod :=
+S.subtype.map_multiset_prod m
+
+@[simp, norm_cast] theorem coe_finset_prod {ι M} [comm_monoid M] (S : submonoid M)
+  (f : ι → S) (s : finset ι) :
+  ↑(∏ i in s, f i) = (∏ i in s, f i : M) :=
+S.subtype.map_prod f s
+
 /-- Product of a list of elements in a submonoid is in the submonoid. -/
 @[to_additive "Sum of a list of elements in an `add_submonoid` is in the `add_submonoid`."]
 lemma list_prod_mem : ∀ {l : list M}, (∀x ∈ l, x ∈ S) → l.prod ∈ S
@@ -68,9 +83,8 @@ lemma prod_mem {M : Type*} [comm_monoid M] (S : submonoid M)
   ∏ c in t, f c ∈ S :=
 S.multiset_prod_mem (t.1.map f) $ λ x hx, let ⟨i, hi, hix⟩ := multiset.mem_map.1 hx in hix ▸ h i hi
 
-lemma pow_mem {x : M} (hx : x ∈ S) : ∀ n:ℕ, x^n ∈ S
-| 0 := S.one_mem
-| (n+1) := S.mul_mem hx (pow_mem n)
+lemma pow_mem {x : M} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S :=
+by simpa only [coe_pow] using ((⟨x, hx⟩ : S) ^ n).coe_prop
 
 open set
 

src/ring_theory/subring.lean

@@ -233,6 +233,8 @@ instance to_ring : ring s :=
 @[simp, norm_cast] lemma coe_mul (x y : s) : (↑(x * y) : R) = ↑x * ↑y := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : s) : R) = 0 := rfl
 @[simp, norm_cast] lemma coe_one : ((1 : s) : R) = 1 := rfl
+@[simp, norm_cast] lemma coe_pow (x : s) (n : ℕ) : (↑(x ^ n) : R) = x ^ n :=
+s.to_submonoid.coe_pow x n
 
 @[simp] lemma coe_eq_zero_iff {x : s} : (x : R) = 0 ↔ x = 0 :=
 ⟨λ h, subtype.ext (trans h s.coe_zero.symm),
@@ -281,6 +283,10 @@ def subtype (s : subring R) : s →+* R :=
  .. s.to_submonoid.subtype, .. s.to_add_subgroup.subtype }
 
 @[simp] theorem coe_subtype : ⇑s.subtype = coe := rfl
+@[simp, norm_cast] lemma coe_nat_cast (n : ℕ) : ((n : s) : R) = n :=
+s.subtype.map_nat_cast n
+@[simp, norm_cast] lemma coe_int_cast (n : ℤ) : ((n : s) : R) = n :=
+s.subtype.map_int_cast n
 
 /-! # Partial order -/