feat(data/rat/cast): generalize ext lemmas (#16268)

* generalize `monoid_with_zero_hom.ext_rat` to `monoid_with_zero`;
* deduce `ext` lemma for `ring_hom`s from `monoid_with_zero_hom` version;
* use hom classes.

Author: urkud

src/data/rat/cast.lean

@@ -300,53 +300,41 @@ by rw [cast_def, map_div₀, map_int_cast, map_nat_cast, cast_def]
 @[simp] lemma eq_rat_cast {k} [division_ring k] [ring_hom_class F ℚ k] (f : F) (r : ℚ) : f r = r :=
 by rw [← map_rat_cast f, rat.cast_id]
 
-lemma ring_hom.ext_rat {R : Type*} [semiring R] (f g : ℚ →+* R) : f = g :=
-begin
-  ext r,
-  refine rat.num_denom_cases_on' r _,
-  intros a b b0,
-  let φ : ℤ →+* R := f.comp (int.cast_ring_hom ℚ),
-  let ψ : ℤ →+* R := g.comp (int.cast_ring_hom ℚ),
-  rw [rat.mk_eq_div, int.cast_coe_nat],
-  have b0' : (b:ℚ) ≠ 0 := nat.cast_ne_zero.2 b0,
-  have : ∀ n : ℤ, f n = g n := λ n, show φ n = ψ n, by rw [φ.ext_int ψ],
-  calc f (a * b⁻¹)
-      = f a * f b⁻¹ * (g (b:ℤ) * g b⁻¹) :
-        by rw [int.cast_coe_nat, ← g.map_mul, mul_inv_cancel b0', g.map_one, mul_one, f.map_mul]
-  ... = g a * f b⁻¹ * (f (b:ℤ) * g b⁻¹) : by rw [this a, ← this b]
-  ... = g (a * b⁻¹) :
-        by rw [int.cast_coe_nat, mul_assoc, ← mul_assoc (f b⁻¹),
-              ← f.map_mul, inv_mul_cancel b0', f.map_one, one_mul, g.map_mul]
-end
-
-instance rat.subsingleton_ring_hom {R : Type*} [semiring R] : subsingleton (ℚ →+* R) :=
-⟨ring_hom.ext_rat⟩
-
 namespace monoid_with_zero_hom
 
-variables {M : Type*} [group_with_zero M]
+variables {M₀ : Type*} [monoid_with_zero M₀] [monoid_with_zero_hom_class F ℚ M₀] {f g : F}
+include M₀
+
+/-- If `f` and `g` agree on the integers then they are equal `φ`. -/
+theorem ext_rat' (h : ∀ m : ℤ, f m = g m) : f = g :=
+fun_like.ext f g $ λ r, by rw [← r.num_div_denom, div_eq_mul_inv, map_mul, map_mul, h,
+  ← int.cast_coe_nat, eq_on_inv₀ f g (h _)]
 
 /-- If `f` and `g` agree on the integers then they are equal `φ`.
 
 See note [partially-applied ext lemmas] for why `comp` is used here. -/
-@[ext]
-theorem ext_rat {f g : ℚ →*₀ M}
-  (same_on_int : f.comp (int.cast_ring_hom ℚ).to_monoid_with_zero_hom =
-    g.comp (int.cast_ring_hom ℚ).to_monoid_with_zero_hom) : f = g :=
-begin
-  have same_on_int' : ∀ k : ℤ, f k = g k := congr_fun same_on_int,
-  ext x,
-  rw [← @rat.num_denom x, rat.mk_eq_div, map_div₀ f, map_div₀ g,
-    same_on_int' x.num, same_on_int' x.denom],
-end
+@[ext] theorem ext_rat {f g : ℚ →*₀ M₀}
+  (h : f.comp (int.cast_ring_hom ℚ : ℤ →*₀ ℚ) = g.comp (int.cast_ring_hom ℚ)) : f = g :=
+ext_rat' $ congr_fun h
 
 /-- Positive integer values of a morphism `φ` and its value on `-1` completely determine `φ`. -/
-theorem ext_rat_on_pnat {f g : ℚ →*₀ M}
+theorem ext_rat_on_pnat
   (same_on_neg_one : f (-1) = g (-1)) (same_on_pnat : ∀ n : ℕ, 0 < n → f n = g n) : f = g :=
-ext_rat $ ext_int' (by simpa) ‹_›
+ext_rat' $ fun_like.congr_fun $ show (f : ℚ →*₀ M₀).comp (int.cast_ring_hom ℚ : ℤ →*₀ ℚ) =
+  (g : ℚ →*₀ M₀).comp (int.cast_ring_hom ℚ : ℤ →*₀ ℚ),
+  from ext_int' (by simpa) (by simpa)
 
 end monoid_with_zero_hom
 
+/-- Any two ring homomorphisms from `ℚ` to a semiring are equal. If the codomain is a division ring,
+then this lemma follows from `eq_rat_cast`. -/
+lemma ring_hom.ext_rat {R : Type*} [semiring R] [ring_hom_class F ℚ R] (f g : F) : f = g :=
+monoid_with_zero_hom.ext_rat' $ ring_hom.congr_fun $
+  ((f : ℚ →+* R).comp (int.cast_ring_hom ℚ)).ext_int ((g : ℚ →+* R).comp (int.cast_ring_hom ℚ))
+
+instance rat.subsingleton_ring_hom {R : Type*} [semiring R] : subsingleton (ℚ →+* R) :=
+⟨ring_hom.ext_rat⟩
+
 namespace mul_opposite
 
 variables [division_ring α]

src/ring_theory/witt_vector/structure_polynomial.lean

@@ -133,7 +133,7 @@ theorem witt_structure_rat_prop (Φ : mv_polynomial idx ℚ) (n : ℕ) :
 calc bind₁ (witt_structure_rat p Φ) (W_ ℚ n)
     = bind₁ (λ k, bind₁ (λ i, (rename (prod.mk i)) (W_ ℚ k)) Φ)
         (bind₁ (X_in_terms_of_W p ℚ) (W_ ℚ n)) :
-      by { rw bind₁_bind₁, apply eval₂_hom_congr (ring_hom.ext_rat _ _) rfl rfl }
+      by { rw bind₁_bind₁, exact eval₂_hom_congr (ring_hom.ext_rat _ _) rfl rfl }
 ... = bind₁ (λ i, (rename (prod.mk i) (W_ ℚ n))) Φ :
       by rw [bind₁_X_in_terms_of_W_witt_polynomial p _ n, bind₁_X_right]