awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst : SMul M X
inst_1 : Monoid N
inst_2 : Monoid Y
inst_3 : MulDistribMulAction N Y
f g : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X),
    HMul.hMul (α := (a : X) → Y) (β := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y) (m • x) =
      σ m • HMul.hMul (α := (a : X) → Y) (β := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y) x

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst : SMul M X
inst_1 : Monoid N
inst_2 : Monoid Y
inst_3 : MulDistribMulAction N Y
⊢ ∀ (m : M) (x : X), 1 (m • x) = HSMul.hSMul (β := Y) (σ m) (1 x)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst : SMul M X
inst_1 : Monoid N
inst_2 : Monoid Y
inst_3 : MulDistribMulAction N Y
f g : X →ₑ[σ] Y
⊢ (⇑(f * g) : (a : X) → Y) = HMul.hMul (α := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst : SMul M X
inst_1 : Monoid N
inst_2 : Monoid Y
inst_3 : MulDistribMulAction N Y
⊢ Eq (α := (a : X) → Y) (⇑1 : (a : X) → Y) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst_3 : Monoid A
inst_4 : MulDistribMulAction M A
B : Type u_5
inst_5 : Monoid B
inst_6 : MulDistribMulAction N B
B₁ : Type u_6
inst_7 : Monoid B₁
inst_8 : MulDistribMulAction M B₁
C : Type u_7
inst_9 : Monoid C
inst_10 : MulDistribMulAction P C
A' : Type u_8
inst_11 : Group A'
inst_12 : MulDistribMulAction M A'
B' : Type u_9
inst_13 : Group B'
inst_14 : MulDistribMulAction N B'
f g : A →ₑ*[φ] B
h : Eq (α := (a : A) → B) ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) f) ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) g)
rcases :
  ∀ (tF : MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B) (map_one' : tF.toFun 1 = 1)
    (map_mul' : ∀ (x y : A), tF.toFun (x * y) = tF.toFun x * tF.toFun y)
    (h :
      Eq (α := (a : A) → B)
        ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' })
        ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) g)),
    { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' : A →ₑ*[φ] B } = g
⊢ f = g

Tactic:
rcases f with ⟨tF, _, _⟩
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst_3 : Monoid A
inst_4 : MulDistribMulAction M A
B : Type u_5
inst_5 : Monoid B
inst_6 : MulDistribMulAction N B
B₁ : Type u_6
inst_7 : Monoid B₁
inst_8 : MulDistribMulAction M B₁
C : Type u_7
inst_9 : Monoid C
inst_10 : MulDistribMulAction P C
A' : Type u_8
inst_11 : Group A'
inst_12 : MulDistribMulAction M A'
B' : Type u_9
inst_13 : Group B'
inst_14 : MulDistribMulAction N B'
g : A →ₑ*[φ] B
tF : MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B
map_one' : tF.toFun 1 = 1
map_mul' : ∀ (x y : A), tF.toFun (x * y) = tF.toFun x * tF.toFun y
h :
  Eq (α := (a : A) → B)
    ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' })
    ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) g)
rcases :
  ∀ (tG : MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B) (map_one'_1 : tG.toFun 1 = 1)
    (map_mul'_1 : ∀ (x y : A), tG.toFun (x * y) = tG.toFun x * tG.toFun y)
    (h :
      Eq (α := (a : A) → B)
        ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' })
        ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) { toMulActionHom := tG, map_one' := map_one'_1, map_mul' := map_mul'_1 })),
    { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' : A →ₑ*[φ] B } =
      { toMulActionHom := tG, map_one' := map_one'_1, map_mul' := map_mul'_1 }
⊢ { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' : A →ₑ*[φ] B } = g

Tactic:
rcases g with ⟨tG, _, _⟩
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst_3 : Monoid A
inst_4 : MulDistribMulAction M A
B : Type u_5
inst_5 : Monoid B
inst_6 : MulDistribMulAction N B
B₁ : Type u_6
inst_7 : Monoid B₁
inst_8 : MulDistribMulAction M B₁
C : Type u_7
inst_9 : Monoid C
inst_10 : MulDistribMulAction P C
A' : Type u_8
inst_11 : Group A'
inst_12 : MulDistribMulAction M A'
B' : Type u_9
inst_13 : Group B'
inst_14 : MulDistribMulAction N B'
tF : MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B
map_one' : tF.toFun 1 = 1
map_mul' : ∀ (x y : A), tF.toFun (x * y) = tF.toFun x * tF.toFun y
tG : MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B
map_one'_1 : tG.toFun 1 = 1
map_mul'_1 : ∀ (x y : A), tG.toFun (x * y) = tG.toFun x * tG.toFun y
h :
  Eq (α := (a : A) → B)
    ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' })
    ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) { toMulActionHom := tG, map_one' := map_one'_1, map_mul' := map_mul'_1 })
