chore({algebra,data/rat}): use forgetful inheritance for algebra_rat (

#14894)

Throughout mathlib we've been struggling with diamonds arising from the `algebra_rat [division_ring K] [char_zero K] : algebra ℚ K` instance: since this instance provided its own inclusion map `to_fun : ℚ → K` and scalar multiplication by rationals `smul : ℚ → K → K`, it would not be definitionally equal to other instances such as `algebra.id`, and we'd need tactics like `convert` to deal with this inequality.

Following the previous `nsmul` and `zmul` refactors, this PR applies the forgetful inheritance pattern to the `algebra_rat` instance, allowing you to supply a definitionally convenient value for the conflicting `to_fun` and `smul` fields as the fields `of_rat` and `qsmul` in the `division_ring K` instance. `of_rat` is used to define the coercion `ℚ → K` (in the instance `rat.cast_coe`), whic is used to define the map `rat.cast_hom : ℚ →+* K`, which is used along with `qsmul` to define `algebra_rat`.

A default value for `of_rat` and `qsmul` and coherence proofs are provided using the `opt_param`/`auto_param` mechanism, just like for `nsmul` and `zsmul`.

I have included a test after the definition of `algebra_rat`, to ensure definitional equality with `algebra.id`.

src/algebra/algebra/basic.lean

@@ -758,7 +758,7 @@ end division_ring
 end alg_hom
 
 @[simp] lemma rat.smul_one_eq_coe {A : Type*} [division_ring A] [algebra ℚ A] (m : ℚ) :
-  m • (1 : A) = ↑m :=
+  @@has_smul.smul algebra.to_has_smul m (1 : A) = ↑m :=
 by rw [algebra.smul_def, mul_one, ring_hom.eq_rat_cast]
 
 set_option old_structure_cmd true
@@ -1327,7 +1327,13 @@ end
 section rat
 
 instance algebra_rat {α} [division_ring α] [char_zero α] : algebra ℚ α :=
-(rat.cast_hom α).to_algebra' $ λ r x, r.cast_commute x
+{ smul := (•),
+  smul_def' := division_ring.qsmul_eq_mul',
+  to_ring_hom := rat.cast_hom α,
+  commutes' := rat.cast_commute }
+
+/-- The two `algebra ℚ ℚ` instances should coincide. -/
+example : algebra_rat = algebra.id ℚ := rfl
 
 @[simp] theorem algebra_map_rat_rat : algebra_map ℚ ℚ = ring_hom.id ℚ :=
 subsingleton.elim _ _

src/algebra/field/basic.lean

@@ -50,23 +50,66 @@ set_option old_structure_cmd true
 universe u
 variables {α β K : Type*}
 
+/-- The default definition of the coercion `(↑(a : ℚ) : K)` for a division ring `K`
+is defined as `(a / b : K) = (a : K) * (b : K)⁻¹`.
+Use `coe` instead of `rat.cast_rec` for better definitional behaviour.
+-/
+def rat.cast_rec [has_lift_t ℕ K] [has_lift_t ℤ K] [has_mul K] [has_inv K] : ℚ → K
+| ⟨a, b, _, _⟩ := ↑a * (↑b)⁻¹
+
+/--
+Type class for the canonical homomorphism `ℚ → K`.
+-/
+@[protect_proj]
+class has_rat_cast (K : Type u) :=
+(rat_cast : ℚ → K)
+
+/-- The default definition of the scalar multiplication `(a : ℚ) • (x : K)` for a division ring `K`
+is given by `a • x = (↑ a) * x`.
+Use `(a : ℚ) • (x : K)` instead of `qsmul_rec` for better definitional behaviour.
+-/
+def qsmul_rec (coe : ℚ → K) [has_mul K] (a : ℚ) (x : K) : K :=
+coe a * x
+
 /-- A `division_semiring` is a `semiring` with multiplicative inverses for nonzero elements. -/
 @[protect_proj, ancestor semiring group_with_zero]
 class division_semiring (α : Type*) extends semiring α, group_with_zero α
 
-/-- A `division_ring` is a `ring` with multiplicative inverses for nonzero elements. -/
-@[protect_proj, ancestor ring division_semiring]
-class division_ring (α : Type*) extends ring α, div_inv_monoid α, nontrivial α :=
-(mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1)
-(inv_zero : (0 : α)⁻¹ = 0)
+/-- A `division_ring` is a `ring` with multiplicative inverses for nonzero elements.
+
+An instance of `division_ring K` includes maps `of_rat : ℚ → K` and `qsmul : ℚ → K → K`.
+If the division ring has positive characteristic p, we define `of_rat (1 / p) = 1 / 0 = 0`
+for consistency with our division by zero convention.
+The fields `of_rat` and `qsmul are needed to implement the
+`algebra_rat [division_ring K] : algebra ℚ K` instance, since we need to control the specific
+definitions for some special cases of `K` (in particular `K = ℚ` itself).
+See also Note [forgetful inheritance].
+-/
+@[protect_proj, ancestor ring div_inv_monoid nontrivial]
+class division_ring (K : Type u) extends ring K, div_inv_monoid K, nontrivial K, has_rat_cast K :=
+(mul_inv_cancel : ∀ {a : K}, a ≠ 0 → a * a⁻¹ = 1)
+(inv_zero : (0 : K)⁻¹ = 0)
+(rat_cast := rat.cast_rec)
+(rat_cast_mk : ∀ (a : ℤ) (b : ℕ) h1 h2, rat_cast ⟨a, b, h1, h2⟩ = a * b⁻¹ . try_refl_tac)
+(qsmul : ℚ → K → K := qsmul_rec rat_cast)
+(qsmul_eq_mul' : ∀ (a : ℚ) (x : K), qsmul a x = rat_cast a * x . try_refl_tac)
 
 /-- A `semifield` is a `comm_semiring` with multiplicative inverses for nonzero elements. -/
 @[protect_proj, ancestor comm_semiring division_semiring comm_group_with_zero]
 class semifield (α : Type*) extends comm_semiring α, division_semiring α, comm_group_with_zero α
 
-/-- A `field` is a `comm_ring` with multiplicative inverses for nonzero elements. -/
-@[protect_proj, ancestor comm_ring division_ring]
-class field (α : Type*) extends comm_ring α, division_ring α
+/-- A `field` is a `comm_ring` with multiplicative inverses for nonzero elements.
+
+An instance of `field K` includes maps `of_rat : ℚ → K` and `qsmul : ℚ → K → K`.
+If the field has positive characteristic p, we define `of_rat (1 / p) = 1 / 0 = 0`
+for consistency with our division by zero convention.
+The fields `of_rat` and `qsmul are needed to implement the
+`algebra_rat [division_ring K] : algebra ℚ K` instance, since we need to control the specific
+definitions for some special cases of `K` (in particular `K = ℚ` itself).
+See also Note [forgetful inheritance].
+-/
+@[protect_proj, ancestor comm_ring div_inv_monoid nontrivial]
+class field (K : Type u) extends comm_ring K, division_ring K
 
 @[priority 100] -- see Note [lower instance priority]
 instance division_ring.to_division_semiring [division_ring α] : division_semiring α :=
@@ -104,6 +147,30 @@ end division_semiring
 section division_ring
 variables [division_ring K] {a b : K}
 
+namespace rat
+
+/-- Construct the canonical injection from `ℚ` into an arbitrary
+  division ring. If the field has positive characteristic `p`,
+  we define `1 / p = 1 / 0 = 0` for consistency with our
+  division by zero convention. -/
+-- see Note [coercion into rings]
+@[priority 900] instance cast_coe {K : Type*} [has_rat_cast K] : has_coe_t ℚ K :=
+⟨has_rat_cast.rat_cast⟩
+
+theorem cast_mk' (a b h1 h2) : ((⟨a, b, h1, h2⟩ : ℚ) : K) = a * b⁻¹ :=
+division_ring.rat_cast_mk _ _ _ _
+
+theorem cast_def : ∀ (r : ℚ), (r : K) = r.num / r.denom
+| ⟨a, b, h1, h2⟩ := (cast_mk' _ _ _ _).trans (div_eq_mul_inv _ _).symm
+
+@[priority 100]
+instance smul_division_ring : has_smul ℚ K :=
+⟨division_ring.qsmul⟩
+
+lemma smul_def (a : ℚ) (x : K) : a • x = ↑a * x := division_ring.qsmul_eq_mul' a x
+
+end rat
+
 local attribute [simp]
   division_def mul_comm mul_assoc
   mul_left_comm mul_inv_cancel inv_mul_cancel
@@ -355,17 +422,23 @@ See note [reducible non-instances]. -/
 @[reducible]
 protected def function.injective.division_ring [division_ring K] {K'}
   [has_zero K'] [has_one K'] [has_add K'] [has_mul K'] [has_neg K'] [has_sub K'] [has_inv K']
-  [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_pow K' ℕ] [has_pow K' ℤ]
-  [has_nat_cast K'] [has_int_cast K']
+  [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_smul ℚ K'] [has_pow K' ℕ] [has_pow K' ℤ]
+  [has_nat_cast K'] [has_int_cast K'] [has_rat_cast K']
   (f : K' → K) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
   (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
   (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
   (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
   (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
+  (qsmul : ∀ x (n : ℚ), f (n • x) = n • f x)
   (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ x (n : ℤ), f (x ^ n) = f x ^ n)
-  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) :
+  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) (rat_cast : ∀ n : ℚ, f n = n) :
   division_ring K' :=
-{ .. hf.group_with_zero f zero one mul inv div npow zpow,
+{ rat_cast := coe,
+  rat_cast_mk := λ a b h1 h2, hf (by erw [rat_cast, mul, inv, int_cast, nat_cast];
+                                     exact division_ring.rat_cast_mk a b h1 h2),
+  qsmul := (•),
+  qsmul_eq_mul' := λ a x, hf (by erw [qsmul, mul, rat.smul_def, rat_cast]),
+  .. hf.group_with_zero f zero one mul inv div npow zpow,
   .. hf.ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast }
 
 /-- Pullback a `field` along an injective function. -/
@@ -388,15 +461,21 @@ See note [reducible non-instances]. -/
 @[reducible]
 protected def function.injective.field [field K] {K'}
   [has_zero K'] [has_mul K'] [has_add K'] [has_neg K'] [has_sub K'] [has_one K'] [has_inv K']
-  [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_pow K' ℕ] [has_pow K' ℤ]
-  [has_nat_cast K'] [has_int_cast K']
+  [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_smul ℚ K'] [has_pow K' ℕ] [has_pow K' ℤ]
+  [has_nat_cast K'] [has_int_cast K'] [has_rat_cast K']
   (f : K' → K) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
   (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
   (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
   (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
   (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
+  (qsmul : ∀ x (n : ℚ), f (n • x) = n • f x)
   (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ x (n : ℤ), f (x ^ n) = f x ^ n)
-  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) :
+  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) (rat_cast : ∀ n : ℚ, f n = n) :
   field K' :=
-{ .. hf.comm_group_with_zero f zero one mul inv div npow zpow,
+{ rat_cast := coe,
+  rat_cast_mk := λ a b h1 h2, hf (by erw [rat_cast, mul, inv, int_cast, nat_cast];
+                                     exact division_ring.rat_cast_mk a b h1 h2),
+  qsmul := (•),
+  qsmul_eq_mul' := λ a x, hf (by erw [qsmul, mul, rat.smul_def, rat_cast]),
+  .. hf.comm_group_with_zero f zero one mul inv div npow zpow,
   .. hf.comm_ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast }

src/algebra/group/ulift.lean

@@ -79,6 +79,10 @@ instance add_monoid_with_one [add_monoid_with_one α] : add_monoid_with_one (uli
   nat_cast_succ := λ n, congr_arg ulift.up (nat.cast_succ _),
   .. ulift.has_one, .. ulift.add_monoid }
 
+@[simp] lemma nat_cast_down [add_monoid_with_one α] (n : ℕ) :
+  (n : ulift α).down = n :=
+rfl
+
 @[to_additive]
 instance comm_monoid [comm_monoid α] : comm_monoid (ulift α) :=
 equiv.ulift.injective.comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
@@ -105,6 +109,10 @@ instance add_group_with_one [add_group_with_one α] : add_group_with_one (ulift
   int_cast_neg_succ_of_nat := λ n, congr_arg ulift.up (int.cast_neg_succ_of_nat _),
   .. ulift.add_monoid_with_one, .. ulift.add_group }
 
+@[simp] lemma int_cast_down [add_group_with_one α] (n : ℤ) :
+  (n : ulift α).down = n :=
+rfl
+
 @[to_additive]
 instance comm_group [comm_group α] : comm_group (ulift α) :=
 equiv.ulift.injective.comm_group _ rfl (λ _ _, rfl) (λ _, rfl)

src/algebra/order/field.lean

@@ -60,19 +60,22 @@ def injective.linear_ordered_semifield [linear_ordered_semifield α] [has_zero 
 /-- Pullback a `linear_ordered_field` under an injective map. -/
 @[reducible] -- See note [reducible non-instances]
 def injective.linear_ordered_field [linear_ordered_field α] [has_zero β] [has_one β] [has_add β]
-  [has_mul β] [has_neg β] [has_sub β] [has_pow β ℕ] [has_smul ℕ β] [has_smul ℤ β]
-  [has_nat_cast β] [has_int_cast β] [has_inv β] [has_div β] [has_pow β ℤ] [has_sup β] [has_inf β]
+  [has_mul β] [has_neg β] [has_sub β] [has_pow β ℕ] [has_smul ℕ β] [has_smul ℤ β] [has_smul ℚ β]
+  [has_nat_cast β] [has_int_cast β] [has_rat_cast β] [has_inv β] [has_div β] [has_pow β ℤ]
+  [has_sup β] [has_inf β]
   (f : β → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
   (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
   (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
   (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
   (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
+  (qsmul : ∀ x (n : ℚ), f (n • x) = n • f x)
   (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ x (n : ℤ), f (x ^ n) = f x ^ n)
-  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n)
+  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) (rat_cast : ∀ n : ℚ, f n = n)
   (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
   linear_ordered_field β :=
 { .. hf.linear_ordered_ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf,
-  .. hf.field f zero one add mul neg sub inv div nsmul zsmul npow zpow nat_cast int_cast }
+  .. hf.field f zero one add mul neg sub inv div nsmul zsmul qsmul npow zpow nat_cast int_cast
+      rat_cast }
 
 end function
 

src/algebra/ring/ulift.lean

@@ -103,9 +103,21 @@ instance comm_ring [comm_ring α] : comm_ring (ulift α) :=
 by refine_struct { .. ulift.ring };
 tactic.pi_instance_derive_field
 
+instance [has_rat_cast α] : has_rat_cast (ulift α) :=
+⟨λ a, ulift.up (coe a)⟩
+
+@[simp] lemma rat_cast_down [has_rat_cast α] (n : ℚ) : ulift.down (n : ulift α) = n :=
+rfl
+
 instance field [field α] : field (ulift α) :=
-begin refine_struct { zero := (0 : ulift α), inv := has_inv.inv, div := has_div.div,
-  zpow := λ n a, ulift.up (a.down ^ n),
+begin
+  have of_rat_mk : ∀ a b h1 h2, ((⟨a, b, h1, h2⟩ : ℚ) : ulift α) = ↑a * (↑b)⁻¹,
+  { intros a b h1 h2,
+    ext,
+    rw [rat_cast_down, mul_down, inv_down, nat_cast_down, int_cast_down],
+    exact field.rat_cast_mk a b h1 h2 },
+  refine_struct { zero := (0 : ulift α), inv := has_inv.inv, div := has_div.div,
+  zpow := λ n a, ulift.up (a.down ^ n), rat_cast := coe, rat_cast_mk := of_rat_mk, qsmul := (•),
   .. @ulift.nontrivial α _, .. ulift.comm_ring }; tactic.pi_instance_derive_field,
   -- `mul_inv_cancel` requires special attention: it leaves the goal `∀ {a}, a ≠ 0 → a * a⁻¹ = 1`.
   cases a,

src/algebra/star/self_adjoint.lean

@@ -127,8 +127,15 @@ end ring
 section comm_ring
 variables [comm_ring R] [star_ring R]
 
+lemma mul_mem {x y : R} (hx : x ∈ self_adjoint R) (hy : y ∈ self_adjoint R) :
+  x * y ∈ self_adjoint R :=
+begin
+  rw mem_iff at ⊢ hx hy,
+  rw [star_mul', hx, hy]
+end
+
 instance : has_mul (self_adjoint R) :=
-⟨λ x y, ⟨(x : R) * y, by simp only [mem_iff, star_mul', star_coe_eq]⟩⟩
+⟨λ x y, ⟨(x : R) * y, mul_mem x.prop y.prop⟩⟩
 
 @[simp, norm_cast] lemma coe_mul (x y : self_adjoint R) : ↑(x * y) = (x : R) * y := rfl
 
@@ -159,11 +166,27 @@ instance : has_pow (self_adjoint R) ℤ :=
 
 @[simp, norm_cast] lemma coe_zpow (x : self_adjoint R) (z : ℤ) : ↑(x ^ z) = (x : R) ^ z := rfl
 
+lemma rat_cast_mem : ∀ (x : ℚ), (x : R) ∈ self_adjoint R
+| ⟨a, b, h1, h2⟩ :=
+  by rw [mem_iff, rat.cast_mk', star_mul', star_inv', star_nat_cast, star_int_cast]
+
+instance : has_rat_cast (self_adjoint R) :=
+⟨λ n, ⟨n, rat_cast_mem n⟩⟩
+
+@[simp, norm_cast] lemma coe_rat_cast (x : ℚ) : ↑(x : self_adjoint R) = (x : R) :=
+rfl
+
+instance has_qsmul : has_smul ℚ (self_adjoint R) :=
+⟨λ a x, ⟨a • x, by rw rat.smul_def; exact mul_mem (rat_cast_mem a) x.prop⟩⟩
+
+@[simp, norm_cast] lemma coe_rat_smul (x : self_adjoint R) (a : ℚ) : ↑(a • x) = a • (x : R) :=
+rfl
+
 instance : field (self_adjoint R) :=
 function.injective.field _ subtype.coe_injective
   (self_adjoint R).coe_zero coe_one (self_adjoint R).coe_add coe_mul (self_adjoint R).coe_neg
   (self_adjoint R).coe_sub coe_inv coe_div (self_adjoint R).coe_nsmul (self_adjoint R).coe_zsmul
-  coe_pow coe_zpow (λ _, rfl) (λ _, rfl)
+  coe_rat_smul coe_pow coe_zpow (λ _, rfl) (λ _, rfl) coe_rat_cast
 
 end field
 

src/data/rat/basic.lean

@@ -42,6 +42,9 @@ instance : field ℚ :=
   one              := 1,
   mul              := (*),
   inv              := has_inv.inv,
+  rat_cast         := id,
+  rat_cast_mk      := λ a b h1 h2, (num_div_denom _).symm,
+  qsmul            := (*),
   .. rat.comm_ring,
   .. rat.comm_group_with_zero}
 

src/data/rat/cast.lean

@@ -34,17 +34,8 @@ open_locale rat
 section with_div_ring
 variable [division_ring α]
 
-/-- Construct the canonical injection from `ℚ` into an arbitrary
-  division ring. If the field has positive characteristic `p`,
-  we define `1 / p = 1 / 0 = 0` for consistency with our
-  division by zero convention. -/
--- see Note [coercion into rings]
-@[priority 900] instance cast_coe : has_coe_t ℚ α := ⟨λ r, r.1 / r.2⟩
-
-theorem cast_def (r : ℚ) : (r : α) = r.num / r.denom := rfl
-
 @[simp] theorem cast_of_int (n : ℤ) : (of_int n : α) = n :=
-show (n / (1:ℕ) : α) = n, by rw [nat.cast_one, div_one]
+(cast_def _).trans $ show (n / (1:ℕ) : α) = n, by rw [nat.cast_one, div_one]
 
 @[simp, norm_cast] theorem cast_coe_int (n : ℤ) : ((n : ℚ) : α) = n :=
 by rw [coe_int_eq_of_int, cast_of_int]
@@ -59,7 +50,7 @@ by rw [← int.cast_coe_nat, cast_coe_int, int.cast_coe_nat]
 (cast_of_int _).trans int.cast_one
 
 theorem cast_commute (r : ℚ) (a : α) : commute ↑r a :=
-(r.1.cast_commute a).div_left (r.2.cast_commute a)
+by simpa only [cast_def] using (r.1.cast_commute a).div_left (r.2.cast_commute a)
 
 theorem cast_comm (r : ℚ) (a : α) : (r : α) * a = a * r :=
 (cast_commute r a).eq
@@ -81,8 +72,8 @@ begin
   rw [num_denom'] at e,
   have := congr_arg (coe : ℤ → α) ((mk_eq b0' $ ne_of_gt $ int.coe_nat_pos.2 h).1 e),
   rw [int.cast_mul, int.cast_mul, int.cast_coe_nat] at this,
-  symmetry, change (a / b : α) = n / d,
-  rw [div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
+  symmetry,
+  rw [cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
       ← mul_assoc, this, mul_assoc, mul_inv_cancel b0, mul_one]
 end
 
@@ -102,7 +93,7 @@ end
 end
 
 @[simp, norm_cast] theorem cast_neg : ∀ n, ((-n : ℚ) : α) = -n
-| ⟨n, d, h, c⟩ := show (↑-n / d : α) = -(n / d),
+| ⟨n, d, h, c⟩ := by simpa only [cast_def] using show (↑-n / d : α) = -(n / d),
   by rw [div_eq_mul_inv, div_eq_mul_inv, int.cast_neg, neg_mul_eq_neg_mul]
 
 @[norm_cast] theorem cast_sub_of_ne_zero {m n : ℚ}
@@ -291,7 +282,7 @@ open rat ring_hom
 lemma ring_hom.eq_rat_cast {k} [division_ring k] (f : ℚ →+* k) (r : ℚ) : f r = r :=
 calc f r = f (r.1 / r.2) : by rw [← int.cast_coe_nat, ← mk_eq_div, num_denom]
      ... = f r.1 / f r.2 : f.map_div _ _
-     ... = r.1 / r.2     : by rw [map_nat_cast, map_int_cast]
+     ... = r             : by rw [map_nat_cast, map_int_cast, cast_def]
 
 -- This seems to be true for a `[char_p k]` too because `k'` must have the same characteristic
 -- but the proof would be much longer