/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
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 564bcc44d2b394a50c0cd6340c14a6b02a50a99a
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Cast.Defs
import Mathlib.Algebra.Hom.Equiv.Basic
import Mathlib.Algebra.GroupWithZero.InjSurj

/-!
# `ULift` instances for groups and monoids

This file defines instances for group, monoid, semigroup and related structures on `ULift` types.

(Recall `ULift α` is just a "copy" of a type `α` in a higher universe.)

We also provide `MulEquiv.ulift : ULift R ≃* R` (and its additive analogue).
-/


universe u v

variable {
α: Type u
α : 
Type u: Type (u+1)
Type u} {
β: Type ?u.15
β : 
Type _: Type (?u.4+1)
Type _} {
x: ULift α
x 
y: ULift α
y : 
ULift: Type ?u.1023 → Type (max?u.1023v)
ULift.{v} 
α: Type u
α}

namespace ULift

@[
to_additive: {α : Type u} → [inst : Zero α] → Zero (ULift α)
to_additive]
instance 
one: {α : Type u} → [inst : One α] → One (ULift α)
one [
One: Type ?u.24 → Type ?u.24
One 
α: Type u
α] : 
One: Type ?u.27 → Type ?u.27
One (
ULift: Type ?u.28 → Type (max?u.28?u.29)
ULift 
α: Type u
α) :=
  ⟨⟨
1: ?m.44
1⟩⟩
#align ulift.has_one 
ULift.one: {α : Type u} → [inst : One α] → One (ULift α)
ULift.one
#align ulift.has_zero 
ULift.zero: {α : Type u} → [inst : Zero α] → Zero (ULift α)
ULift.zero

@[
to_additive: ∀ {α : Type u} [inst : Zero α], 0.down = 0
to_additive (attr := simp)]
theorem 
one_down: ∀ [inst : One α], 1.down = 1
one_down [
One: Type ?u.164 → Type ?u.164
One 
α: Type u
α] : (
1: ?m.172
1 : 
ULift: Type ?u.169 → Type (max?u.169?u.170)
ULift 
α: Type u
α).
down: {α : Type ?u.210} → ULift α → α
down = 
1: ?m.214
1 :=
  
rfl: ∀ {α : Sort ?u.249} {a : α}, a = a
rfl
#align ulift.one_down 
ULift.one_down: ∀ {α : Type u} [inst : One α], 1.down = 1
ULift.one_down
#align ulift.zero_down 
ULift.zero_down: ∀ {α : Type u} [inst : Zero α], 0.down = 0
ULift.zero_down

@[
to_additive: {α : Type u} → [inst : Add α] → Add (ULift α)
to_additive]
instance 
mul: {α : Type u} → [inst : Mul α] → Mul (ULift α)
mul [
Mul: Type ?u.293 → Type ?u.293
Mul 
α: Type u
α] : 
Mul: Type ?u.296 → Type ?u.296
Mul (
ULift: Type ?u.297 → Type (max?u.297?u.298)
ULift 
α: Type u
α) :=
  ⟨fun 
f: ?m.307
f 
g: ?m.310
g => ⟨
f: ?m.307
f.
down: {α : Type ?u.321} → ULift α → α
down * 
g: ?m.310
g.
down: {α : Type ?u.325} → ULift α → α
down⟩⟩
#align ulift.has_mul 
ULift.mul: {α : Type u} → [inst : Mul α] → Mul (ULift α)
ULift.mul
#align ulift.has_add 
ULift.add: {α : Type u} → [inst : Add α] → Add (ULift α)
ULift.add

@[
to_additive: ∀ {α : Type u} {x y : ULift α} [inst : Add α], (x + y).down = x.down + y.down
to_additive (attr := simp)]
theorem 
mul_down: ∀ [inst : Mul α], (x * y).down = x.down * y.down
mul_down [
Mul: Type ?u.569 → Type ?u.569
Mul 
α: Type u
α] : (
x: ULift α
x * 
y: ULift α
y).
down: {α : Type ?u.631} → ULift α → α
down = 
x: ULift α
x.
down: {α : Type ?u.638} → ULift α → α
down * 
y: ULift α
y.
down: {α : Type ?u.641} → ULift α → α
down :=
  
rfl: ∀ {α : Sort ?u.682} {a : α}, a = a
rfl
#align ulift.mul_down 
ULift.mul_down: ∀ {α : Type u} {x y : ULift α} [inst : Mul α], (x * y).down = x.down * y.down
ULift.mul_down
#align ulift.add_down 
ULift.add_down: ∀ {α : Type u} {x y : ULift α} [inst : Add α], (x + y).down = x.down + y.down
ULift.add_down

@[
to_additive: {α : Type u} → [inst : Sub α] → Sub (ULift α)
to_additive]
instance 
div: {α : Type u} → [inst : Div α] → Div (ULift α)
div [
Div: Type ?u.750 → Type ?u.750
Div 
α: Type u
α] : 
Div: Type ?u.753 → Type ?u.753
Div (
ULift: Type ?u.754 → Type (max?u.754?u.755)
ULift 
α: Type u
α) :=
  ⟨fun 
f: ?m.764
f 
g: ?m.767
g => ⟨
f: ?m.764
f.
down: {α : Type ?u.778} → ULift α → α
down / 
g: ?m.767
g.
down: {α : Type ?u.782} → ULift α → α
down⟩⟩
#align ulift.has_div 
ULift.div: {α : Type u} → [inst : Div α] → Div (ULift α)
ULift.div
#align ulift.has_sub 
ULift.sub: {α : Type u} → [inst : Sub α] → Sub (ULift α)
ULift.sub

@[
to_additive: ∀ {α : Type u} {x y : ULift α} [inst : Sub α], (x - y).down = x.down - y.down
to_additive (attr := simp)]
theorem 
div_down: ∀ [inst : Div α], (x / y).down = x.down / y.down
div_down [
Div: Type ?u.1026 → Type ?u.1026
Div 
α: Type u
α] : (
x: ULift α
x / 
y: ULift α
y).
down: {α : Type ?u.1088} → ULift α → α
down = 
x: ULift α
x.
down: {α : Type ?u.1095} → ULift α → α
down / 
y: ULift α
y.
down: {α : Type ?u.1098} → ULift α → α
down :=
  
rfl: ∀ {α : Sort ?u.1139} {a : α}, a = a
rfl
#align ulift.div_down 
ULift.div_down: ∀ {α : Type u} {x y : ULift α} [inst : Div α], (x / y).down = x.down / y.down
ULift.div_down
#align ulift.sub_down 
ULift.sub_down: ∀ {α : Type u} {x y : ULift α} [inst : Sub α], (x - y).down = x.down - y.down
ULift.sub_down

@[
to_additive: {α : Type u} → [inst : Neg α] → Neg (ULift α)
to_additive]
instance 
inv: [inst : Inv α] → Inv (ULift α)
inv [
Inv: Type ?u.1207 → Type ?u.1207
Inv 
α: Type u
α] : 
Inv: Type ?u.1210 → Type ?u.1210
Inv (
ULift: Type ?u.1211 → Type (max?u.1211?u.1212)
ULift 
α: Type u
α) :=
  ⟨fun 
f: ?m.1221
f => ⟨
f: ?m.1221
f.
down: {α : Type ?u.1243} → ULift α → α
down⁻¹⟩⟩
#align ulift.has_inv 
ULift.inv: {α : Type u} → [inst : Inv α] → Inv (ULift α)
ULift.inv
#align ulift.has_neg 
ULift.neg: {α : Type u} → [inst : Neg α] → Neg (ULift α)
ULift.neg

@[
to_additive: ∀ {α : Type u} {x : ULift α} [inst : Neg α], (-x).down = -x.down
to_additive (attr := simp)]
theorem 
inv_down: ∀ {α : Type u} {x : ULift α} [inst : Inv α], x⁻¹.down = x.down⁻¹
inv_down [
Inv: Type ?u.1394 → Type ?u.1394
Inv 
α: Type u
α] : 
x: ULift α
x⁻¹.
down: {α : Type ?u.1423} → ULift α → α
down = 
x: ULift α
x.
down: {α : Type ?u.1429} → ULift α → α
down⁻¹ :=
  
