[Merged by Bors] - chore: Split off and golf ulift field instances

Mathlib.lean

@@ -49,6 +49,7 @@ import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Field.Opposite
 import Mathlib.Algebra.Field.Power
+import Mathlib.Algebra.Field.ULift
 import Mathlib.Algebra.Free
 import Mathlib.Algebra.FreeMonoid.Basic
 import Mathlib.Algebra.FreeMonoid.Count
@@ -185,6 +186,7 @@ import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Algebra.Order.Monoid.WithZero.Basic
 import Mathlib.Algebra.Order.Monoid.WithZero.Defs
 import Mathlib.Algebra.Order.Nonneg.Field
+import Mathlib.Algebra.Order.Nonneg.Floor
 import Mathlib.Algebra.Order.Nonneg.Ring
 import Mathlib.Algebra.Order.Pi
 import Mathlib.Algebra.Order.Pointwise

Mathlib/Algebra/Field/ULift.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+
+! This file was ported from Lean 3 source module algebra.field.ulift
+! leanprover-community/mathlib commit 13e18cfa070ea337ea960176414f5ae3a1534aae
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Field.Basic
+import Mathlib.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.)
+-/
+
+universe u v
+variable {α : Type u} {x y : ULift.{v} α}
+
+namespace ULift
+
+instance [RatCast α] : RatCast (ULift α) := ⟨λ a ↦ up a⟩
+
+@[simp, norm_cast]
+theorem up_ratCast [RatCast α] (q : ℚ) : up (q : α) = q :=
+  rfl
+#align ulift.up_rat_cast ULift.up_ratCast
+
+@[simp, norm_cast]
+theorem down_ratCast [RatCast α] (q : ℚ) : down (q : ULift α) = q :=
+  rfl
+#align ulift.down_rat_cast ULift.down_ratCast
+
+instance divisionSemiring [DivisionSemiring α] : DivisionSemiring (ULift α) := by
+  refine' down_injective.divisionSemiring down .. <;> intros <;> rfl
+#align ulift.division_semiring ULift.divisionSemiring
+
+instance semifield [Semifield α] : Semifield (ULift α) :=
+  { ULift.divisionSemiring, ULift.commGroupWithZero with }
+#align ulift.semifield ULift.semifield
+
+instance divisionRing [DivisionRing α] : DivisionRing (ULift α) := by
+  refine' down_injective.divisionRing down .. <;> intros <;> rfl
+#align ulift.division_ring ULift.divisionRing
+
+instance field [Field α] : Field (ULift α) :=
+  { ULift.semifield, ULift.divisionRing with }
+#align ulift.field ULift.field
+
+end ULift

Mathlib/Algebra/Group/ULift.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.group.ulift
-! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94
+! leanprover-community/mathlib commit 13e18cfa070ea337ea960176414f5ae3a1534aae
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -140,23 +140,47 @@ instance monoid [Monoid α] : Monoid (ULift α) :=
 #align ulift.monoid ULift.monoid
 #align ulift.add_monoid ULift.addMonoid
 
+@[to_additive]
+instance commMonoid [CommMonoid α] : CommMonoid (ULift α) :=
+  Equiv.ulift.injective.commMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
+#align ulift.comm_monoid ULift.commMonoid
+#align ulift.add_comm_monoid ULift.addCommMonoid
+
+instance natCast [NatCast α] : NatCast (ULift α) := ⟨λ a ↦ up a⟩
+#align ulift.has_nat_cast ULift.natCast
+instance intCast [IntCast α] : IntCast (ULift α) := ⟨λ a ↦ up a⟩
+#align ulift.has_int_cast ULift.intCast
+
+@[simp, norm_cast]
+theorem up_natCast [NatCast α] (n : ℕ) : up (n : α) = n :=
+  rfl
+#align ulift.up_nat_cast ULift.up_natCast
+
+@[simp, norm_cast]
+theorem up_intCast [IntCast α] (n : ℤ) : up (n : α) = n :=
+  rfl
+#align ulift.up_int_cast ULift.up_intCast
+
+@[simp, norm_cast]
+theorem down_natCast [NatCast α] (n : ℕ) : down (n : ULift α) = n :=
+  rfl
+#align ulift.down_nat_cast ULift.down_natCast
+
+@[simp, norm_cast]
+theorem down_intCast [IntCast α] (n : ℤ) : down (n : ULift α) = n :=
+  rfl
+#align ulift.down_int_cast ULift.down_intCast
+
 instance addMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (ULift α) :=
   { ULift.one, ULift.addMonoid with
       natCast := fun n => ⟨n⟩
       natCast_zero := congr_arg ULift.up Nat.cast_zero,
       natCast_succ := fun _ => congr_arg ULift.up (Nat.cast_succ _) }
 #align ulift.add_monoid_with_one ULift.addMonoidWithOne
 
