awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N_1 : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P_1 : Type u_12
Q_1 : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst_1 : Mul P
inst_2 : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
x : N
⊢ (fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q))
      ((fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P)) k) x =
    k x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N_1 : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P_1 : Type u_12
Q_1 : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst_1 : Mul P
inst_2 : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
h₁ :
  ∀ (x : N),
    (g : (a : P) → Q) ((h * k) ((f.symm : (a : N) → M) x)) =
      HMul.hMul (α := N → Q) (β := N → Q) (fun (n : N) ↦ (g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)))
        (fun (n : N) ↦ (g : (a : P) → Q) (k ((f.symm : (a : N) → M) n))) x
⊢ (fun (n : N) ↦ (g : (a : P) → Q) ((h * k) ((f.symm : (a : N) → M) n))) =
    HMul.hMul (α := N → Q) (fun (n : N) ↦ (g : (a : P) → Q) (h ((f.symm : (a : N) → M) n))) fun (n : N) ↦
      (g : (a : P) → Q) (k ((f.symm : (a : N) → M) n))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N_1 : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P_1 : Type u_12
Q_1 : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst_1 : Mul P
inst_2 : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
x : N
⊢ (g : (a : P) → Q) ((h * k) ((f.symm : (a : N) → M) x)) =
    HMul.hMul (α := N → Q) (β := N → Q) (fun (n : N) ↦ (g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)))
      (fun (n : N) ↦ (g : (a : P) → Q) (k ((f.symm : (a : N) → M) n))) x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : M₁ ≃* M₂
f : M₁ →* N
h :
  ∀ (x : M₁),
    Eq.{u_8 + 1} (α := N)
      (((fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) ((fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) f) : (a : M₁) → N)
          x :
        N)
      ((f : (a : M₁) → N) x : N)