rfl: ∀ {α : Sort ?u.1441} {a : α}, a = a
rfl
#align ulift.inv_down 
ULift.inv_down: ∀ {α : Type u} {x : ULift α} [inst : Inv α], x⁻¹.down = x.down⁻¹
ULift.inv_down
#align ulift.neg_down 
ULift.neg_down: ∀ {α : Type u} {x : ULift α} [inst : Neg α], (-x).down = -x.down
ULift.neg_down

@[
to_additive: {α : Type u} → {β : Type u_1} → [inst : VAdd α β] → VAdd α (ULift β)
to_additive]
instance 
smul: [inst : SMul α β] → SMul α (ULift β)
smul [
SMul: Type ?u.1495 → Type ?u.1494 → Type (max?u.1495?u.1494)
SMul 
α: Type u
α 
β: Type ?u.1485
β] : 
SMul: Type ?u.1499 → Type ?u.1498 → Type (max?u.1499?u.1498)
SMul 
α: Type u
α (
ULift: Type ?u.1500 → Type (max?u.1500?u.1501)
ULift 
β: Type ?u.1485
β) :=
  ⟨fun 
n: ?m.1514
n 
x: ?m.1517
x => 
up: {α : Type ?u.1519} → α → ULift α
up (
n: ?m.1514
n • 
x: ?m.1517
x.
down: {α : Type ?u.1531} → ULift α → α
down)⟩
#align ulift.has_smul 
ULift.smul: {α : Type u} → {β : Type u_1} → [inst : SMul α β] → SMul α (ULift β)
ULift.smul
#align ulift.has_vadd 
ULift.vadd: {α : Type u} → {β : Type u_1} → [inst : VAdd α β] → VAdd α (ULift β)
ULift.vadd

@[
to_additive: ∀ {α : Type u} {β : Type u_1} [inst : VAdd α β] (a : α) (b : ULift β), (a +ᵥ b).down = a +ᵥ b.down
to_additive (attr := simp)]
theorem 
smul_down: ∀ [inst : SMul α β] (a : α) (b : ULift β), (a • b).down = a • b.down
smul_down [
SMul: Type ?u.1778 → Type ?u.1777 → Type (max?u.1778?u.1777)
SMul 
α: Type u
α 
β: Type ?u.1768
β] (
a: α
a : 
α: Type u
α) (
b: ULift β
b : 
ULift: Type ?u.1783 → Type (max?u.1783v)
ULift.{v} 
β: Type ?u.1768
β) : (
a: α
a • 
b: ULift β
b).
down: {α : Type ?u.1831} → ULift α → α
down = 
a: α
a • 
b: ULift β
b.
down: {α : Type ?u.1842} → ULift α → α
down :=
  
rfl: ∀ {α : Sort ?u.1866} {a : α}, a = a
rfl
#align ulift.smul_down 
ULift.smul_down: ∀ {α : Type u} {β : Type u_1} [inst : SMul α β] (a : α) (b : ULift β), (a • b).down = a • b.down
ULift.smul_down
#align ulift.vadd_down 
ULift.vadd_down: ∀ {α : Type u} {β : Type u_1} [inst : VAdd α β] (a : α) (b : ULift β), (a +ᵥ b).down = a +ᵥ b.down
ULift.vadd_down

@[to_additive existing (reorder := 1 2) 
smul: {α : Type u} → {β : Type u_1} → [inst : SMul α β] → SMul α (ULift β)
smul]
instance 
pow: {α : Type u} → {β : Type u_1} → [inst : Pow α β] → Pow (ULift α) β
pow [
Pow: Type ?u.1944 → Type ?u.1943 → Type (max?u.1944?u.1943)
Pow 
α: Type u
α 
β: Type ?u.1934
β] : 
Pow: Type ?u.1948 → Type ?u.1947 → Type (max?u.1948?u.1947)
Pow (
ULift: Type ?u.1949 → Type (max?u.1949?u.1950)
ULift 
α: Type u
α) 
β: Type ?u.1934
β :=
  ⟨fun 
x: ?m.1963
x 
n: ?m.1966
n => 
up: {α : Type ?u.1968} → α → ULift α
up (
x: ?m.1963
x.
down: {α : Type ?u.1975} → ULift α → α
down ^ 
n: ?m.1966
n)⟩
#align ulift.has_pow 
ULift.pow: {α : Type u} → {β : Type u_1} → [inst : Pow α β] → Pow (ULift α) β
ULift.pow

@[to_additive existing (attr := simp) (reorder := 1 2) 
smul_down: ∀ {α : Type u} {β : Type u_1} [inst : SMul α β] (a : α) (b : ULift β), (a • b).down = a • b.down
smul_down]
theorem 
pow_down: ∀ [inst : Pow α β] (a : ULift α) (b : β), (a ^ b).down = a.down ^ b
pow_down [
Pow: Type ?u.5193 → Type ?u.5192 → Type (max?u.5193?u.5192)
Pow 
α: Type u
α 
β: Type ?u.5183
β] (
a: ULift α
a : 
ULift: Type ?u.5196 → Type (max?u.5196v)
ULift.{v} 
α: Type u
α) (
b: β
b : 
β: Type ?u.5183
β) : (
a: ULift α
a ^ 
b: β
b).
down: {α : Type ?u.8272} → ULift α → α
down = 
a: ULift α
a.
down: {α : Type ?u.8279} → ULift α → α
down ^ 
b: β
b :=
  
rfl: ∀ {α : Sort ?u.11319} {a : α}, a = a
rfl
#align ulift.pow_down 
ULift.pow_down: ∀ {α : Type u} {β : Type u_1} [inst : Pow α β] (a : ULift α) (b : β), (a ^ b).down = a.down ^ b
ULift.pow_down

/-- The multiplicative equivalence between `ULift α` and `α`.
-/
@[
to_additive: {α : Type u} → [inst : Add α] → ULift α ≃+ α
to_additive "The additive equivalence between `ULift α` and `α`."]
def 
_root_.MulEquiv.ulift: [inst : Mul α] → ULift α ≃* α
_root_.MulEquiv.ulift [
Mul: Type ?u.11381 → Type ?u.11381
Mul 
α: Type u
α] : 
ULift: Type ?u.11386 → Type (max?u.11386?u.11387)
ULift 
α: Type u
α ≃* 
α: Type u
α :=
  { 
Equiv.ulift: {α : Type ?u.11415} → ULift α ≃ α
Equiv.ulift with map_mul' := fun 
_: ?m.11495
_ 
_: ?m.11498
_ => 
rfl: ∀ {α : Sort ?u.11500} {a : α}, a = a
rfl }
#align mul_equiv.ulift 
MulEquiv.ulift: {α : Type u} → [inst : Mul α] → ULift α ≃* α
MulEquiv.ulift

-- porting notes: below failed due to error above, manually added
--@[to_additive]
instance 
semigroup: {α : Type u} → [inst : Semigroup α] → Semigroup (ULift α)
semigroup [
Semigroup: Type ?u.11645 → Type ?u.11645
Semigroup 
α: Type u
α] : 
Semigroup: Type ?u.11648 → Type ?u.11648
Semigroup (
ULift: Type ?u.11649 → Type (max?u.11649?u.11650)
ULift 
α: Type u
α) :=
  (
MulEquiv.ulift: {α : Type ?u.11654} → [inst : Mul α] → ULift α ≃* α
MulEquiv.ulift.
injective: ∀ {M : Type ?u.11672} {N : Type ?u.11673} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), Function.Injective ↑e
injective.
semigroup: {M₁ : Type ?u.11723} →
  {M₂ : Type ?u.11722} →
    [inst : Mul M₁] →
      [inst_1 : Semigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → Semigroup M₁
semigroup 
_: ?m.11731 → ?m.11732
_) fun 
_: ?m.11777
_ 
_: ?m.11780
_ => 
rfl: ∀ {α : Sort ?u.11782} {a : α}, a = a
rfl
#align ulift.semigroup 
ULift.semigroup: {α : Type u} → [inst : Semigroup α] → Semigroup (ULift α)
ULift.semigroup

instance 
addSemigroup: [inst : AddSemigroup α] → AddSemigroup (ULift α)
addSemigroup [
AddSemigroup: Type ?u.12234 → Type ?u.12234
AddSemigroup 
α: Type u
α] : 
AddSemigroup: Type ?u.12237 → Type ?u.12237
AddSemigroup (
ULift: Type ?u.12238 → Type (max?u.12238?u.12239)
ULift 
α: Type u
α) :=
  (
Equiv.ulift: {α : Type ?u.12242} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.12246} {β : Sort ?u.12245} (e : α ≃ β), Function.Injective ↑e
injective.
addSemigroup: {M₁ : Type ?u.12252} →
  {M₂ : Type ?u.12251} →
    [inst : Add M₁] →
      [inst_1 : AddSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x + y) = f x + f y) → AddSemigroup M₁