-@[simp]
-theorem nat_cast_down [AddMonoidWithOne α] (n : ℕ) : (n : ULift α).down = n :=
-  rfl
-#align ulift.nat_cast_down ULift.nat_cast_down
-
-@[to_additive]
-instance commMonoid [CommMonoid α] : CommMonoid (ULift α) :=
-  Equiv.ulift.injective.commMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
-#align ulift.comm_monoid ULift.commMonoid
-#align ulift.add_comm_monoid ULift.addCommMonoid
+instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne (ULift α) :=
+  { ULift.addMonoidWithOne, ULift.addCommMonoid with }
+#align ulift.add_comm_monoid_with_one ULift.addCommMonoidWithOne
 
 instance monoidWithZero [MonoidWithZero α] : MonoidWithZero (ULift α) :=
   Equiv.ulift.injective.monoidWithZero _ rfl rfl (fun _ _ => rfl) fun _ _ => rfl
@@ -180,24 +204,23 @@ instance group [Group α] : Group (ULift α) :=
 #align ulift.group ULift.group
 #align ulift.add_group ULift.addGroup
 
+@[to_additive]
+instance commGroup [CommGroup α] : CommGroup (ULift α) :=
+  Equiv.ulift.injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
+    (fun _ _ => rfl) fun _ _ => rfl
+#align ulift.comm_group ULift.commGroup
+#align ulift.add_comm_group ULift.addCommGroup
+
 instance addGroupWithOne [AddGroupWithOne α] : AddGroupWithOne (ULift α) :=
   { ULift.addMonoidWithOne, ULift.addGroup with
       intCast := fun n => ⟨n⟩,
       intCast_ofNat := fun _ => congr_arg ULift.up (Int.cast_ofNat _),
       intCast_negSucc := fun _ => congr_arg ULift.up (Int.cast_negSucc _) }
 #align ulift.add_group_with_one ULift.addGroupWithOne
 
-@[simp]
-theorem int_cast_down [AddGroupWithOne α] (n : ℤ) : (n : ULift α).down = n :=
-  rfl
-#align ulift.int_cast_down ULift.int_cast_down
-
-@[to_additive]
-instance commGroup [CommGroup α] : CommGroup (ULift α) :=
-  Equiv.ulift.injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
-#align ulift.comm_group ULift.commGroup
-#align ulift.add_comm_group ULift.addCommGroup
+instance addCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne (ULift α) :=
+  { ULift.addGroupWithOne, ULift.addCommGroup with }
+#align ulift.add_comm_group_with_one ULift.addCommGroupWithOne
 
 instance groupWithZero [GroupWithZero α] : GroupWithZero (ULift α) :=
   Equiv.ulift.injective.groupWithZero _ rfl rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)

Mathlib/Algebra/Order/Nonneg/Field.lean

@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 
 ! This file was ported from Lean 3 source module algebra.order.nonneg.field
-! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
+! leanprover-community/mathlib commit b3f4f007a962e3787aa0f3b5c7942a1317f7d88e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathlib.Algebra.Order.Archimedean
-import Mathlib.Algebra.Order.Nonneg.Ring
-import Mathlib.Algebra.Order.Field.InjSurj
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Field.Canonical.Defs
+import Mathlib.Algebra.Order.Field.InjSurj
+import Mathlib.Algebra.Order.Nonneg.Ring
 
 /-!
 # Semifield structure on the type of nonnegative elements
