/-
Copyright (c) 2018 Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hughes,
  Johannes Hölzl, Yury Kudryashov
Ported by: Frédéric Dupuis

! This file was ported from Lean 3 source module algebra.hom.commute
! leanprover-community/mathlib commit 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Group
import Mathlib.Algebra.Group.Commute

/-!
# Multiplicative homomorphisms respect semiconjugation and commutation.
-/


section Commute

variable {
F: Type ?u.23
F 
M: Type ?u.5
M 
N: Type ?u.959
N : 
Type _: Type (?u.953+1)
Type _} [
Mul: Type ?u.32 → Type ?u.32
Mul 
M: Type ?u.5
M] [
Mul: Type ?u.14 → Type ?u.14
Mul 
N: Type ?u.8
N] {
a: M
a 
x: M
x 
y: M
y : 
M: Type ?u.5
M}

@[
to_additive: ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {a x y : M} [inst_2 : AddHomClass F M N],
  AddSemiconjBy a x y → ∀ (f : F), AddSemiconjBy (↑f a) (↑f x) (↑f y)
to_additive (attr := simp)]
protected theorem 
SemiconjBy.map: ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {a x y : M} [inst_2 : MulHomClass F M N],
  SemiconjBy a x y → ∀ (f : F), SemiconjBy (↑f a) (↑f x) (↑f y)
SemiconjBy.map [
MulHomClass: Type ?u.46 →
  (M : outParam (Type ?u.45)) →
    (N : outParam (Type ?u.44)) → [inst : Mul M] → [inst : Mul N] → Type (max(max?u.46?u.45)?u.44)
MulHomClass 
F: Type ?u.23
F 
M: Type ?u.26
M 
N: Type ?u.29
N] (
h: SemiconjBy a x y
h : 
SemiconjBy: {M : Type ?u.63} → [inst : Mul M] → M → M → M → Prop
SemiconjBy 
a: M
a 
x: M
x 
y: M
y) (
f: F
f : 
F: Type ?u.23
F) :
    
SemiconjBy: {M : Type ?u.85} → [inst : Mul M] → M → M → M → Prop
SemiconjBy (
f: F
f 
a: M
a) (
f: F
f 
x: M
x) (
f: F
f 
y: M
y) := by
Goals accomplished! 🐙 
F: Type u_1

M: Type u_2

N: Type u_3

inst✝²: Mul M

inst✝¹: Mul N

a, x, y: M

inst✝: MulHomClass F M N

h: SemiconjBy a x y

f: F

SemiconjBy (↑f a) (↑f x) (↑f y)simpa only [
SemiconjBy: {M : Type ?u.385} → [inst : Mul M] → M → M → M → Prop
SemiconjBy, 
map_mul: ∀ {M : Type ?u.388} {N : Type ?u.389} {F : Type ?u.387} [inst : Mul M] [inst_1 : Mul N] [inst_2 : MulHomClass F M N]
  (f : F) (x y : M), ↑f (x * y) = ↑f x * ↑f y
map_mul] using 
congr_arg: ∀ {α : Sort ?u.523} {β : Sort ?u.522} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
f: F
f 
h: SemiconjBy a x y
h
Goals accomplished! 🐙
#align semiconj_by.map 
SemiconjBy.map: ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {a x y : M} [inst_2 : MulHomClass F M N],
  SemiconjBy a x y → ∀ (f : F), SemiconjBy (↑f a) (↑f x) (↑f y)
SemiconjBy.map
#align add_semiconj_by.map 
AddSemiconjBy.map: ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {a x y : M} [inst_2 : AddHomClass F M N],
  AddSemiconjBy a x y → ∀ (f : F), AddSemiconjBy (↑f a) (↑f x) (↑f y)
AddSemiconjBy.map

@[
to_additive: ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {x y : M} [inst_2 : AddHomClass F M N],
  AddCommute x y → ∀ (f : F), AddCommute (↑f x) (↑f y)
to_additive (attr := simp)]
protected theorem 
Commute.map: ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {x y : M} [inst_2 : MulHomClass F M N],
  Commute x y → ∀ (f : F), Commute (↑f x) (↑f y)
Commute.map [
MulHomClass: Type ?u.976 →
  (M : outParam (Type ?u.975)) →
    (N : outParam (Type ?u.974)) → [inst : Mul M] → [inst : Mul N] → Type (max(max?u.976?u.975)?u.974)
MulHomClass 
F: Type ?u.953
F 
M: Type ?u.956
M 
N: Type ?u.959
N] (
h: Commute x y
h : 
Commute: {S : Type ?u.993} → [inst : Mul S] → S → S → Prop
Commute 
x: M
x 
y: M
y) (
f: F
f : 
F: Type ?u.953
F) : 
Commute: {S : Type ?u.1015} → [inst : Mul S] → S → S → Prop
Commute (
f: F
f 
x: M
x) (
f: F
f 
y: M
y) :=
  
SemiconjBy.map: ∀ {F : Type ?u.1219} {M : Type ?u.1220} {N : Type ?u.1221} [inst : Mul M] [inst_1 : Mul N] {a x y : M}
  [inst_2 : MulHomClass F M N], SemiconjBy a x y → ∀ (f : F), SemiconjBy (↑f a) (↑f x) (↑f y)
SemiconjBy.map 
h: Commute x y
h 
f: F
f
#align commute.map 
Commute.map: ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {x y : M} [inst_2 : MulHomClass F M N],
  Commute x y → ∀ (f : F), Commute (↑f x) (↑f y)
Commute.map
#align add_commute.map 
AddCommute.map: ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {x y : M} [inst_2 : AddHomClass F M N],
  AddCommute x y → ∀ (f : F), AddCommute (↑f x) (↑f y)
AddCommute.map

end Commute