/-
Copyright (c) 2021 Julian Kuelshammer. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Julian Kuelshammer

! This file was ported from Lean 3 source module algebra.pempty_instances
! leanprover-community/mathlib commit c3019c79074b0619edb4b27553a91b2e82242395
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Defs
import Mathlib.Tactic.ToAdditive

/-!
# Instances on pempty

This file collects facts about algebraic structures on the (universe-polymorphic) empty type, e.g.
that it is a semigroup.
-/


universe u

@[
to_additive: AddSemigroup PEmpty
to_additive]
instance 
SemigroupPEmpty: Semigroup PEmpty
SemigroupPEmpty : 
Semigroup: Type ?u.2 → Type ?u.2
Semigroup 
PEmpty: Type u
PEmpty.{u + 1} where
  mul 
x: ?m.11
x 
_: ?m.14
_ := by
Goals accomplished! 🐙 
x, x✝: PEmpty

PEmptycases 
x: PEmpty
x
Goals accomplished! 🐙
  mul_assoc 
x: ?m.23
x 
y: ?m.26
y 
z: ?m.29
z := by
Goals accomplished! 🐙 
x, y, z: PEmpty

x * y * z = x * (y * z)cases 
x: PEmpty
x
Goals accomplished! 🐙
#align semigroup_pempty 
SemigroupPEmpty: Semigroup PEmpty
SemigroupPEmpty
#align add_semigroup_pempty 
AddSemigroupPEmpty: AddSemigroup PEmpty
AddSemigroupPEmpty