mk :
  ∀ (toFun : A → B)
    (map_smul' :
      ∀ (m : M) (x : A), toFun (m • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := N) ((φ : (a : M) → N) m : N) (toFun x))
    (map_one' :
      { toFun := toFun, map_smul' := map_smul' :
              MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
          1 =
        1)
    (map_mul' :
      ∀ (x y : A),
        { toFun := toFun, map_smul' := map_smul' :
                MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
            (x * y) =
          { toFun := toFun, map_smul' := map_smul' :
                  MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
              x *
            { toFun := toFun, map_smul' := map_smul' :
                  MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
              y)
    (h :
      Eq (α := (a : A) → B)
        ((fun (m : A →ₑ*[φ] B) ↦ m.toFun)
          { toFun := toFun, map_smul' := map_smul', map_one' := map_one', map_mul' := map_mul' })
        ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) { toMulActionHom := tG, map_one' := map_one'_1, map_mul' := map_mul'_1 })),
    { toFun := toFun, map_smul' := map_smul', map_one' := map_one', map_mul' := map_mul' : A →ₑ*[φ] B } =
      { toMulActionHom := tG, map_one' := map_one'_1, map_mul' := map_mul'_1 }
⊢ { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' : A →ₑ*[φ] B } =
    { toMulActionHom := tG, map_one' := map_one'_1, map_mul' := map_mul'_1 }

Tactic:
cases tF
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst_3 : Monoid A
inst_4 : MulDistribMulAction M A
B : Type u_5
inst_5 : Monoid B
inst_6 : MulDistribMulAction N B
B₁ : Type u_6
inst_7 : Monoid B₁
inst_8 : MulDistribMulAction M B₁
C : Type u_7
inst_9 : Monoid C
inst_10 : MulDistribMulAction P C
A' : Type u_8
inst_11 : Group A'
inst_12 : MulDistribMulAction M A'
B' : Type u_9
inst_13 : Group B'
inst_14 : MulDistribMulAction N B'
toFun : A → B
map_smul' : ∀ (m : M) (x : A), toFun (m • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := N) ((φ : (a : M) → N) m : N) (toFun x)
map_one' :
  { toFun := toFun, map_smul' := map_smul' :
          MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
      1 =
    1
map_mul' :
  ∀ (x y : A),
    { toFun := toFun, map_smul' := map_smul' :
            MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
        (x * y) =
      { toFun := toFun, map_smul' := map_smul' :
              MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
          x *
        { toFun := toFun, map_smul' := map_smul' :
              MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
          y
toFun_1 : A → B
map_smul'_1 :
  ∀ (m : M) (x : A), toFun_1 (m • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := N) ((φ : (a : M) → N) m : N) (toFun_1 x)
map_one'_1 :
  { toFun := toFun_1, map_smul' := map_smul'_1 :
          MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
      1 =
    1
map_mul'_1 :
  ∀ (x y : A),
    { toFun := toFun_1, map_smul' := map_smul'_1 :
            MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
        (x * y) =
      { toFun := toFun_1, map_smul' := map_smul'_1 :
              MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
          x *
        { toFun := toFun_1, map_smul' := map_smul'_1 :
              MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
          y
h :
  Eq (α := (a : A) → B)
    ((fun (m : A →ₑ*[φ] B) ↦ m.toFun)
      { toFun := toFun, map_smul' := map_smul', map_one' := map_one', map_mul' := map_mul' })
    ((fun (m : A →ₑ*[φ] B) ↦ m.toFun)
      { toFun := toFun_1, map_smul' := map_smul'_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })
⊢ { toFun := toFun, map_smul' := map_smul', map_one' := map_one', map_mul' := map_mul' : A →ₑ*[φ] B } =
    { toFun := toFun_1, map_smul' := map_smul'_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }

Tactic:
congr
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f : A →ₑ*[φ] B
⊢ f.toFun = (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f : A →ₑ*[φ] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →* B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f : A →ₑ*[φ] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₑ[(⇑φ : (a : M) → N)] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f g : A →ₑ*[φ] B
⊢ (∀ (x : A), Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)) → f = g

Tactic:
DFunLike.ext f g

Premises used: DFunLike.ext
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h : f = g
x : A
⊢ Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)

Tactic:
DFunLike.congr_fun h _

Premises used: DFunLike.congr_fun
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h :
  Eq (α := MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B) (↑f : A →ₑ[(⇑φ : (a : M) → N)] B)
    (↑g : A →ₑ[(⇑φ : (a : M) → N)] B)
a : ∀ (a : A), Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h :
  Eq (α := MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B) (↑f : A →ₑ[(⇑φ : (a : M) → N)] B)
    (↑g : A →ₑ[(⇑φ : (a : M) → N)] B)
a : A
⊢ Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
MulActionHom.congr_fun h a

Premises used: MulActionHom.congr_fun
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h :
  Eq (α := MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B) (↑f : A →ₑ[(⇑φ : (a : M) → N)] B)
    (↑g : A →ₑ[(⇑φ : (a : M) → N)] B)
a : A
⊢ Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
exact MulActionHom.congr_fun h a

Premises used: MulActionHom.congr_fun
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h : Eq (α := A →* B) (↑f : A →* B) (↑g : A →* B)
a : ∀ (a : A), Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h : Eq (α := A →* B) (↑f : A →* B) (↑g : A →* B)
a : A
⊢ Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
DFunLike.congr_fun h a

Premises used: DFunLike.congr_fun
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h : Eq (α := A →* B) (↑f : A →* B) (↑g : A →* B)
a : A
⊢ Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
exact DFunLike.congr_fun h a

Premises used: DFunLike.congr_fun
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f : A →ₑ*[φ] B
⊢ Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)

Tactic:
map_one f

Premises used: map_one
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f : A →ₑ*[φ] B
x y : A
⊢ (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)

Tactic:
map_mul f x y

Premises used: map_mul
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A' : Type u_8
inst_2 : Group A'
inst_3 : MulDistribMulAction M A'
B' : Type u_9
inst_4 : Group B'
inst_5 : MulDistribMulAction N B'
f : A' →ₑ*[φ] B'
x : A'
⊢ Eq.{u_9 + 1} (α := B') ((f : (a : A') → B') x⁻¹ : B') (((f : (a : A') → B') x)⁻¹ : B')

Tactic:
map_inv f x

Premises used: map_inv
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A' : Type u_8
inst_2 : Group A'
inst_3 : MulDistribMulAction M A'
B' : Type u_9
inst_4 : Group B'
inst_5 : MulDistribMulAction N B'
f : A' →ₑ*[φ] B'
x y : A'
⊢ (f : (a : A') → B') (x / y) = HDiv.hDiv (α := B') (β := B') ((f : (a : A') → B') x : B') ((f : (a : A') → B') y : B')

Tactic:
map_div f x y

Premises used: map_div
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f : A →ₑ*[φ] B
m : M
x : A
⊢ (f : (a : A) → B) (m • x) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := N) (β := B) ((φ : (a : M) → N) m : N) ((f : (a : A) → B) x : B)

Tactic:
map_smulₛₗ f m x

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
A : Type u_4
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
x : A
⊢ (MulDistribMulActionHom.id M : (a : A) → A) x = x

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A_1 : Type u_4
inst_3 : Monoid A_1
inst_4 : MulDistribMulAction M A_1
B_1 : Type u_5
inst_5 : Monoid B_1
inst_6 : MulDistribMulAction N B_1
B₁ : Type u_6
inst_7 : Monoid B₁
inst_8 : MulDistribMulAction M B₁
C : Type u_7
inst_9 : Monoid C
inst_10 : MulDistribMulAction P C
A' : Type u_8
inst_11 : Group A'
inst_12 : MulDistribMulAction M A'
B' : Type u_9
inst_13 : Group B'
inst_14 : MulDistribMulAction N B'
F : Type u_10
inst_15 : FunLike F A_1 B_1
A : Type u_11
inst_16 : AddMonoid A
inst_17 : DistribMulAction M A
B : Type u_12
inst_18 : AddMonoid B
inst_19 : DistribMulAction N B
m : M
x : A
⊢ ZeroHom.toFun (↑0 : ZeroHom A B) (m • x) =
    HSMul.hSMul.{u_2, u_12, u_12} (α := N) (β := B) ((φ : (a : M) → N) m : N) (ZeroHom.toFun (↑0 : ZeroHom A B) x)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_11
inst_2 : AddMonoid A
inst_3 : DistribMulAction M A
B : Type u_12
inst_4 : AddMonoid B
inst_5 : DistribMulAction N B
⊢ Eq (α := (a : A) → B) (⇑0 : (a : A) → B) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
A : Type u_4
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
⊢ Eq.{u_4 + 1} (α := (a : A) → A) (⇑1 : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_11
inst_2 : AddMonoid A
inst_3 : DistribMulAction M A
B : Type u_12
inst_4 : AddMonoid B
inst_5 : DistribMulAction N B
a : A
⊢ Eq.{u_12 + 1} (α := B) ((0 : (a : A) → B) a : B) (0 : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
A : Type u_4
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
a : A
⊢ (1 : (a : A) → A) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
A : Type u_4
inst_3 : Monoid A
inst_4 : MulDistribMulAction M A
B : Type u_5
inst_5 : Monoid B
inst_6 : MulDistribMulAction N B
C : Type u_7
inst_7 : Monoid C
inst_8 : MulDistribMulAction P C
g : B →ₑ*[ψ] C
f : A →ₑ*[φ] B
inst_9 : φ.CompTriple ψ χ
x : A
⊢ Eq.{u_7 + 1} (α := C) ((g.comp f : (a : A) → C) x : C) ((g : (a : B) → C) ((f : (a : A) → B) x : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f : A →ₑ*[φ] B
x : A
rw :
  Eq.{u_5 + 1} (α := B) ((MulDistribMulActionHom.id N : (a : B) → B) ((f : (a : A) → B) x : B) : B)
    ((f : (a : A) → B) x : B)
rw₁ rw₂ : Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
⊢ Eq.{u_5 + 1} (α := B) ((comp (MulDistribMulActionHom.id N) f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rw [comp_apply, id_apply]

Premises used: MulDistribMulActionHom.id_apply, MulDistribMulActionHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
A : Type u_4
inst_2 : Monoid A
inst_3 : MulDistribMulAction M A
B : Type u_5
inst_4 : Monoid B
inst_5 : MulDistribMulAction N B
f : A →ₑ*[φ] B
x : A
rw :
  Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) ((MulDistribMulActionHom.id M : (a : A) → A) x : A) : B)
    ((f : (a : A) → B) x : B)
rw₁ rw₂ : Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
⊢ Eq.{u_5 + 1} (α := B) ((f.comp (MulDistribMulActionHom.id M) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rw [comp_apply, id_apply]

Premises used: MulDistribMulActionHom.id_apply, MulDistribMulActionHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
A : Type u_4
inst_3 : Monoid A
inst_4 : MulDistribMulAction M A
B : Type u_5
inst_5 : Monoid B
inst_6 : MulDistribMulAction N B
C : Type u_7
inst_7 : Monoid C
inst_8 : MulDistribMulAction P C
Q : Type u_11
D : Type u_12
inst_9 : Monoid Q
inst_10 : Monoid D
inst_11 : MulDistribMulAction Q D
η : P →* Q
θ : M →* Q
ζ : N →* Q
h : C →ₑ*[η] D
g : B →ₑ*[ψ] C
f : A →ₑ*[φ] B
inst_12 : φ.CompTriple ψ χ
inst_13 : χ.CompTriple η θ
inst_14 : ψ.CompTriple η ζ
inst_15 : φ.CompTriple ζ θ
⊢ h.comp (g.comp f) = (h.comp g).comp f

Tactic:
ext fun _ => rfl

Premises used: MulDistribMulActionHom.ext, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
R : Type u_10
inst : Semiring R
S : Type u_11
inst_1 : Semiring S
N' : Type u_13
inst_2 : AddMonoid N'
inst_3 : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') 1 : N') ((g : (a : R) → N') 1 : N')
a : ∀ (x : R), Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') x : N') ((g : (a : R) → N') x : N')
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
R : Type u_10
inst : Semiring R
S : Type u_11
inst_1 : Semiring S
N' : Type u_13
inst_2 : AddMonoid N'
inst_3 : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') 1 : N') ((g : (a : R) → N') 1 : N')
x : R
a : Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') (x * 1) : N') ((g : (a : R) → N') (x * 1) : N')
a₁ :
  Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') (HSMul.hSMul (β := R) x 1) : N')
    ((g : (a : R) → N') (HSMul.hSMul (β := R) x 1) : N')
a₂ :
  HSMul.hSMul.{u_11, u_13, u_13} (α := S) (β := N') ((σ : (a : R) → S) x : S) ((f : (a : R) → N') 1 : N') =
    (g : (a : R) → N') (HSMul.hSMul (β := R) x 1)
a₃ :
  HSMul.hSMul.{u_11, u_13, u_13} (α := S) (β := N') ((σ : (a : R) → S) x : S) ((f : (a : R) → N') 1 : N') =
    HSMul.hSMul.{u_11, u_13, u_13} (α := S) (β := N') ((σ : (a : R) → S) x : S) ((g : (a : R) → N') 1 : N')
a₄ a₅ :
  HSMul.hSMul.{u_11, u_13, u_13} (α := S) (β := N') ((σ : (a : R) → S) x : S) ((g : (a : R) → N') 1 : N') =
    HSMul.hSMul.{u_11, u_13, u_13} (α := S) (β := N') ((σ : (a : R) → S) x : S) ((g : (a : R) → N') 1 : N')
⊢ Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') x : N') ((g : (a : R) → N') x : N')

Tactic:
rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]

Premises used: DistribMulActionHom.map_smulₑ, smul_eq_mul, mul_one