@@ -100,34 +100,4 @@ instance linearOrderedCommGroupWithZero [LinearOrderedField α] :
   inferInstance
 #align nonneg.linear_ordered_comm_group_with_zero Nonneg.linearOrderedCommGroupWithZero
 
-/-! ### Floor -/
-
-
-instance archimedean [OrderedAddCommMonoid α] [Archimedean α] : Archimedean { x : α // 0 ≤ x } :=
-  ⟨fun x y hy =>
-    let ⟨n, hr⟩ := Archimedean.arch (x : α) (hy : (0 : α) < y)
-    ⟨n, show (x : α) ≤ (n • y : { x : α // 0 ≤ x }) by simp [*, -nsmul_eq_mul, nsmul_coe]⟩⟩
-#align nonneg.archimedean Nonneg.archimedean
-
-instance floorSemiring [OrderedSemiring α] [FloorSemiring α] :
-    FloorSemiring { r : α // 0 ≤ r } where
-  floor a := ⌊(a : α)⌋₊
-  ceil a := ⌈(a : α)⌉₊
-  floor_of_neg ha := FloorSemiring.floor_of_neg ha
-  gc_floor ha := FloorSemiring.gc_floor (Subtype.coe_le_coe.2 ha)
-  gc_ceil a n := FloorSemiring.gc_ceil (a : α) n
-#align nonneg.floor_semiring Nonneg.floorSemiring
-
-@[norm_cast]
-theorem nat_floor_coe [OrderedSemiring α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) :
-    ⌊(a : α)⌋₊ = ⌊a⌋₊ :=
-  rfl
-#align nonneg.nat_floor_coe Nonneg.nat_floor_coe
-
-@[norm_cast]
-theorem nat_ceil_coe [OrderedSemiring α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) :
-    ⌈(a : α)⌉₊ = ⌈a⌉₊ :=
-  rfl
-#align nonneg.nat_ceil_coe Nonneg.nat_ceil_coe
-
 end Nonneg

Mathlib/Algebra/Order/Nonneg/Floor.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2021 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+! This file was ported from Lean 3 source module algebra.order.nonneg.floor
+! leanprover-community/mathlib commit b3f4f007a962e3787aa0f3b5c7942a1317f7d88e
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Order.Nonneg.Ring
+import Mathlib.Algebra.Order.Archimedean
+
+/-!
+# Nonnegative elements are archimedean
+
+This file defines instances and prove some properties about the nonnegative elements
+`{x : α // 0 ≤ x}` of an arbitrary type `α`.
+
+This is used to derive algebraic structures on `ℝ≥0` and `ℚ≥0` automatically.
+
+## Main declarations
+
+* `{x : α // 0 ≤ x}` is a `floor_semiring` if `α` is.
+-/
+
+namespace Nonneg
+
+variable {α : Type _}
+
+instance archimedean [OrderedAddCommMonoid α] [Archimedean α] : Archimedean { x : α // 0 ≤ x } :=
+  ⟨fun x y hy =>
+    let ⟨n, hr⟩ := Archimedean.arch (x : α) (hy : (0 : α) < y)
+    ⟨n, show (x : α) ≤ (n • y : { x : α // 0 ≤ x }) by simp [*, -nsmul_eq_mul, nsmul_coe]⟩⟩
+#align nonneg.archimedean Nonneg.archimedean
+
+instance floorSemiring [OrderedSemiring α] [FloorSemiring α] :
+    FloorSemiring { r : α // 0 ≤ r } where
+  floor a := ⌊(a : α)⌋₊
+  ceil a := ⌈(a : α)⌉₊
+  floor_of_neg ha := FloorSemiring.floor_of_neg ha
+  gc_floor ha := FloorSemiring.gc_floor (Subtype.coe_le_coe.2 ha)
+  gc_ceil a n := FloorSemiring.gc_ceil (a : α) n
+#align nonneg.floor_semiring Nonneg.floorSemiring
+
+@[norm_cast]
+theorem nat_floor_coe [OrderedSemiring α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) :
+    ⌊(a : α)⌋₊ = ⌊a⌋₊ :=
+  rfl
+#align nonneg.nat_floor_coe Nonneg.nat_floor_coe
+
+@[norm_cast]
+theorem nat_ceil_coe [OrderedSemiring α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) :
+    ⌈(a : α)⌉₊ = ⌈a⌉₊ :=
+  rfl
+#align nonneg.nat_ceil_coe Nonneg.nat_ceil_coe

Mathlib/Algebra/Ring/ULift.lean

@@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.ring.ulift
-! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
+! leanprover-community/mathlib commit 13e18cfa070ea337ea960176414f5ae3a1534aae
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.ULift
-import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Ring.Equiv
 
 /-!
@@ -157,34 +156,4 @@ instance commRing [CommRing α] : CommRing (ULift α) :=
   { ULift.ring with mul_comm }
 #align ulift.comm_ring ULift.commRing
 
-instance [RatCast α] : RatCast (ULift α) :=
-  ⟨fun a => ULift.up ↑a⟩
-
-@[simp]
-theorem rat_cast_down [RatCast α] (n : ℚ) : ULift.down (n : ULift α) = n := rfl
-#align ulift.rat_cast_down ULift.rat_cast_down
-
-instance field [Field α] : Field (ULift α) :=
-  { @ULift.nontrivial α _, ULift.commRing with
-    inv := Inv.inv
-    div := Div.div
-    zpow := fun n a => ULift.up (a.down ^ n)
-    ratCast := fun a => (a : ULift α)
-    ratCast_mk := fun a b h1 h2 => by
-      apply ULift.down_inj.1
-      dsimp [RatCast.ratCast]
-      exact Field.ratCast_mk a b h1 h2
-    qsmul := (· • ·)
-    inv_zero
-    div_eq_mul_inv
-    qsmul_eq_mul' := fun _ _ => by
-      apply ULift.down_inj.1
-      dsimp [RatCast.ratCast]
-      exact DivisionRing.qsmul_eq_mul' _ _
-    zpow_zero' := DivInvMonoid.zpow_zero'
-    zpow_succ' := DivInvMonoid.zpow_succ'
-    zpow_neg' := DivInvMonoid.zpow_neg'
-    mul_inv_cancel := fun _ ha => by simp [ULift.down_inj.1, ha] }
-#align ulift.field ULift.field
-
 end ULift

Mathlib/Data/Rat/NNRat.lean

@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 
 ! This file was ported from Lean 3 source module data.rat.nnrat
-! leanprover-community/mathlib commit 28aa996fc6fb4317f0083c4e6daf79878d81be33
+! leanprover-community/mathlib commit b3f4f007a962e3787aa0f3b5c7942a1317f7d88e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.Order.Nonneg.Field
+import Mathlib.Algebra.Order.Nonneg.Floor
 
 /-!
 # Nonnegative rationals

Mathlib/Data/Real/NNReal.lean

@@ -4,15 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 
 ! This file was ported from Lean 3 source module data.real.nnreal
-! leanprover-community/mathlib commit b2ff9a3d7a15fd5b0f060b135421d6a89a999c2f
+! leanprover-community/mathlib commit b3f4f007a962e3787aa0f3b5c7942a1317f7d88e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathlib.Order.ConditionallyCompleteLattice.Group
 import Mathlib.Algebra.Algebra.Basic
-import Mathlib.Algebra.Order.Nonneg.Field
 import Mathlib.Algebra.Order.Field.Canonical.Basic
+import Mathlib.Algebra.Order.Nonneg.Field
+import Mathlib.Algebra.Order.Nonneg.Floor
 import Mathlib.Data.Real.Pointwise
+import Mathlib.Order.ConditionallyCompleteLattice.Group
 import Mathlib.Tactic.Positivity
 
 /-!