⊢ (fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) ((fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) f) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : M₁ ≃* M₂
f : M₁ →* N
x : M₁
⊢ Eq.{u_8 + 1} (α := N)
    (((fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) ((fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) f) : (a : M₁) → N) x :
      N)
    ((f : (a : M₁) → N) x : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : M₁ ≃* M₂
f : M₂ →* N
h :
  ∀ (x : M₂),
    Eq.{u_8 + 1} (α := N)
      (((fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) ((fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) f) : (a : M₂) → N)
          x :
        N)
      ((f : (a : M₂) → N) x : N)
⊢ (fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) ((fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) f) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : M₁ ≃* M₂
f : M₂ →* N
x : M₂
⊢ Eq.{u_8 + 1} (α := N)
    (((fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) ((fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) f) : (a : M₂) → N) x :
      N)
    ((f : (a : M₂) → N) x : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₁
h :
  ∀ (x : M),
    Eq.{u_9 + 1} (α := N₁) ((e.symm.toMonoidHom.comp (e.toMonoidHom.comp f) : (a : M) → N₁) x : N₁)
      ((f : (a : M) → N₁) x : N₁)
⊢ e.symm.toMonoidHom.comp (e.toMonoidHom.comp f) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₁
x : M
⊢ Eq.{u_9 + 1} (α := N₁) ((e.symm.toMonoidHom.comp (e.toMonoidHom.comp f) : (a : M) → N₁) x : N₁)
    ((f : (a : M) → N₁) x : N₁)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₂
h :
  ∀ (x : M),
    Eq.{u_10 + 1} (α := N₂) ((e.toMonoidHom.comp (e.symm.toMonoidHom.comp f) : (a : M) → N₂) x : N₂)
      ((f : (a : M) → N₂) x : N₂)
⊢ e.toMonoidHom.comp (e.symm.toMonoidHom.comp f) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₂
x : M
⊢ Eq.{u_10 + 1} (α := N₂) ((e.toMonoidHom.comp (e.symm.toMonoidHom.comp f) : (a : M) → N₂) x : N₂)
    ((f : (a : M) → N₂) x : N₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M : Type u_4
N : Type u_8
inst : MulOneClass M
inst_1 : Monoid N
⊢ Eq (α := (M →* N) ≃ (M →* N)) (monoidHomCongrLeftEquiv (refl M)) (Equiv.refl (M →* N))

Tactic:
rfl

Premises used: MulEquiv.monoidHomCongrLeftEquiv, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M : Type u_4
N : Type u_8
inst : MulOneClass M
inst_1 : Monoid N
⊢ Eq (α := (M →* N) ≃ (M →* N)) (monoidHomCongrRightEquiv (refl N)) (Equiv.refl (M →* N))

Tactic:
rfl

Premises used: MulEquiv.monoidHomCongrRightEquiv, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M₁ : Type u_5
M₂ : Type u_6
N : Type u_8
inst : MulOneClass M₁
inst_1 : MulOneClass M₂
inst_2 : Monoid N
e : M₁ ≃* M₂
⊢ Eq (α := (M₂ →* N) ≃ (M₁ →* N)) (Equiv.symm e.monoidHomCongrLeftEquiv) e.symm.monoidHomCongrLeftEquiv

Tactic:
rfl

Premises used: MulEquiv.monoidHomCongrLeftEquiv, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M : Type u_4
N₁ : Type u_9
N₂ : Type u_10
inst : MulOneClass M
inst_1 : Monoid N₁
inst_2 : Monoid N₂
e : N₁ ≃* N₂
⊢ Eq (α := (M →* N₂) ≃ (M →* N₁)) (Equiv.symm e.monoidHomCongrRightEquiv) e.symm.monoidHomCongrRightEquiv

Tactic:
rfl

Premises used: MulEquiv.monoidHomCongrRightEquiv, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
inst : MulOneClass M₁
inst_1 : MulOneClass M₂
inst_2 : MulOneClass M₃
inst_3 : Monoid N
e₁₂ : M₁ ≃* M₂
e₂₃ : M₂ ≃* M₃
⊢ Eq (α := (M₁ →* N) ≃ (M₃ →* N)) (e₁₂.trans e₂₃).monoidHomCongrLeftEquiv
    (Equiv.trans e₁₂.monoidHomCongrLeftEquiv e₂₃.monoidHomCongrLeftEquiv)

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.monoidHomCongrLeftEquiv, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M : Type u_4
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
inst : MulOneClass M
inst_1 : Monoid N₁
inst_2 : Monoid N₂
inst_3 : Monoid N₃
e₁₂ : N₁ ≃* N₂
e₂₃ : N₂ ≃* N₃
⊢ Eq (α := (M →* N₁) ≃ (M →* N₃)) (e₁₂.trans e₂₃).monoidHomCongrRightEquiv
    (Equiv.trans e₁₂.monoidHomCongrRightEquiv e₂₃.monoidHomCongrRightEquiv)

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.monoidHomCongrRightEquiv, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : CommMonoid N
inst_6 : CommMonoid N₁
inst_7 : CommMonoid N₂
inst_8 : CommMonoid N₃
e : M₁ ≃* M₂
f g : M₁ →* N
h :
  ∀ (x : M₂),
    Eq.{u_8 + 1} (α := N) ((Equiv.toFun e.monoidHomCongrLeftEquiv (f * g) : (a : M₂) → N) x : N)
      ((Equiv.toFun e.monoidHomCongrLeftEquiv f * Equiv.toFun e.monoidHomCongrLeftEquiv g : (a : M₂) → N) x : N)
⊢ Equiv.toFun e.monoidHomCongrLeftEquiv (f * g) =
    Equiv.toFun e.monoidHomCongrLeftEquiv f * Equiv.toFun e.monoidHomCongrLeftEquiv g

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : CommMonoid N
inst_6 : CommMonoid N₁
inst_7 : CommMonoid N₂
inst_8 : CommMonoid N₃
e : M₁ ≃* M₂
f g : M₁ →* N
x : M₂
⊢ Eq.{u_8 + 1} (α := N) ((Equiv.toFun e.monoidHomCongrLeftEquiv (f * g) : (a : M₂) → N) x : N)
    ((Equiv.toFun e.monoidHomCongrLeftEquiv f * Equiv.toFun e.monoidHomCongrLeftEquiv g : (a : M₂) → N) x : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : CommMonoid N
inst_6 : CommMonoid N₁
inst_7 : CommMonoid N₂
inst_8 : CommMonoid N₃
e : N₁ ≃* N₂
f g : M →* N₁
h :
  ∀ (x : M),
    Eq.{u_10 + 1} (α := N₂) ((Equiv.toFun e.monoidHomCongrRightEquiv (f * g) : (a : M) → N₂) x : N₂)
      ((Equiv.toFun e.monoidHomCongrRightEquiv f * Equiv.toFun e.monoidHomCongrRightEquiv g : (a : M) → N₂) x : N₂)
⊢ Equiv.toFun e.monoidHomCongrRightEquiv (f * g) =
    Equiv.toFun e.monoidHomCongrRightEquiv f * Equiv.toFun e.monoidHomCongrRightEquiv g

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : CommMonoid N
inst_6 : CommMonoid N₁
inst_7 : CommMonoid N₂
inst_8 : CommMonoid N₃
e : N₁ ≃* N₂
f g : M →* N₁
x : M
⊢ Eq.{u_10 + 1} (α := N₂) ((Equiv.toFun e.monoidHomCongrRightEquiv (f * g) : (a : M) → N₂) x : N₂)
    ((Equiv.toFun e.monoidHomCongrRightEquiv f * Equiv.toFun e.monoidHomCongrRightEquiv g : (a : M) → N₂) x : N₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M : Type u_4
N : Type u_8
inst : MulOneClass M
inst_1 : CommMonoid N
⊢ Eq (α := (M →* N) ≃* (M →* N)) (monoidHomCongrLeft (refl M)) (refl (M →* N))

Tactic:
rfl

Premises used: MulEquiv.refl, MulEquiv.monoidHomCongrLeftEquiv, Equiv.refl, rfl, MulEquiv.monoidHomCongrLeft
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M : Type u_4
N : Type u_8
inst : MulOneClass M
inst_1 : CommMonoid N
⊢ Eq (α := (M →* N) ≃* (M →* N)) (monoidHomCongrRight (refl N)) (refl (M →* N))

Tactic:
rfl

Premises used: MulEquiv.refl, MulEquiv.monoidHomCongrRight, MulEquiv.monoidHomCongrRightEquiv, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M₁ : Type u_5
M₂ : Type u_6
N : Type u_8
inst : MulOneClass M₁
inst_1 : MulOneClass M₂
inst_2 : CommMonoid N
e : M₁ ≃* M₂
⊢ Eq (α := (M₂ →* N) ≃* (M₁ →* N)) (symm e.monoidHomCongrLeft) e.symm.monoidHomCongrLeft

Tactic:
rfl

Premises used: MulEquiv.monoidHomCongrLeftEquiv, Equiv.symm, MulEquiv.symm, rfl, MulEquiv.monoidHomCongrLeft
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M : Type u_4
N₁ : Type u_9
N₂ : Type u_10
inst : MulOneClass M
inst_1 : CommMonoid N₁
inst_2 : CommMonoid N₂
e : N₁ ≃* N₂
⊢ Eq (α := (M →* N₂) ≃* (M →* N₁)) (symm e.monoidHomCongrRight) e.symm.monoidHomCongrRight

Tactic:
rfl

Premises used: MulEquiv.monoidHomCongrRight, MulEquiv.monoidHomCongrRightEquiv, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
inst : MulOneClass M₁
inst_1 : MulOneClass M₂
inst_2 : MulOneClass M₃
inst_3 : CommMonoid N
e₁₂ : M₁ ≃* M₂
e₂₃ : M₂ ≃* M₃
⊢ Eq (α := (M₁ →* N) ≃* (M₃ →* N)) (e₁₂.trans e₂₃).monoidHomCongrLeft
    (trans e₁₂.monoidHomCongrLeft e₂₃.monoidHomCongrLeft)

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.monoidHomCongrLeftEquiv, MulEquiv.trans, rfl, MulEquiv.monoidHomCongrLeft
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
M : Type u_4
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
inst : MulOneClass M
inst_1 : CommMonoid N₁
inst_2 : CommMonoid N₂
inst_3 : CommMonoid N₃
e₁₂ : N₁ ≃* N₂
e₂₃ : N₂ ≃* N₃
⊢ Eq (α := (M →* N₁) ≃* (M →* N₃)) (e₁₂.trans e₂₃).monoidHomCongrRight
    (trans e₁₂.monoidHomCongrRight e₂₃.monoidHomCongrRight)

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.trans, MulEquiv.monoidHomCongrRight, MulEquiv.monoidHomCongrRightEquiv, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
η : Type u_16
Ms : η → Type u_17
inst : (j : η) → Mul (Ms j)
⊢ Eq (α := ((j : η) → Ms j) ≃* ((j : η) → Ms j)) (piCongrRight (Ms := Ms) (Ns := Ms) fun (j : η) ↦ refl (Ms j))
    (refl ((j : η) → Ms j))

Tactic:
rfl

Premises used: MulEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
η : Type u_16
Ms : η → Type u_17
Ns : η → Type u_18
inst : (j : η) → Mul (Ms j)
inst_1 : (j : η) → Mul (Ns j)
es : (j : η) → MulEquiv.{u_17, u_18} (Ms j) (Ns j)
⊢ (piCongrRight (Ms := Ms) (Ns := Ns) es).symm = piCongrRight (Ms := Ns) (Ns := Ms) fun (i : η) ↦ (es i).symm

Tactic:
rfl

Premises used: MulEquiv.piCongrRight, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
η : Type u_16
Ms : η → Type u_17
Ns : η → Type u_18
Ps : η → Type u_19
inst : (j : η) → Mul (Ms j)
inst_1 : (j : η) → Mul (Ns j)
inst_2 : (j : η) → Mul (Ps j)
es : (j : η) → MulEquiv.{u_17, u_18} (Ms j) (Ns j)
fs : (j : η) → MulEquiv.{u_18, u_19} (Ns j) (Ps j)
⊢ (piCongrRight (Ms := Ms) (Ns := Ns) es).trans (piCongrRight (Ms := Ns) (Ns := Ps) fs) =
    piCongrRight (Ms := Ms) (Ns := Ps) fun (i : η) ↦ (es i).trans (fs i)

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.piCongrRight, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
G : Type u_14
inst : InvolutiveInv G
⊢ Equiv.symm (Equiv.inv G) = Equiv.inv G

Tactic:
rfl

Premises used: Equiv.inv, Function.Involutive.toPerm, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
M : Type u_4
N : Type u_5
inst : One M
inst_1 : One N
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : OneHomClass F M N
f : F
x : M
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) ↔ x = 1

Tactic:
_root_.map_eq_one_iff f (EmbeddingLike.injective f)

Premises used: map_eq_one_iff, EmbeddingLike.injective
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
M : Type u_4
N : Type u_5
inst : One M
inst_1 : One N
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : OneHomClass F M N
f : F
x : M
⊢ Ne.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) ↔ x ≠ 1

Tactic:
map_eq_one_iff.not

Premises used: EmbeddingLike.map_eq_one_iff, Iff.not
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F_1 : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F_1 M N
F : Type u_9
inst_1 : Mul M
inst_2 : Mul N
inst_3 : EquivLike F M N
h : MulEquivClass F M N
⊢ MulHomClass F M N

Tactic:
{ h with }

Premises used: MulEquivClass.map_mul, MulHomClass.mk
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F M N
inst_1 : MulOneClass M
inst_2 : MulOneClass N
inst_3 : MulEquivClass F M N
e : F
rw : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) (1 * EquivLike.inv e 1) : N) ((e : (a : M) → N) (EquivLike.inv e 1) : N)
rw₁ rw₂ : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) (EquivLike.inv e 1) : N) ((e : (a : M) → N) (EquivLike.inv e 1) : N)
⊢ HMul.hMul (α := N) (β := N) ((e : (a : M) → N) 1 : N) ((e : (a : M) → N) (EquivLike.inv e 1) : N) =
    (e : (a : M) → N) (EquivLike.inv e 1)