addSemigroup 
_: ?m.12260 → ?m.12261
_) fun 
_: ?m.12300
_ 
_: ?m.12303
_ => 
rfl: ∀ {α : Sort ?u.12305} {a : α}, a = a
rfl
#align ulift.add_semigroup 
ULift.addSemigroup: {α : Type u} → [inst : AddSemigroup α] → AddSemigroup (ULift α)
ULift.addSemigroup


@[
to_additive: {α : Type u} → [inst : AddCommSemigroup α] → AddCommSemigroup (ULift α)
to_additive]
instance 
commSemigroup: {α : Type u} → [inst : CommSemigroup α] → CommSemigroup (ULift α)
commSemigroup [
CommSemigroup: Type ?u.12555 → Type ?u.12555
CommSemigroup 
α: Type u
α] : 
CommSemigroup: Type ?u.12558 → Type ?u.12558
CommSemigroup (
ULift: Type ?u.12559 → Type (max?u.12559?u.12560)
ULift 
α: Type u
α) :=
  (
Equiv.ulift: {α : Type ?u.12563} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.12567} {β : Sort ?u.12566} (e : α ≃ β), Function.Injective ↑e
injective.
commSemigroup: {M₁ : Type ?u.12573} →
  {M₂ : Type ?u.12572} →
    [inst : Mul M₁] →
      [inst_1 : CommSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → CommSemigroup M₁
commSemigroup 
_: ?m.12581 → ?m.12582
_) fun 
_: ?m.12622
_ 
_: ?m.12625
_ => 
rfl: ∀ {α : Sort ?u.12627} {a : α}, a = a
rfl
#align ulift.comm_semigroup 
ULift.commSemigroup: {α : Type u} → [inst : CommSemigroup α] → CommSemigroup (ULift α)
ULift.commSemigroup
#align ulift.add_comm_semigroup 
ULift.addCommSemigroup: {α : Type u} → [inst : AddCommSemigroup α] → AddCommSemigroup (ULift α)
ULift.addCommSemigroup

@[
to_additive: {α : Type u} → [inst : AddZeroClass α] → AddZeroClass (ULift α)
to_additive]
instance 
mulOneClass: [inst : MulOneClass α] → MulOneClass (ULift α)
mulOneClass [
MulOneClass: Type ?u.13026 → Type ?u.13026
MulOneClass 
α: Type u
α] : 
MulOneClass: Type ?u.13029 → Type ?u.13029
MulOneClass (
ULift: Type ?u.13030 → Type (max?u.13030?u.13031)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.13034} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.13038} {β : Sort ?u.13037} (e : α ≃ β), Function.Injective ↑e
injective.
mulOneClass: {M₁ : Type ?u.13044} →
  {M₂ : Type ?u.13043} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : MulOneClass M₂] →
          (f : M₁ → M₂) → Function.Injective f → f 1 = 1 → (∀ (x y : M₁), f (x * y) = f x * f y) → MulOneClass M₁
mulOneClass 
_: ?m.13054 → ?m.13055
_ 
rfl: ∀ {α : Sort ?u.13132} {a : α}, a = a
rfl (by
Goals accomplished! 🐙 
α: Type u

β: Type ?u.13017

x, y: ULift α

inst✝: MulOneClass α

∀ (x y : ULift α), ↑Equiv.ulift (x * y) = ↑Equiv.ulift x * ↑Equiv.ulift yintros
α: Type u

β: Type ?u.13017

x, y: ULift α

inst✝: MulOneClass α

x✝, y✝: ULift α

↑Equiv.ulift (x✝ * y✝) = ↑Equiv.ulift x✝ * ↑Equiv.ulift y✝;
α: Type u

β: Type ?u.13017

x, y: ULift α

inst✝: MulOneClass α

x✝, y✝: ULift α

↑Equiv.ulift (x✝ * y✝) = ↑Equiv.ulift x✝ * ↑Equiv.ulift y✝ 
α: Type u

β: Type ?u.13017

x, y: ULift α

inst✝: MulOneClass α

∀ (x y : ULift α), ↑Equiv.ulift (x * y) = ↑Equiv.ulift x * ↑Equiv.ulift yrfl
Goals accomplished! 🐙)
#align ulift.mul_one_class 
ULift.mulOneClass: {α : Type u} → [inst : MulOneClass α] → MulOneClass (ULift α)
ULift.mulOneClass
#align ulift.add_zero_class 
ULift.addZeroClass: {α : Type u} → [inst : AddZeroClass α] → AddZeroClass (ULift α)
ULift.addZeroClass

