feat(data/equiv/mul_add): conj as a mul_aut (#3367)

src/data/equiv/mul_add.lean

@@ -208,10 +208,31 @@ instance : inhabited (mul_aut M) := ⟨1⟩
 @[simp] lemma coe_mul (e₁ e₂ : mul_aut M) : ⇑(e₁ * e₂) = e₁ ∘ e₂ := rfl
 @[simp] lemma coe_one : ⇑(1 : mul_aut M) = id := rfl
 
+lemma mul_def (e₁ e₂ : mul_aut M) : e₁ * e₂ = e₂.trans e₁ := rfl
+lemma one_def : (1 : mul_aut M) = mul_equiv.refl _ := rfl
+lemma inv_def (e₁ : mul_aut M) : e₁⁻¹ = e₁.symm := rfl
+@[simp] lemma mul_apply (e₁ e₂ : mul_aut M) (m : M) : (e₁ * e₂) m = e₁ (e₂ m) := rfl
+@[simp] lemma one_apply (m : M) : (1 : mul_aut M) m = m := rfl
+
 /-- Monoid hom from the group of multiplicative automorphisms to the group of permutations. -/
 def to_perm : mul_aut M →* equiv.perm M :=
 by refine_struct { to_fun := mul_equiv.to_equiv }; intros; refl
 
+/-- group conjugation as a group homomorphism into the automorphism group.
+  `conj g h = g * h * g⁻¹` -/
+def conj [group G] : G →* mul_aut G :=
+{ to_fun := λ g,
+  { to_fun := λ h, g * h * g⁻¹,
+    inv_fun := λ h, g⁻¹ * h * g,
+    left_inv := λ _, by simp [mul_assoc],
+    right_inv := λ _, by simp [mul_assoc],
+    map_mul' := by simp [mul_assoc] },
+  map_mul' := λ _ _, by ext; simp [mul_assoc],
+  map_one' := by ext; simp [mul_assoc] }
+
+@[simp] lemma conj_apply [group G] (g h : G) : conj g h = g * h * g⁻¹ := rfl
+@[simp] lemma conj_symm_apply [group G] (g h : G) : (conj g).symm h = g⁻¹ * h * g := rfl
+
 end mul_aut
 
 namespace add_aut
@@ -235,6 +256,12 @@ instance : inhabited (add_aut A) := ⟨1⟩
 @[simp] lemma coe_mul (e₁ e₂ : add_aut A) : ⇑(e₁ * e₂) = e₁ ∘ e₂ := rfl
 @[simp] lemma coe_one : ⇑(1 : add_aut A) = id := rfl
 
+lemma mul_def (e₁ e₂ : add_aut A) : e₁ * e₂ = e₂.trans e₁ := rfl
+lemma one_def : (1 : add_aut A) = add_equiv.refl _ := rfl
+lemma inv_def (e₁ : add_aut A) : e₁⁻¹ = e₁.symm := rfl
+@[simp] lemma mul_apply (e₁ e₂ : add_aut A) (a : A) : (e₁ * e₂) a = e₁ (e₂ a) := rfl
+@[simp] lemma one_apply (a : A) : (1 : add_aut A) a = a := rfl
+
 /-- Monoid hom from the group of multiplicative automorphisms to the group of permutations. -/
 def to_perm : add_aut A →* equiv.perm A :=
 by refine_struct { to_fun := add_equiv.to_equiv }; intros; refl
@@ -263,7 +290,6 @@ def map_equiv (h : M ≃* N) : units M ≃* units N :=
 
 end units
 
-
 namespace equiv
 
 section group

src/group_theory/semidirect_product.lean

@@ -139,15 +139,19 @@ le_antisymm
 
 section lift
 variables (f₁ : N →* H) (f₂ : G →* H)
-  (h : ∀ n g, f₁ (φ g n) = f₂ g * f₁ n * f₂ g⁻¹)
+  (h : ∀ g, f₁.comp (φ g).to_monoid_hom = (mul_aut.conj (f₂ g)).to_monoid_hom.comp f₁)
 
 /-- Define a group hom `N ⋊[φ] G →* H`, by defining maps `N →* H` and `G →* H`  -/
 def lift (f₁ : N →* H) (f₂ : G →* H)
-  (h : ∀ n g, f₁ (φ g n) = f₂ g * f₁ n * f₂ g⁻¹) :
+  (h : ∀ g, f₁.comp (φ g).to_monoid_hom = (mul_aut.conj (f₂ g)).to_monoid_hom.comp f₁) :
   N ⋊[φ] G →* H :=
 { to_fun := λ a, f₁ a.1 * f₂ a.2,
   map_one' := by simp,
-  map_mul' := λ a b, by simp [h, _root_.mul_assoc] }
+  map_mul' := λ a b, begin
+    have := λ n g, monoid_hom.ext_iff.1 (h n) g,
+    simp only [mul_aut.conj_apply, monoid_hom.comp_apply, mul_equiv.to_monoid_hom_apply] at this,
+    simp [this, mul_assoc]
+  end }
 
 @[simp] lemma lift_inl (n : N) : lift f₁ f₂ h (inl n) = f₁ n := by simp [lift]
 @[simp] lemma lift_comp_inl : (lift f₁ f₂ h).comp inl = f₁ := by ext; simp
@@ -156,7 +160,7 @@ def lift (f₁ : N →* H) (f₂ : G →* H)
 @[simp] lemma lift_comp_inr : (lift f₁ f₂ h).comp inr = f₂ := by ext; simp
 
 lemma lift_unique (F : N ⋊[φ] G →* H) :
-  F = lift (F.comp inl) (F.comp inr) (by simp [inl_aut]) :=
+  F = lift (F.comp inl) (F.comp inr) (λ _, by ext; simp [inl_aut]) :=
 begin
   ext,
   simp only [lift, monoid_hom.comp_apply, monoid_hom.coe_mk],