Tactic:
rw [← map_mul, one_mul]

Premises used: MulEquivClass.map_mul, one_mul
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
f g : M ≃* N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
mk :
  ∀ (toEquiv : M ≃ N) (map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
    (h₁ : { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.toFun = g.toFun)
    (h₂ : { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.invFun = g.invFun),
    { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
g : M ≃* N
toEquiv : M ≃ N
map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
h₁ : { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.toFun = g.toFun
h₂ : { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.invFun = g.invFun
mk :
  ∀ (toEquiv_1 : M ≃ N) (map_mul'_1 : ∀ (x y : M), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y)
    (h₁ :
      { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.toFun =
        { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.toFun)
    (h₂ :
      { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.invFun =
        { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.invFun),
    { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N } = { toEquiv := toEquiv_1, map_mul' := map_mul'_1 }
⊢ { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N } = g

Tactic:
cases g
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
toEquiv : M ≃ N
map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
toEquiv_1 : M ≃ N
map_mul'_1 : ∀ (x y : M), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y
h₁ :
  { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.toFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.toFun
h₂ :
  { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.invFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.invFun
mk : toEquiv = toEquiv_1
⊢ { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N } = { toEquiv := toEquiv_1, map_mul' := map_mul'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
toEquiv : M ≃ N
map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
toEquiv_1 : M ≃ N
map_mul'_1 : ∀ (x y : M), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y
h₁ :
  { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.toFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.toFun
h₂ :
  { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.invFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.invFun
⊢ toEquiv = toEquiv_1

Tactic:
apply Equiv.coe_fn_injective h₁

Premises used: Equiv.coe_fn_injective
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f g : M ≃* N
h : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
x x' : M
⊢ x = x' → Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x' : N)

Tactic:
DFunLike.congr_arg f

Premises used: DFunLike.congr_arg
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f g : M ≃* N
h : f = g
x : M
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃ N
hf :
  ∀ (x y : M),
    (f : (a : M) → N) (x * y) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ Eq (α := (a : M) → N) (⇑{ toEquiv := f, map_mul' := hf : M ≃* N } : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
e' : N → M
h₁ : LeftInverse e' (⇑e : (a : M) → N)
h₂ : RightInverse e' (⇑e : (a : M) → N)
h₃ :
  ∀ (x y : M),
    { toFun := (⇑e : (a : M) → N), invFun := e', left_inv := h₁, right_inv := h₂ : M ≃ N }.toFun (x * y) =
      { toFun := (⇑e : (a : M) → N), invFun := e', left_inv := h₁, right_inv := h₂ : M ≃ N }.toFun x *
        { toFun := (⇑e : (a : M) → N), invFun := e', left_inv := h₁, right_inv := h₂ : M ≃ N }.toFun y
⊢ { toFun := (⇑e : (a : M) → N), invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃ : M ≃* N } = e

Tactic:
ext fun _ => rfl

Premises used: MulEquiv.ext, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ f.toEquiv = (↑f : M ≃ N)

Tactic:
rfl

Premises used: EquivLike.toEquiv, rfl