no goals
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a✝ b✝ a'✝ b'✝ : PreEnvelGroup R
ha : PreEnvelGroupRel' R a✝ a'✝
hb : PreEnvelGroupRel' R b✝ b'✝
⊢ mapAux f (PreEnvelGroup.mul a✝ b✝) = mapAux f (PreEnvelGroup.mul a'✝ b'✝)
simp [toEnvelGroup.mapAux, well_def f ha, well_def f hb]
no goals
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a✝ a'✝ : PreEnvelGroup R
ha : PreEnvelGroupRel' R a✝ a'✝
⊢ mapAux f (PreEnvelGroup.inv a✝) = mapAux f (PreEnvelGroup.inv a'✝)
simp [toEnvelGroup.mapAux, well_def f ha]
no goals
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a b c : PreEnvelGroup R
⊢ mapAux f (PreEnvelGroup.mul (PreEnvelGroup.mul a b) c) = mapAux f (PreEnvelGroup.mul a (PreEnvelGroup.mul b c))
apply mul_assoc
no goals
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (PreEnvelGroup.mul unit a) = mapAux f a
simp [toEnvelGroup.mapAux]
no goals
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (PreEnvelGroup.mul a unit) = mapAux f a
simp [toEnvelGroup.mapAux]
no goals
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (PreEnvelGroup.mul (PreEnvelGroup.inv a) a) = mapAux f unit
simp [toEnvelGroup.mapAux]
no goals
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x y : R
⊢ mapAux f (PreEnvelGroup.mul (PreEnvelGroup.mul (incl x) (incl y)) (PreEnvelGroup.inv (incl x))) =
    mapAux f (incl (x ◃ y))
simp [toEnvelGroup.mapAux]