import data.int.cast.defs

import algebra.hom.equiv.basic

import algebra.group_with_zero.inj_surj

universes u v

variables {α : Type u} {β : Type*} {x y : ulift.{v} α}

namespace ulift

@[to_additive] instance has_one [has_one α] : has_one (ulift α) := ⟨⟨1⟩⟩

@[simp, to_additive] lemma one_down [has_one α] : (1 : ulift α).down = 1 := rfl

@[to_additive] instance has_mul [has_mul α] : has_mul (ulift α) := ⟨λ f g, ⟨f.down * g.down⟩⟩

@[simp, to_additive] lemma mul_down [has_mul α] : (x * y).down = x.down * y.down := rfl

@[to_additive] instance has_div [has_div α] : has_div (ulift α) := ⟨λ f g, ⟨f.down / g.down⟩⟩

@[simp, to_additive] lemma div_down [has_div α] : (x / y).down = x.down / y.down := rfl

@[to_additive] instance has_inv [has_inv α] : has_inv (ulift α) := ⟨λ f, ⟨f.down⁻¹⟩⟩

@[simp, to_additive] lemma inv_down [has_inv α] : x⁻¹.down = (x.down)⁻¹ := rfl

instance has_smul [has_smul α β] : has_smul α (ulift β) := ⟨λ n x, up (n • x.down)⟩

lemma smul_down [has_smul α β] (a : α) (b : ulift.{v} β) : (a • b).down = a • b.down := rfl

instance has_pow [has_pow α β] : has_pow (ulift α) β := ⟨λ x n, up (x.down ^ n)⟩

lemma pow_down [has_pow α β] (a : ulift.{v} α) (b : β) : (a ^ b).down = a.down ^ b := rfl

def _root_.mul_equiv.ulift [has_mul α] : ulift α ≃* α :=

{ map_mul' := λ x y, rfl,

.. equiv.ulift }

instance semigroup [semigroup α] : semigroup (ulift α) :=

mul_equiv.ulift.injective.semigroup _ $ λ x y, rfl

instance comm_semigroup [comm_semigroup α] : comm_semigroup (ulift α) :=

equiv.ulift.injective.comm_semigroup _ $ λ x y, rfl

instance mul_one_class [mul_one_class α] : mul_one_class (ulift α) :=

equiv.ulift.injective.mul_one_class _ rfl $ λ x y, rfl

instance mul_zero_one_class [mul_zero_one_class α] : mul_zero_one_class (ulift α) :=

equiv.ulift.injective.mul_zero_one_class _ rfl rfl $ λ x y, rfl

instance monoid [monoid α] : monoid (ulift α) :=

equiv.ulift.injective.monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance comm_monoid [comm_monoid α] : comm_monoid (ulift α) :=

equiv.ulift.injective.comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

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 add_monoid_with_one [add_monoid_with_one α] : add_monoid_with_one (ulift α) :=

{ nat_cast_zero := congr_arg ulift.up nat.cast_zero,

nat_cast_succ := λ n, congr_arg ulift.up (nat.cast_succ _),

.. ulift.has_one, .. ulift.add_monoid, ..ulift.has_nat_cast }

instance add_comm_monoid_with_one [add_comm_monoid_with_one α] :

add_comm_monoid_with_one (ulift α) :=

{ ..ulift.add_monoid_with_one, .. ulift.add_comm_monoid }

instance monoid_with_zero [monoid_with_zero α] : monoid_with_zero (ulift α) :=

equiv.ulift.injective.monoid_with_zero _ rfl rfl (λ _ _, rfl) (λ _ _, rfl)

instance comm_monoid_with_zero [comm_monoid_with_zero α] : comm_monoid_with_zero (ulift α) :=

equiv.ulift.injective.comm_monoid_with_zero _ rfl rfl (λ _ _, rfl) (λ _ _, rfl)

instance div_inv_monoid [div_inv_monoid α] : div_inv_monoid (ulift α) :=

equiv.ulift.injective.div_inv_monoid _ rfl (λ _ _, rfl) (λ _, rfl)

(λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance group [group α] : group (ulift α) :=

equiv.ulift.injective.group _ rfl (λ _ _, rfl) (λ _, rfl)

(λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance comm_group [comm_group α] : comm_group (ulift α) :=

equiv.ulift.injective.comm_group _ rfl (λ _ _, rfl) (λ _, rfl)

(λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance add_group_with_one [add_group_with_one α] : add_group_with_one (ulift α) :=

{ int_cast := λ n, ⟨n⟩,

int_cast_of_nat := λ n, congr_arg ulift.up (int.cast_of_nat _),

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 }

instance add_comm_group_with_one [add_comm_group_with_one α] : add_comm_group_with_one (ulift α) :=

{ ..ulift.add_group_with_one, .. ulift.add_comm_group }

instance group_with_zero [group_with_zero α] : group_with_zero (ulift α) :=

equiv.ulift.injective.group_with_zero _ rfl rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

(λ _ _, rfl)

instance comm_group_with_zero [comm_group_with_zero α] : comm_group_with_zero (ulift α) :=

equiv.ulift.injective.comm_group_with_zero _ rfl rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)

(λ _ _, rfl) (λ _ _, rfl)

instance left_cancel_semigroup [left_cancel_semigroup α] :

left_cancel_semigroup (ulift α) :=

equiv.ulift.injective.left_cancel_semigroup _ (λ _ _, rfl)

instance right_cancel_semigroup [right_cancel_semigroup α] :

right_cancel_semigroup (ulift α) :=

equiv.ulift.injective.right_cancel_semigroup _ (λ _ _, rfl)

instance left_cancel_monoid [left_cancel_monoid α] :

left_cancel_monoid (ulift α) :=

equiv.ulift.injective.left_cancel_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance right_cancel_monoid [right_cancel_monoid α] :

right_cancel_monoid (ulift α) :=

equiv.ulift.injective.right_cancel_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance cancel_monoid [cancel_monoid α] :

cancel_monoid (ulift α) :=

equiv.ulift.injective.cancel_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance cancel_comm_monoid [cancel_comm_monoid α] :

cancel_comm_monoid (ulift α) :=

equiv.ulift.injective.cancel_comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance nontrivial [nontrivial α] : nontrivial (ulift α) :=

equiv.ulift.symm.injective.nontrivial

end ulift