[Merged by Bors] - chore(algebra/ring/ulift): Split off and golf field instances

src/algebra/field/ulift.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import algebra.field.basic
+import algebra.ring.ulift
+
+/-!
+# Field instances for `ulift`
+
+This file defines instances for field, semifield and related structures on `ulift` types.
+(Recall `ulift α` is just a "copy" of a type `α` in a higher universe.)
+-/
+
+universes u v
+variables {α : Type u} {x y : ulift.{v} α}
+
+namespace ulift
+
+instance [has_rat_cast α] : has_rat_cast (ulift α) := ⟨λ a, up a⟩
+
+@[simp, norm_cast] lemma up_rat_cast [has_rat_cast α] (q : ℚ) : up (q : α) = q := rfl
+@[simp, norm_cast] lemma down_rat_cast [has_rat_cast α] (q : ℚ) : down (q : ulift α) = q := rfl
+
+instance division_semiring [division_semiring α] : division_semiring (ulift α) :=
+by refine down_injective.division_semiring down _ _ _ _ _ _ _ _ _ _; intros; refl
+
+instance semifield [semifield α] : semifield (ulift α) :=
+{ ..ulift.division_semiring, ..ulift.comm_group_with_zero }
+
+instance division_ring [division_ring α] : division_ring (ulift α) :=
+{ ..ulift.division_semiring, ..ulift.add_group }
+
+instance field [field α] : field (ulift α) :=
+{ ..ulift.semifield, ..ulift.division_ring }
+
+end ulift

src/algebra/ring/ulift.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.group.ulift
-import algebra.field.defs
 import algebra.ring.equiv
 
 /-!
@@ -25,6 +24,14 @@ variables {α : Type u} {x y : ulift.{v} α}
 
 namespace ulift
 
+instance [has_nat_cast α] : has_nat_cast (ulift α) := ⟨λ n, up n⟩
+instance [has_int_cast α] : has_int_cast (ulift α) := ⟨λ n, up n⟩
+
+@[simp, norm_cast] lemma up_nat_cast [has_nat_cast α] (n : ℕ) : up (n : α) = n := rfl
+@[simp, norm_cast] lemma up_int_cast [has_int_cast α] (n : ℤ) : up (n : α) = n := rfl
+@[simp, norm_cast] lemma down_nat_cast [has_nat_cast α] (n : ℕ) : down (n : ulift α) = n := rfl
+@[simp, norm_cast] lemma down_int_cast [has_int_cast α] (n : ℤ) : down (n : ulift α) = n := rfl
+
 instance mul_zero_class [mul_zero_class α] : mul_zero_class (ulift α) :=
 by refine_struct { zero := (0 : ulift α), mul := (*), .. }; tactic.pi_instance_derive_field
 
@@ -107,25 +114,4 @@ 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
-  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,
-  tauto
-end
-
 end ulift