instance 
mulZeroOneClass: [inst : MulZeroOneClass α] → MulZeroOneClass (ULift α)
mulZeroOneClass [
MulZeroOneClass: Type ?u.13604 → Type ?u.13604
MulZeroOneClass 
α: Type u
α] : 
MulZeroOneClass: Type ?u.13607 → Type ?u.13607
MulZeroOneClass (
ULift: Type ?u.13608 → Type (max?u.13608?u.13609)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.13612} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.13616} {β : Sort ?u.13615} (e : α ≃ β), Function.Injective ↑e
injective.
mulZeroOneClass: {M₀ : Type ?u.13622} →
  {M₀' : Type ?u.13621} →
    [inst : MulZeroOneClass M₀] →
      [inst_1 : Mul M₀'] →
        [inst_2 : Zero M₀'] →
          [inst_3 : One M₀'] →
            (f : M₀' → M₀) →
              Function.Injective f → f 0 = 0 → f 1 = 1 → (∀ (a b : M₀'), f (a * b) = f a * f b) → MulZeroOneClass M₀'
mulZeroOneClass 
_: ?m.13635 → ?m.13634
_ 
rfl: ∀ {α : Sort ?u.13755} {a : α}, a = a
rfl 
rfl: ∀ {α : Sort ?u.13832} {a : α}, a = a
rfl (by
Goals accomplished! 🐙 
α: Type u

β: Type ?u.13595

x, y: ULift α

inst✝: MulZeroOneClass α

∀ (a b : ULift α), ↑Equiv.ulift (a * b) = ↑Equiv.ulift a * ↑Equiv.ulift bintros
α: Type u

β: Type ?u.13595

x, y: ULift α

inst✝: MulZeroOneClass α

a✝, b✝: ULift α

↑Equiv.ulift (a✝ * b✝) = ↑Equiv.ulift a✝ * ↑Equiv.ulift b✝;
α: Type u

β: Type ?u.13595

x, y: ULift α

inst✝: MulZeroOneClass α

a✝, b✝: ULift α

↑Equiv.ulift (a✝ * b✝) = ↑Equiv.ulift a✝ * ↑Equiv.ulift b✝ 
α: Type u

β: Type ?u.13595

x, y: ULift α

inst✝: MulZeroOneClass α

∀ (a b : ULift α), ↑Equiv.ulift (a * b) = ↑Equiv.ulift a * ↑Equiv.ulift brfl
Goals accomplished! 🐙)
#align ulift.mul_zero_one_class 
ULift.mulZeroOneClass: {α : Type u} → [inst : MulZeroOneClass α] → MulZeroOneClass (ULift α)
ULift.mulZeroOneClass

@[
to_additive: {α : Type u} → [inst : AddMonoid α] → AddMonoid (ULift α)
to_additive]
instance 
monoid: {α : Type u} → [inst : Monoid α] → Monoid (ULift α)
monoid [
Monoid: Type ?u.14158 → Type ?u.14158
Monoid 
α: Type u
α] : 
Monoid: Type ?u.14161 → Type ?u.14161
Monoid (
ULift: Type ?u.14162 → Type (max?u.14162?u.14163)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.14166} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.14170} {β : Sort ?u.14169} (e : α ≃ β), Function.Injective ↑e
injective.
monoid: {M₁ : Type ?u.14176} →
  {M₂ : Type ?u.14175} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Monoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 → (∀ (x y : M₁), f (x * y) = f x * f y) → (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → Monoid M₁
monoid 
_: ?m.14188 → ?m.14189
_ 
rfl: ∀ {α : Sort ?u.14291} {a : α}, a = a
rfl (fun 
_: ?m.14420
_ 
_: ?m.14423
_ => 
rfl: ∀ {α : Sort ?u.14425} {a : α}, a = a
rfl) fun 
_: ?m.14513
_ 
_: ?m.14516
_ => 
rfl: ∀ {α : Sort ?u.14518} {a : α}, a = a
rfl
#align ulift.monoid 
ULift.monoid: {α : Type u} → [inst : Monoid α] → Monoid (ULift α)
ULift.monoid
#align ulift.add_monoid 
ULift.addMonoid: {α : Type u} → [inst : AddMonoid α] → AddMonoid (ULift α)
ULift.addMonoid

@[
to_additive: {α : Type u} → [inst : AddCommMonoid α] → AddCommMonoid (ULift α)
to_additive]
instance 
commMonoid: [inst : CommMonoid α] → CommMonoid (ULift α)
commMonoid [
CommMonoid: Type ?u.14795 → Type ?u.14795
CommMonoid 
α: Type u
α] : 
CommMonoid: Type ?u.14798 → Type ?u.14798
CommMonoid (
ULift: Type ?u.14799 → Type (max?u.14799?u.14800)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.14803} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.14807} {β : Sort ?u.14806} (e : α ≃ β), Function.Injective ↑e
injective.
commMonoid: {M₁ : Type ?u.14813} →
  {M₂ : Type ?u.14812} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : CommMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) → (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → CommMonoid M₁
commMonoid 
_: ?m.14825 → ?m.14826
_ 
rfl: ∀ {α : Sort ?u.14925} {a : α}, a = a
rfl (fun 
_: ?m.15112
_ 
_: ?m.15115
_ => 
rfl: ∀ {α : Sort ?u.15117} {a : α}, a = a
rfl) fun 
_: ?m.15256
_ 
_: ?m.15259
_ => 
rfl: ∀ {α : Sort ?u.15261} {a : α}, a = a
rfl
#align ulift.comm_monoid 
ULift.commMonoid: {α : Type u} → [inst : CommMonoid α] → CommMonoid (ULift α)
ULift.commMonoid
#align ulift.add_comm_monoid 
ULift.addCommMonoid: {α : Type u} → [inst : AddCommMonoid α] → AddCommMonoid (ULift α)
ULift.addCommMonoid

instance 
natCast: [inst : NatCast α] → NatCast (ULift α)
natCast [
NatCast: Type ?u.15600 → Type ?u.15600
NatCast 
α: Type u
α] : 
NatCast: Type ?u.15603 → Type ?u.15603
NatCast (
ULift: Type ?u.15604 → Type (max?u.15604?u.15605)
ULift 
α: Type u
α) := ⟨λ 
a: ?m.15614
a ↦ 
up: {α : Type ?u.15616} → α → ULift α
up 
a: ?m.15614
a⟩
#align ulift.has_nat_cast 
ULift.natCast: {α : Type u} → [inst : NatCast α] → NatCast (ULift α)
ULift.natCast
instance 
intCast: [inst : IntCast α] → IntCast (ULift α)
intCast [
IntCast: Type ?u.15711 → Type ?u.15711
IntCast 
α: Type u
α] : 
IntCast: Type ?u.15714 → Type ?u.15714
IntCast (
ULift: Type ?u.15715 → Type (max?u.15715?u.15716)
ULift 
α: Type u
α) := ⟨λ 
a: ?m.15725
a ↦ 
up: {α : Type ?u.15727} → α → ULift α
up 
a: ?m.15725
a⟩
#align ulift.has_int_cast 
ULift.intCast: {α : Type u} → [inst : IntCast α] → IntCast (ULift α)
ULift.intCast

@[simp, norm_cast]
theorem 
up_natCast: ∀ {α : Type u} [inst : NatCast α] (n : ℕ), { down := ↑n } = ↑n
up_natCast [
NatCast: Type ?u.15822 → Type ?u.15822
NatCast 
α: Type u
α] (
n: ℕ
n : 
ℕ: Type
ℕ) : 
up: {α : Type ?u.15828} → α → ULift α
up (
n: ℕ
n : 
α: Type u
α) = 
n: ℕ
n :=
  
rfl: ∀ {α : Sort ?u.15955} {a : α}, a = a
rfl
#align ulift.up_nat_cast 
ULift.up_natCast: ∀ {α : Type u} [inst : NatCast α] (n : ℕ), { down := ↑n } = ↑n
ULift.up_natCast

@[simp, norm_cast]
theorem 
up_intCast: ∀ {α : Type u} [inst : IntCast α] (n : ℤ), { down := ↑n } = ↑n
up_intCast [
IntCast: Type ?u.16013 → Type ?u.16013
IntCast 
α: Type u
α] (
n: ℤ
n : 
ℤ: Type
ℤ) : 
up: {α : Type ?u.16019} → α → ULift α
up (
n: ℤ
n : 
α: Type u
α) = 
n: ℤ
n :=
  
rfl: ∀ {α : Sort ?u.16146} {a : α}, a = a
rfl
#align ulift.up_int_cast 
ULift.up_intCast: ∀ {α : Type u} [inst : IntCast α] (n : ℤ), { down := ↑n } = ↑n
ULift.up_intCast

@[simp, norm_cast]
theorem 
down_natCast: ∀ {α : Type u} [inst : NatCast α] (n : ℕ), (↑n).down = ↑n
down_natCast [
NatCast: Type ?u.16204 → Type ?u.16204
NatCast 
α: Type u
α] (
n: ℕ
n : 
ℕ: Type
ℕ) : 
down: {α : Type ?u.16210} → ULift α → α
down (
n: ℕ
n : 
ULift: Type ?u.16214 → Type (max?u.16214?u.16215)
ULift 
α: Type u
α) = 
n: ℕ
n :=
  
rfl: ∀ {α : Sort ?u.16334} {a : α}, a = a
rfl
#align ulift.down_nat_cast 
ULift.down_natCast: ∀ {α : Type u} [inst : NatCast α] (n : ℕ), (↑n).down = ↑n
ULift.down_natCast

@[simp, norm_cast]
theorem 
down_intCast: ∀ {α : Type u} [inst : IntCast α] (n : ℤ), (↑n).down = ↑n
down_intCast [
IntCast: Type ?u.16390 → Type ?u.16390
IntCast 
α: Type u
α] (
n: ℤ
n : 
ℤ: Type
ℤ) : 
down: {α : Type ?u.16396} → ULift α → α
down (
n: ℤ
n : 
ULift: Type ?u.16400 → Type (max?u.16400?u.16401)
ULift 
α: Type u
α) = 
n: ℤ
n :=
  
rfl: ∀ {α : Sort ?u.16520} {a : α}, a = a
rfl
#align ulift.down_int_cast 
ULift.down_intCast: ∀ {α : Type u} [inst : IntCast α] (n : ℤ), (↑n).down = ↑n
ULift.down_intCast

instance 
addMonoidWithOne: {α : Type u} → [inst : AddMonoidWithOne α] → AddMonoidWithOne (ULift α)
addMonoidWithOne [
AddMonoidWithOne: Type ?u.16576 → Type ?u.16576
AddMonoidWithOne 
α: Type u
α] : 
AddMonoidWithOne: Type ?u.16579 → Type ?u.16579
AddMonoidWithOne (
ULift: Type ?u.16580 → Type (max?u.16580?u.16581)
ULift 
α: Type u
α) :=
  { 
ULift.one: {α : Type ?u.16587} → [inst : One α] → One (ULift α)
ULift.one, 
ULift.addMonoid: {α : Type ?u.16641} → [inst : AddMonoid α] → AddMonoid (ULift α)
ULift.addMonoid with
      natCast := fun 
n: ?m.16673
n => ⟨
n: ?m.16673
n⟩
      natCast_zero := 
congr_arg: ∀ {α : Sort ?u.16784} {β : Sort ?u.16783} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
ULift.up: {α : Type ?u.16789} → α → ULift α
ULift.up 
Nat.cast_zero: ∀ {R : Type ?u.16803} [inst : AddMonoidWithOne R], ↑0 = 0
Nat.cast_zero,
      natCast_succ := fun 
_: ?m.16842
_ => 
congr_arg: ∀ {α : Sort ?u.16845} {β : Sort ?u.16844} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
ULift.up: {α : Type ?u.16850} → α → ULift α
ULift.up (
Nat.cast_succ: ∀ {R : Type ?u.16859} [inst : AddMonoidWithOne R] (n : ℕ), ↑(Nat.succ n) = ↑n + 1
Nat.cast_succ 
_: ℕ
_) }
#align ulift.add_monoid_with_one 
ULift.addMonoidWithOne: {α : Type u} → [inst : AddMonoidWithOne α] → AddMonoidWithOne (ULift α)
ULift.addMonoidWithOne

instance 
addCommMonoidWithOne: [inst : AddCommMonoidWithOne α] → AddCommMonoidWithOne (ULift α)
addCommMonoidWithOne [
AddCommMonoidWithOne: Type ?u.17024 → Type ?u.17024
AddCommMonoidWithOne 
α: Type u
α] : 
AddCommMonoidWithOne: Type ?u.17027 → Type ?u.17027
AddCommMonoidWithOne (
ULift: Type ?u.17028 → Type (max?u.17028?u.17029)
ULift 
α: Type u
α) :=
  
{ ULift.addMonoidWithOne, ULift.addCommMonoid with }: AddCommMonoidWithOne ?m.17081
{ 
ULift.addMonoidWithOne: {α : Type ?u.17035} → [inst : AddMonoidWithOne α] → AddMonoidWithOne (ULift α)
ULift.addMonoidWithOne
{ ULift.addMonoidWithOne, ULift.addCommMonoid with }: AddCommMonoidWithOne ?m.17081
, 
ULift.addCommMonoid: {α : Type ?u.17057} → [inst : AddCommMonoid α] → AddCommMonoid (ULift α)
ULift.addCommMonoid
{ ULift.addMonoidWithOne, ULift.addCommMonoid with }: AddCommMonoidWithOne ?m.17081
 
{ ULift.addMonoidWithOne, ULift.addCommMonoid with }: AddCommMonoidWithOne ?m.17081
with
{ ULift.addMonoidWithOne, ULift.addCommMonoid with }: AddCommMonoidWithOne ?m.17081
 }
#align ulift.add_comm_monoid_with_one 
ULift.addCommMonoidWithOne: {α : Type u} → [inst : AddCommMonoidWithOne α] → AddCommMonoidWithOne (ULift α)
ULift.addCommMonoidWithOne

instance 
monoidWithZero: [inst : MonoidWithZero α] → MonoidWithZero (ULift α)
monoidWithZero [
MonoidWithZero: Type ?u.17247 → Type ?u.17247
MonoidWithZero 
α: Type u
α] : 
MonoidWithZero: Type ?u.17250 → Type ?u.17250
MonoidWithZero (
ULift: Type ?u.17251 → Type (max?u.17251?u.17252)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.17255} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.17259} {β : Sort ?u.17258} (e : α ≃ β), Function.Injective ↑e
injective.
monoidWithZero: {M₀ : Type ?u.17265} →
  {M₀' : Type ?u.17264} →
    [inst : Zero M₀'] →
      [inst_1 : Mul M₀'] →
        [inst_2 : One M₀'] →
          [inst_3 : Pow M₀' ℕ] →
            [inst_4 : MonoidWithZero M₀] →
              (f : M₀' → M₀) →
                Function.Injective f →
                  f 0 = 0 →
                    f 1 = 1 →
                      (∀ (x y : M₀'), f (x * y) = f x * f y) →
                        (∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n) → MonoidWithZero M₀'
monoidWithZero 
_: ?m.17280 → ?m.17279
_ 
rfl: ∀ {α : Sort ?u.17422} {a : α}, a = a
rfl 
rfl: ∀ {α : Sort ?u.17480} {a : α}, a = a
rfl (fun 
_: ?m.17604
_ 
_: ?m.17607
_ => 
rfl: ∀ {α : Sort ?u.17609} {a : α}, a = a
rfl) fun 
_: ?m.17649
_ 
_: ?m.17652
_ => 
rfl: ∀ {α : Sort ?u.17654} {a : α}, a = a
rfl
#align ulift.monoid_with_zero 
ULift.monoidWithZero: {α : Type u} → [inst : MonoidWithZero α] → MonoidWithZero (ULift α)
ULift.monoidWithZero

instance 
commMonoidWithZero: [inst : CommMonoidWithZero α] → CommMonoidWithZero (ULift α)
commMonoidWithZero [
CommMonoidWithZero: Type ?u.17798 → Type ?u.17798
CommMonoidWithZero 
α: Type u
α] : 
CommMonoidWithZero: Type ?u.17801 → Type ?u.17801
CommMonoidWithZero (
ULift: Type ?u.17802 → Type (max?u.17802?u.17803)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.17806} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.17810} {β : Sort ?u.17809} (e : α ≃ β), Function.Injective ↑e
injective.
commMonoidWithZero: {M₀ : Type ?u.17816} →
  {M₀' : Type ?u.17815} →
    [inst : Zero M₀'] →
      [inst_1 : Mul M₀'] →
        [inst_2 : One M₀'] →
          [inst_3 : Pow M₀' ℕ] →
            [inst_4 : CommMonoidWithZero M₀] →
              (f : M₀' → M₀) →
                Function.Injective f →
                  f 0 = 0 →
                    f 1 = 1 →
                      (∀ (x y : M₀'), f (x * y) = f x * f y) →
                        (∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n) → CommMonoidWithZero M₀'
commMonoidWithZero 
_: ?m.17831 → ?m.17830
_ 
rfl: ∀ {α : Sort ?u.17972} {a : α}, a = a
rfl 
rfl: ∀ {α : Sort ?u.18018} {a : α}, a = a
rfl (fun 
_: ?m.18155
_ 
_: ?m.18158
_ => 
rfl: ∀ {α : Sort ?u.18160} {a : α}, a = a
rfl) fun 
_: ?m.18209
_ 
_: ?m.18212
_ => 
rfl: ∀ {α : Sort ?u.18214} {a : α}, a = a
rfl
#align ulift.comm_monoid_with_zero 
ULift.commMonoidWithZero: {α : Type u} → [inst : CommMonoidWithZero α] → CommMonoidWithZero (ULift α)
ULift.commMonoidWithZero

@[
to_additive: {α : Type u} → [inst : SubNegMonoid α] → SubNegMonoid (ULift α)
to_additive]
instance 
divInvMonoid: {α : Type u} → [inst : DivInvMonoid α] → DivInvMonoid (ULift α)
divInvMonoid [
DivInvMonoid: Type ?u.18368 → Type ?u.18368
DivInvMonoid 
α: Type u
α] : 
DivInvMonoid: Type ?u.18371 → Type ?u.18371
DivInvMonoid (
ULift: Type ?u.18372 → Type (max?u.18372?u.18373)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.18376} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.18380} {β : Sort ?u.18379} (e : α ≃ β), Function.Injective ↑e
injective.
divInvMonoid: {M₁ : Type ?u.18386} →
  {M₂ : Type ?u.18385} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Inv M₁] →
            [inst_4 : Div M₁] →
              [inst_5 : Pow M₁ ℤ] →
                [inst_6 : DivInvMonoid M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → DivInvMonoid M₁
divInvMonoid 
_: ?m.18404 → ?m.18405
_ 
rfl: ∀ {α : Sort ?u.18569} {a : α}, a = a
rfl (fun 
_: ?m.18736
_ 
_: ?m.18739
_ => 
rfl: ∀ {α : Sort ?u.18741} {a : α}, a = a
rfl) (fun 
_: ?m.18829
_ => 
rfl: ∀ {α : Sort ?u.18831} {a : α}, a = a
rfl) (fun 
_: ?m.18889
_ 
_: ?m.18892
_ => 
rfl: ∀ {α : Sort ?u.18894} {a : α}, a = a
rfl)
    (fun 
_: ?m.18931
_ 
_: ?m.18934
_ => 
rfl: ∀ {α : Sort ?u.18936} {a : α}, a = a
rfl) fun 
_: ?m.18997
_ 
_: ?m.19000
_ => 
rfl: ∀ {α : Sort ?u.19002} {a : α}, a = a
rfl
#align ulift.div_inv_monoid 
ULift.divInvMonoid: {α : Type u} → [inst : DivInvMonoid α] → DivInvMonoid (ULift α)
ULift.divInvMonoid
#align ulift.sub_neg_add_monoid 
ULift.subNegAddMonoid: {α : Type u} → [inst : SubNegMonoid α] → SubNegMonoid (ULift α)
ULift.subNegAddMonoid

@[
to_additive: {α : Type u} → [inst : AddGroup α] → AddGroup (ULift α)
to_additive]
instance 
group: [inst : Group α] → Group (ULift α)
group [
Group: Type ?u.19357 → Type ?u.19357
Group 
α: Type u
α] : 
Group: Type ?u.19360 → Type ?u.19360
Group (
ULift: Type ?u.19361 → Type (max?u.19361?u.19362)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.19365} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.19369} {β : Sort ?u.19368} (e : α ≃ β), Function.Injective ↑e
injective.
group: {M₁ : Type ?u.19375} →
  {M₂ : Type ?u.19374} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Inv M₁] →
            [inst_4 : Div M₁] →
              [inst_5 : Pow M₁ ℤ] →
                [inst_6 : Group M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → Group M₁
group 
_: ?m.19393 → ?m.19394
_ 
rfl: ∀ {α : Sort ?u.19555} {a : α}, a = a
rfl (fun 
_: ?m.19639
_ 
_: ?m.19642
_ => 
rfl: ∀ {α : Sort ?u.19644} {a : α}, a = a
rfl) (fun 
_: ?m.19749
_ => 
rfl: ∀ {α : Sort ?u.19751} {a : α}, a = a
rfl) (fun 
_: ?m.19801
_ 
_: ?m.19804
_ => 
rfl: ∀ {α : Sort ?u.19806} {a : α}, a = a
rfl)
    (fun 
_: ?m.19848
_ 
_: ?m.19851
_ => 
rfl: ∀ {α : Sort ?u.19853} {a : α}, a = a
rfl) fun 
_: ?m.19919
_ 
_: ?m.19922
_ => 
rfl: ∀ {α : Sort ?u.19924} {a : α}, a = a
rfl
#align ulift.group 
ULift.group: {α : Type u} → [inst : Group α] → Group (ULift α)
ULift.group
#align ulift.add_group 
ULift.addGroup: {α : Type u} → [inst : AddGroup α] → AddGroup (ULift α)
ULift.addGroup

@[
to_additive: {α : Type u} → [inst : AddCommGroup α] → AddCommGroup (ULift α)
to_additive]
instance 
commGroup: {α : Type u} → [inst : CommGroup α] → CommGroup (ULift α)
commGroup [
CommGroup: Type ?u.20273 → Type ?u.20273
CommGroup 
α: Type u
α] : 
CommGroup: Type ?u.20276 → Type ?u.20276
CommGroup (
ULift: Type ?u.20277 → Type (max?u.20277?u.20278)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.20281} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.20285} {β : Sort ?u.20284} (e : α ≃ β), Function.Injective ↑e
injective.
commGroup: {M₁ : Type ?u.20291} →
  {M₂ : Type ?u.20290} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Inv M₁] →
            [inst_4 : Div M₁] →
              [inst_5 : Pow M₁ ℤ] →
                [inst_6 : CommGroup M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → CommGroup M₁
commGroup 
_: ?m.20309 → ?m.20310
_ 
rfl: ∀ {α : Sort ?u.20470} {a : α}, a = a
rfl (fun 
_: ?m.20550
_ 
_: ?m.20553
_ => 
rfl: ∀ {α : Sort ?u.20555} {a : α}, a = a
rfl) (fun 
_: ?m.20664
_ => 
rfl: ∀ {α : Sort ?u.20666} {a : α}, a = a
rfl) (fun 
_: ?m.20713
_ 
_: ?m.20716
_ => 
rfl: ∀ {α : Sort ?u.20718} {a : α}, a = a
rfl)
    (fun 
_: ?m.20762
_ 
_: ?m.20765
_ => 
rfl: ∀ {α : Sort ?u.20767} {a : α}, a = a
rfl) fun 
_: ?m.20835
_ 
_: ?m.20838
_ => 
rfl: ∀ {α : Sort ?u.20840} {a : α}, a = a
rfl
#align ulift.comm_group 
ULift.commGroup: {α : Type u} → [inst : CommGroup α] → CommGroup (ULift α)
ULift.commGroup
#align ulift.add_comm_group 
ULift.addCommGroup: {α : Type u} → [inst : AddCommGroup α] → AddCommGroup (ULift α)
ULift.addCommGroup

instance 
addGroupWithOne: [inst : AddGroupWithOne α] → AddGroupWithOne (ULift α)
addGroupWithOne [
AddGroupWithOne: Type ?u.21193 → Type ?u.21193
AddGroupWithOne 
α: Type u
α] : 
AddGroupWithOne: Type ?u.21196 → Type ?u.21196
AddGroupWithOne (
ULift: Type ?u.21197 → Type (max?u.21197?u.21198)
ULift 
α: Type u
α) :=
  { 
ULift.addMonoidWithOne: {α : Type ?u.21204} → [inst : AddMonoidWithOne α] → AddMonoidWithOne (ULift α)
ULift.addMonoidWithOne, 
ULift.addGroup: {α : Type ?u.21226} → [inst : AddGroup α] → AddGroup (ULift α)
ULift.addGroup with
      intCast := fun 
n: ?m.21252
n => ⟨
n: ?m.21252
n⟩,
      intCast_ofNat := fun 
_: ?m.21440
_ => 
congr_arg: ∀ {α : Sort ?u.21443} {β : Sort ?u.21442} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
ULift.up: {α : Type ?u.21448} → α → ULift α
ULift.up (
Int.cast_ofNat: ∀ {R : Type ?u.21457} [inst : AddGroupWithOne R] (n : ℕ), ↑↑n = ↑n
Int.cast_ofNat 
_: ℕ
_),
      intCast_negSucc := fun 
_: ?m.21487
_ => 
congr_arg: ∀ {α : Sort ?u.21490} {β : Sort ?u.21489} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
ULift.up: {α : Type ?u.21495} → α → ULift α
ULift.up (
Int.cast_negSucc: ∀ {R : Type ?u.21504} [inst : AddGroupWithOne R] (n : ℕ), ↑(Int.negSucc n) = -↑(n + 1)
Int.cast_negSucc 
_: ℕ
_) }
#align ulift.add_group_with_one 
ULift.addGroupWithOne: {α : Type u} → [inst : AddGroupWithOne α] → AddGroupWithOne (ULift α)
ULift.addGroupWithOne

instance 
addCommGroupWithOne: [inst : AddCommGroupWithOne α] → AddCommGroupWithOne (ULift α)
addCommGroupWithOne [
AddCommGroupWithOne: Type ?u.21686 → Type ?u.21686
AddCommGroupWithOne 
α: Type u
α] : 
AddCommGroupWithOne: Type ?u.21689 → Type ?u.21689
AddCommGroupWithOne (
ULift: Type ?u.21690 → Type (max?u.21690?u.21691)
ULift 
α: Type u
α) :=
  
{ ULift.addGroupWithOne, ULift.addCommGroup with }: AddCommGroupWithOne ?m.21735
{ 
ULift.addGroupWithOne: {α : Type ?u.21697} → [inst : AddGroupWithOne α] → AddGroupWithOne (ULift α)
ULift.addGroupWithOne
{ ULift.addGroupWithOne, ULift.addCommGroup with }: AddCommGroupWithOne ?m.21735
, 
ULift.addCommGroup: {α : Type ?u.21717} → [inst : AddCommGroup α] → AddCommGroup (ULift α)
ULift.addCommGroup
{ ULift.addGroupWithOne, ULift.addCommGroup with }: AddCommGroupWithOne ?m.21735
 
{ ULift.addGroupWithOne, ULift.addCommGroup with }: AddCommGroupWithOne ?m.21735
with
{ ULift.addGroupWithOne, ULift.addCommGroup with }: AddCommGroupWithOne ?m.21735
 }
#align ulift.add_comm_group_with_one 
ULift.addCommGroupWithOne: {α : Type u} → [inst : AddCommGroupWithOne α] → AddCommGroupWithOne (ULift α)
ULift.addCommGroupWithOne

instance 
groupWithZero: {α : Type u} → [inst : GroupWithZero α] → GroupWithZero (ULift α)
groupWithZero [
GroupWithZero: Type ?u.21931 → Type ?u.21931
GroupWithZero 
α: Type u
α] : 
GroupWithZero: Type ?u.21934 → Type ?u.21934
GroupWithZero (
ULift: Type ?u.21935 → Type (max?u.21935?u.21936)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.21939} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.21943} {β : Sort ?u.21942} (e : α ≃ β), Function.Injective ↑e
injective.
groupWithZero: {G₀ : Type ?u.21949} →
  {G₀' : Type ?u.21948} →
    [inst : GroupWithZero G₀] →
      [inst_1 : Zero G₀'] →
        [inst_2 : Mul G₀'] →
          [inst_3 : One G₀'] →
            [inst_4 : Inv G₀'] →
              [inst_5 : Div G₀'] →
                [inst_6 : Pow G₀' ℕ] →
                  [inst_7 : Pow G₀' ℤ] →
                    (f : G₀' → G₀) →
                      Function.Injective f →
                        f 0 = 0 →
                          f 1 = 1 →
                            (∀ (x y : G₀'), f (x * y) = f x * f y) →
                              (∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) →
                                (∀ (x y : G₀'), f (x / y) = f x / f y) →
                                  (∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n) →
                                    (∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n) → GroupWithZero G₀'
groupWithZero 
_: ?m.21970 → ?m.21969
_ 
rfl: ∀ {α : Sort ?u.22175} {a : α}, a = a
rfl 
rfl: ∀ {α : Sort ?u.22236} {a : α}, a = a
rfl (fun 
_: ?m.22363
_ 
_: ?m.22366
_ => 
rfl: ∀ {α : Sort ?u.22368} {a : α}, a = a
rfl) (fun 
_: ?m.22411
_ => 
rfl: ∀ {α : Sort ?u.22413} {a : α}, a = a
rfl) (fun 
_: ?m.22443
_ 
_: ?m.22446
_ => 
rfl: ∀ {α : Sort ?u.22448} {a : α}, a = a
rfl)
    (fun 
_: ?m.22477
_ 
_: ?m.22480
_ => 
rfl: ∀ {α : Sort ?u.22482} {a : α}, a = a
rfl) fun 
_: ?m.22522
_ 
_: ?m.22525
_ => 
rfl: ∀ {α : Sort ?u.22527} {a : α}, a = a
rfl
#align ulift.group_with_zero 
ULift.groupWithZero: {α : Type u} → [inst : GroupWithZero α] → GroupWithZero (ULift α)
ULift.groupWithZero

instance 
commGroupWithZero: {α : Type u} → [inst : CommGroupWithZero α] → CommGroupWithZero (ULift α)
commGroupWithZero [
CommGroupWithZero: Type ?u.22704 → Type ?u.22704
CommGroupWithZero 
α: Type u
α] : 
CommGroupWithZero: Type ?u.22707 → Type ?u.22707
CommGroupWithZero (
ULift: Type ?u.22708 → Type (max?u.22708?u.22709)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.22712} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.22716} {β : Sort ?u.22715} (e : α ≃ β), Function.Injective ↑e
injective.
commGroupWithZero: {G₀ : Type ?u.22722} →
  {G₀' : Type ?u.22721} →
    [inst : CommGroupWithZero G₀] →
      [inst_1 : Zero G₀'] →
        [inst_2 : Mul G₀'] →
          [inst_3 : One G₀'] →
            [inst_4 : Inv G₀'] →
              [inst_5 : Div G₀'] →
                [inst_6 : Pow G₀' ℕ] →
                  [inst_7 : Pow G₀' ℤ] →
                    (f : G₀' → G₀) →
                      Function.Injective f →
                        f 0 = 0 →
                          f 1 = 1 →
                            (∀ (x y : G₀'), f (x * y) = f x * f y) →
                              (∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) →
                                (∀ (x y : G₀'), f (x / y) = f x / f y) →
                                  (∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n) →
                                    (∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n) → CommGroupWithZero G₀'
commGroupWithZero 
_: ?m.22743 → ?m.22742
_ 
rfl: ∀ {α : Sort ?u.22947} {a : α}, a = a
rfl 
rfl: ∀ {α : Sort ?u.22995} {a : α}, a = a
rfl (fun 
_: ?m.23128
_ 
_: ?m.23131
_ => 
rfl: ∀ {α : Sort ?u.23133} {a : α}, a = a
rfl) (fun 
_: ?m.23178
_ => 
rfl: ∀ {α : Sort ?u.23180} {a : α}, a = a
rfl) (fun 
_: ?m.23207
_ 
_: ?m.23210
_ => 
rfl: ∀ {α : Sort ?u.23212} {a : α}, a = a
rfl)
    (fun 
_: ?m.23238
_ 
_: ?m.23241
_ => 
rfl: ∀ {α : Sort ?u.23243} {a : α}, a = a
rfl) fun 
_: ?m.23285
_ 
_: ?m.23288
_ => 
rfl: ∀ {α : Sort ?u.23290} {a : α}, a = a
rfl
#align ulift.comm_group_with_zero 
ULift.commGroupWithZero: {α : Type u} → [inst : CommGroupWithZero α] → CommGroupWithZero (ULift α)
ULift.commGroupWithZero

@[
to_additive: {α : Type u} → [inst : AddLeftCancelSemigroup α] → AddLeftCancelSemigroup (ULift α)
to_additive]
instance 
leftCancelSemigroup: {α : Type u} → [inst : LeftCancelSemigroup α] → LeftCancelSemigroup (ULift α)
leftCancelSemigroup [
LeftCancelSemigroup: Type ?u.23471 → Type ?u.23471
LeftCancelSemigroup 
α: Type u
α] : 
LeftCancelSemigroup: Type ?u.23474 → Type ?u.23474
LeftCancelSemigroup (
ULift: Type ?u.23475 → Type (max?u.23475?u.23476)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.23479} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.23483} {β : Sort ?u.23482} (e : α ≃ β), Function.Injective ↑e
injective.
leftCancelSemigroup: {M₁ : Type ?u.23489} →
  {M₂ : Type ?u.23488} →
    [inst : Mul M₁] →
      [inst_1 : LeftCancelSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → LeftCancelSemigroup M₁
leftCancelSemigroup 
_: ?m.23497 → ?m.23498
_ fun 
_: ?m.23537
_ 
_: ?m.23540
_ => 
rfl: ∀ {α : Sort ?u.23542} {a : α}, a = a
rfl
#align ulift.left_cancel_semigroup 
ULift.leftCancelSemigroup: {α : Type u} → [inst : LeftCancelSemigroup α] → LeftCancelSemigroup (ULift α)
ULift.leftCancelSemigroup
#align ulift.add_left_cancel_semigroup 
ULift.addLeftCancelSemigroup: {α : Type u} → [inst : AddLeftCancelSemigroup α] → AddLeftCancelSemigroup (ULift α)
ULift.addLeftCancelSemigroup

@[
to_additive: {α : Type u} → [inst : AddRightCancelSemigroup α] → AddRightCancelSemigroup (ULift α)
to_additive]
instance 
rightCancelSemigroup: [inst : RightCancelSemigroup α] → RightCancelSemigroup (ULift α)
rightCancelSemigroup [
RightCancelSemigroup: Type ?u.23933 → Type ?u.23933
RightCancelSemigroup 
α: Type u
α] : 
RightCancelSemigroup: Type ?u.23936 → Type ?u.23936
RightCancelSemigroup (
ULift: Type ?u.23937 → Type (max?u.23937?u.23938)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.23941} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.23945} {β : Sort ?u.23944} (e : α ≃ β), Function.Injective ↑e
injective.
rightCancelSemigroup: {M₁ : Type ?u.23951} →
  {M₂ : Type ?u.23950} →
    [inst : Mul M₁] →
      [inst_1 : RightCancelSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → RightCancelSemigroup M₁
rightCancelSemigroup 
_: ?m.23959 → ?m.23960
_ fun 
_: ?m.23999
_ 
_: ?m.24002
_ => 
rfl: ∀ {α : Sort ?u.24004} {a : α}, a = a
rfl
#align ulift.right_cancel_semigroup 
ULift.rightCancelSemigroup: {α : Type u} → [inst : RightCancelSemigroup α] → RightCancelSemigroup (ULift α)
ULift.rightCancelSemigroup
#align ulift.add_right_cancel_semigroup 
ULift.addRightCancelSemigroup: {α : Type u} → [inst : AddRightCancelSemigroup α] → AddRightCancelSemigroup (ULift α)
ULift.addRightCancelSemigroup

@[
to_additive: {α : Type u} → [inst : AddLeftCancelMonoid α] → AddLeftCancelMonoid (ULift α)
to_additive]
instance 
leftCancelMonoid: [inst : LeftCancelMonoid α] → LeftCancelMonoid (ULift α)
leftCancelMonoid [
LeftCancelMonoid: Type ?u.24388 → Type ?u.24388
LeftCancelMonoid 
α: Type u
α] : 
LeftCancelMonoid: Type ?u.24391 → Type ?u.24391
LeftCancelMonoid (
ULift: Type ?u.24392 → Type (max?u.24392?u.24393)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.24396} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.24400} {β : Sort ?u.24399} (e : α ≃ β), Function.Injective ↑e
injective.
leftCancelMonoid: {M₁ : Type ?u.24406} →
  {M₂ : Type ?u.24405} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : LeftCancelMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) →
                    (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → LeftCancelMonoid M₁
leftCancelMonoid 
_: ?m.24418 → ?m.24419
_ 
rfl: ∀ {α : Sort ?u.24516} {a : α}, a = a
rfl (fun 
_: ?m.24629
_ 
_: ?m.24632
_ => 
rfl: ∀ {α : Sort ?u.24634} {a : α}, a = a
rfl) fun 
_: ?m.24775
_ 
_: ?m.24778
_ => 
rfl: ∀ {α : Sort ?u.24780} {a : α}, a = a
rfl
#align ulift.left_cancel_monoid 
ULift.leftCancelMonoid: {α : Type u} → [inst : LeftCancelMonoid α] → LeftCancelMonoid (ULift α)
ULift.leftCancelMonoid
#align ulift.add_left_cancel_monoid 
ULift.addLeftCancelMonoid: {α : Type u} → [inst : AddLeftCancelMonoid α] → AddLeftCancelMonoid (ULift α)
ULift.addLeftCancelMonoid

@[
to_additive: {α : Type u} → [inst : AddRightCancelMonoid α] → AddRightCancelMonoid (ULift α)
to_additive]
instance 
rightCancelMonoid: {α : Type u} → [inst : RightCancelMonoid α] → RightCancelMonoid (ULift α)
rightCancelMonoid [
RightCancelMonoid: Type ?u.25129 → Type ?u.25129
RightCancelMonoid 
α: Type u
α] : 
RightCancelMonoid: Type ?u.25132 → Type ?u.25132
RightCancelMonoid (
ULift: Type ?u.25133 → Type (max?u.25133?u.25134)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.25137} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.25141} {β : Sort ?u.25140} (e : α ≃ β), Function.Injective ↑e
injective.
rightCancelMonoid: {M₁ : Type ?u.25147} →
  {M₂ : Type ?u.25146} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : RightCancelMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) →
                    (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → RightCancelMonoid M₁
rightCancelMonoid 
_: ?m.25159 → ?m.25160
_ 
rfl: ∀ {α : Sort ?u.25256} {a : α}, a = a
rfl (fun 
_: ?m.25347
_ 
_: ?m.25350
_ => 
rfl: ∀ {α : Sort ?u.25352} {a : α}, a = a
rfl) fun 
_: ?m.25478
_ 
_: ?m.25481
_ => 
rfl: ∀ {α : Sort ?u.25483} {a : α}, a = a
rfl
#align ulift.right_cancel_monoid 
ULift.rightCancelMonoid: {α : Type u} → [inst : RightCancelMonoid α] → RightCancelMonoid (ULift α)
ULift.rightCancelMonoid
#align ulift.add_right_cancel_monoid 
ULift.addRightCancelMonoid: {α : Type u} → [inst : AddRightCancelMonoid α] → AddRightCancelMonoid (ULift α)
ULift.addRightCancelMonoid

@[
to_additive: {α : Type u} → [inst : AddCancelMonoid α] → AddCancelMonoid (ULift α)
to_additive]
instance 
cancelMonoid: [inst : CancelMonoid α] → CancelMonoid (ULift α)
cancelMonoid [
CancelMonoid: Type ?u.25817 → Type ?u.25817
CancelMonoid 
α: Type u
α] : 
CancelMonoid: Type ?u.25820 → Type ?u.25820
CancelMonoid (
ULift: Type ?u.25821 → Type (max?u.25821?u.25822)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.25825} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.25829} {β : Sort ?u.25828} (e : α ≃ β), Function.Injective ↑e
injective.
cancelMonoid: {M₁ : Type ?u.25835} →
  {M₂ : Type ?u.25834} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : CancelMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) → (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → CancelMonoid M₁
cancelMonoid 
_: ?m.25847 → ?m.25848
_ 
rfl: ∀ {α : Sort ?u.25945} {a : α}, a = a
rfl (fun 
_: ?m.26043
_ 
_: ?m.26046
_ => 
rfl: ∀ {α : Sort ?u.26048} {a : α}, a = a
rfl) fun 
_: ?m.26178
_ 
_: ?m.26181
_ => 
rfl: ∀ {α : Sort ?u.26183} {a : α}, a = a
rfl
#align ulift.cancel_monoid 
ULift.cancelMonoid: {α : Type u} → [inst : CancelMonoid α] → CancelMonoid (ULift α)
ULift.cancelMonoid
#align ulift.add_cancel_monoid 
ULift.addCancelMonoid: {α : Type u} → [inst : AddCancelMonoid α] → AddCancelMonoid (ULift α)
ULift.addCancelMonoid

@[
to_additive: {α : Type u} → [inst : AddCancelCommMonoid α] → AddCancelCommMonoid (ULift α)
to_additive]
instance 
cancelCommMonoid: {α : Type u} → [inst : CancelCommMonoid α] → CancelCommMonoid (ULift α)
cancelCommMonoid [
CancelCommMonoid: Type ?u.26497 → Type ?u.26497
CancelCommMonoid 
α: Type u
α] : 
CancelCommMonoid: Type ?u.26500 → Type ?u.26500
CancelCommMonoid (
ULift: Type ?u.26501 → Type (max?u.26501?u.26502)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.26505} → ULift α ≃ α
Equiv.ulift.
injective: ∀ {α : Sort ?u.26509} {β : Sort ?u.26508} (e : α ≃ β), Function.Injective ↑e
injective.
cancelCommMonoid: {M₁ : Type ?u.26515} →
  {M₂ : Type ?u.26514} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : CancelCommMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) →
                    (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → CancelCommMonoid M₁
cancelCommMonoid 
_: ?m.26527 → ?m.26528
_ 
rfl: ∀ {α : Sort ?u.26624} {a : α}, a = a
rfl (fun 
_: ?m.26728
_ 
_: ?m.26731
_ => 
rfl: ∀ {α : Sort ?u.26733} {a : α}, a = a
rfl) fun 
_: ?m.26868
_ 
_: ?m.26871
_ => 
rfl: ∀ {α : Sort ?u.26873} {a : α}, a = a
rfl
#align ulift.cancel_comm_monoid 
ULift.cancelCommMonoid: {α : Type u} → [inst : CancelCommMonoid α] → CancelCommMonoid (ULift α)
ULift.cancelCommMonoid
#align ulift.add_cancel_comm_monoid 
ULift.addCancelCommMonoid: {α : Type u} → [inst : AddCancelCommMonoid α] → AddCancelCommMonoid (ULift α)
ULift.addCancelCommMonoid

instance 
nontrivial: ∀ [inst : Nontrivial α], Nontrivial (ULift α)
nontrivial [
Nontrivial: Type ?u.27194 → Prop
Nontrivial 
α: Type u
α] : 
Nontrivial: Type ?u.27197 → Prop
Nontrivial (
ULift: Type ?u.27198 → Type (max?u.27198?u.27199)
ULift 
α: Type u
α) :=
  
Equiv.ulift: {α : Type ?u.27202} → ULift α ≃ α
Equiv.ulift.
symm: {α : Sort ?u.27206} → {β : Sort ?u.27205} → α ≃ β → β ≃ α
symm.
injective: ∀ {α : Sort ?u.27212} {β : Sort ?u.27211} (e : α ≃ β), Function.Injective ↑e
injective.
nontrivial: ∀ {α : Type ?u.27217} {β : Type ?u.27218} [inst : Nontrivial α] {f : α → β}, Function.Injective f → Nontrivial β
nontrivial
#align ulift.nontrivial 
ULift.nontrivial: ∀ {α : Type u} [inst : Nontrivial α], Nontrivial (ULift α)
ULift.nontrivial

-- TODO we don't do `OrderedCancelCommMonoid` or `OrderedCommGroup`
-- We'd need to add instances for `ULift` in `Order.Basic`.
end ULift