awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit.{u_1, u_2} (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : Membership.mem (γ := Subgroup M) (fixingSubgroup M sᶜ) g
g_eq : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M sᶜ) x) g g_fixing • a = b
⊢ g • a = b

Tactic:
rw [Submonoid.mk_smul] at g_eq

Premises used: Submonoid.mk_smul
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit.{u_1, u_2} (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : Membership.mem (γ := Subgroup M) (fixingSubgroup M sᶜ) g
g_eq : g • a = b
⊢ (fixedBy α g)ᶜ ⊆ s

Tactic:
rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing

Premises used: mem_fixingSubgroup_compl_iff_movedBy_subset
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit.{u_1, u_2} (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : Membership.mem (γ := Subgroup M) (fixingSubgroup M sᶜ) g
g_eq : g • a = b
g_fixing₁ : (fixedBy α g)ᶜ ⊆ s
⊢ g • a = b

Tactic:
rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing

Premises used: mem_fixingSubgroup_compl_iff_movedBy_subset
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit.{u_1, u_2} (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : (fixedBy α g)ᶜ ⊆ s
g_eq : g • a = b
rwa : g • a ∈ s
rwa₁ rwa₂ rwa₃ rwa₄ : a ∈ s
⊢ b ∈ s

Tactic:
rwa [← g_eq, smul_mem_of_set_mem_fixedBy (set_mem_fixedBy_of_movedBy_subset g_fixing)]

Premises used: MulAction.smul_mem_of_set_mem_fixedBy, MulAction.set_mem_fixedBy_of_movedBy_subset
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
f g : X →ₑ[φ] Y
h : f.toFun = g.toFun
mk :
  ∀ (toFun : X → Y) (map_smul' : ∀ (m : M) (x : X), toFun (m • x) = φ m • toFun x)
    (h : { toFun := toFun, map_smul' := map_smul' : X →ₑ[φ] Y }.toFun = g.toFun),
    { toFun := toFun, map_smul' := map_smul' : X →ₑ[φ] Y } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
g : X →ₑ[φ] Y
toFun : X → Y
map_smul' : ∀ (m : M) (x : X), toFun (m • x) = φ m • toFun x
h : { toFun := toFun, map_smul' := map_smul' : X →ₑ[φ] Y }.toFun = g.toFun
mk :
  ∀ (toFun_1 : X → Y) (map_smul'_1 : ∀ (m : M) (x : X), toFun_1 (m • x) = φ m • toFun_1 x)
    (h :
      { toFun := toFun, map_smul' := map_smul' : X →ₑ[φ] Y }.toFun =
        { toFun := toFun_1, map_smul' := map_smul'_1 : X →ₑ[φ] Y }.toFun),
    { toFun := toFun, map_smul' := map_smul' : X →ₑ[φ] Y } = { toFun := toFun_1, map_smul' := map_smul'_1 }
⊢ { toFun := toFun, map_smul' := map_smul' : X →ₑ[φ] Y } = g

Tactic:
cases g
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
toFun : X → Y
map_smul' : ∀ (m : M) (x : X), toFun (m • x) = φ m • toFun x
toFun_1 : X → Y
map_smul'_1 : ∀ (m : M) (x : X), toFun_1 (m • x) = φ m • toFun_1 x
h :
  { toFun := toFun, map_smul' := map_smul' : X →ₑ[φ] Y }.toFun =
    { toFun := toFun_1, map_smul' := map_smul'_1 : X →ₑ[φ] Y }.toFun
⊢ { toFun := toFun, map_smul' := map_smul' : X →ₑ[φ] Y } = { toFun := toFun_1, map_smul' := map_smul'_1 }

Tactic:
congr
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
F : Type u_8
M : Type u_9
X : Type u_10
Y : Type u_11
inst : SMul M X
inst_1 : SMul M Y
inst_2 : FunLike F X Y
inst_3 : MulActionHomClass F M X Y
f : F
c : M
x : X
⊢ (f : (a : X) → Y) (c • x) = HSMul.hSMul (β := Y) c ((f : (a : X) → Y) x : Y)

Tactic:
map_smulₛₗ f c x

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
X : Type u_5
inst : SMul M' X
Y : Type u_6
inst_1 : SMul M' Y
F : Type u_8
inst_2 : FunLike F X Y
inst_3 : MulOneClass X
inst_4 : SMul X Y
inst_5 : IsScalarTower M' X Y
inst_6 : MulActionHomClass F X X Y
f : F
m : M'
x : X
rw : (f : (a : X) → Y) (m • x * 1) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
rw₁ : (f : (a : X) → Y) (HSMul.hSMul (β := X) (m • x) 1) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
rw₂ : HSMul.hSMul (β := Y) (m • x) ((f : (a : X) → Y) 1 : Y) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
rw₃ : m • HSMul.hSMul (β := Y) x ((f : (a : X) → Y) 1 : Y) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
rw₄ :
  HSMul.hSMul (β := Y) m ((f : (a : X) → Y) (HSMul.hSMul (β := X) x 1) : Y) =
    HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
rw₅ : HSMul.hSMul (β := Y) m ((f : (a : X) → Y) (x * 1) : Y) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
rw₆ : HSMul.hSMul (β := Y) m ((f : (a : X) → Y) x : Y) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
rw₇ rw₈ : HSMul.hSMul (β := Y) m ((f : (a : X) → Y) x : Y) = HSMul.hSMul (β := Y) m ((f : (a : X) → Y) x : Y)
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)

Tactic:
rw [← mul_one (m • x), ← smul_eq_mul, map_smul, smul_assoc, ← map_smul,
      smul_eq_mul, mul_one, id_eq]

Premises used: smul_assoc, HSMul.hSMul, smul_eq_mul, mul_one, map_smul, id_eq
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
X : Type u_5
inst : SMul M' X
Y : Type u_6
inst_1 : SMul M' Y
f : MulActionHom.{u_1, u_1, u_5, u_6} (M := M') id X Y
m : M'
x : X
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) m ((f : (a : X) → Y) x : Y)

Tactic:
map_smul f m x

Premises used: map_smul
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
f g : X →ₑ[φ] Y
⊢ (∀ (x : X), Eq.{u_6 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y)) → f = g

Tactic:
DFunLike.ext f g

Premises used: DFunLike.ext
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
f g : X →ₑ[φ] Y
h : f = g
x : X
⊢ Eq.{u_6 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y)

Tactic:
DFunLike.congr_fun h _

Premises used: DFunLike.congr_fun
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
φ' : M → N
h : φ = φ'
f : X →ₑ[φ] Y
⊢ (ofEq h f).toFun = f.toFun

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
φ' : M → N
h : φ = φ'
f : X →ₑ[φ] Y
a : X
⊢ Eq.{u_6 + 1} (α := Y) ((ofEq h f : (a : X) → Y) a : Y) ((f : (a : X) → Y) a : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
X : Type u_5
inst : SMul M' X
Y : Type u_6
inst_1 : SMul M' Y
F : Type u_8
inst_2 : FunLike F X Y
inst_3 : FaithfulSMul M' X
inst_4 : MulActionHomClass F M' X Y
f : F
hf : Function.Injective.{u_5 + 1, u_6 + 1} (α := X) (β := Y) (⇑f : (a : X) → Y)
x x_1 : M'
h : ∀ (a : Y), x • a = x_1 • a
m : X
simp_rw : HSMul.hSMul (β := Y) x ((f : (a : X) → Y) m : Y) = HSMul.hSMul (β := Y) x_1 ((f : (a : X) → Y) m : Y)
⊢ Eq.{u_6 + 1} (α := Y) ((f : (a : X) → Y) (x • m) : Y) ((f : (a : X) → Y) (x_1 • m) : Y)

Tactic:
simp_rw [map_smul, h]

Premises used: map_smul
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
X : Type u_5
inst : SMul M X
x : X
⊢ (MulActionHom.id M : (a : X) → X) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
rw rw₁ :
  Eq.{u_7 + 1} (α := Z) ((g : (a : Y) → Z) (HSMul.hSMul (β := Y) (φ m) ((f : (a : X) → Y) x : Y)) : Z)
    ((g : (a : Y) → Z) (HSMul.hSMul (β := Y) (φ m) ((f : (a : X) → Y) x : Y)) : Z)
⊢ Eq.{u_7 + 1} (α := Z) ((g : (a : Y) → Z) ((f : (a : X) → Y) (m • x) : Y) : Z)
    ((g : (a : Y) → Z) (HSMul.hSMul (β := Y) (φ m) ((f : (a : X) → Y) x : Y)) : Z)

Tactic:
rw [map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
rw rw₁ :
  HSMul.hSMul (β := Z) (ψ (φ m)) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z) =
    HSMul.hSMul (β := Z) (ψ (φ m)) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z)
⊢ (g : (a : Y) → Z) (HSMul.hSMul (β := Y) (φ m) ((f : (a : X) → Y) x : Y)) =
    HSMul.hSMul (β := Z) (ψ (φ m)) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z)

Tactic:
rw [map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
rw rw₁ :
  HSMul.hSMul (β := Z) (χ m) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z) =
    HSMul.hSMul (β := Z) (χ m) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z)
⊢ HSMul.hSMul (β := Z) ((ψ ∘ φ) m) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z) =
    HSMul.hSMul (β := Z) (χ m) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z)

Tactic:
rw [κ.comp_eq]

Premises used: CompTriple.comp_eq
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
Z : Type u_7
inst_2 : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
inst_3 : CompTriple φ ψ χ
x : X
⊢ Eq.{u_7 + 1} (α := Z) ((g.comp f : (a : X) → Z) x : Z) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
f : X →ₑ[φ] Y
x : X
rw : Eq.{u_6 + 1} (α := Y) ((MulActionHom.id N : (a : Y) → Y) ((f : (a : X) → Y) x : Y) : Y) ((f : (a : X) → Y) x : Y)
rw₁ rw₂ : Eq.{u_6 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)
⊢ Eq.{u_6 + 1} (α := Y) ((comp (MulActionHom.id N) f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)

Tactic:
rw [comp_apply, id_apply]

Premises used: MulActionHom.comp_apply, MulActionHom.id_apply
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
f : X →ₑ[φ] Y
x : X
rw : Eq.{u_6 + 1} (α := Y) ((f : (a : X) → Y) ((MulActionHom.id M : (a : X) → X) x : X) : Y) ((f : (a : X) → Y) x : Y)
rw₁ rw₂ : Eq.{u_6 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)
⊢ Eq.{u_6 + 1} (α := Y) ((f.comp (MulActionHom.id M) : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)

Tactic:
rw [comp_apply, id_apply]

Premises used: MulActionHom.comp_apply, MulActionHom.id_apply
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
Z : Type u_7
inst_2 : SMul P Z
Q : Type u_8
T : Type u_9
inst_3 : SMul Q T
η : P → Q
θ : M → Q
ζ : N → Q
h : Z →ₑ[η] T
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
inst_4 : CompTriple φ ψ χ
inst_5 : CompTriple χ η θ
inst_6 : CompTriple ψ η ζ
inst_7 : CompTriple φ ζ θ
⊢ h.comp (g.comp f) = (h.comp g).comp f

Tactic:
ext fun _ => rfl

Premises used: MulActionHom.ext, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst_5 : SMul M Y₁
f : MulActionHom.{u_2, u_2, u_5, u_8} (M := M) id X Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y₁)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y₁)
m : M
x : Y₁
rw rw₁ : g (m • x) = g (m • x)
⊢ g (m • x) = g (HSMul.hSMul (β := Y₁) m ((f : (a : X) → Y₁) (g x) : Y₁))

Tactic:
rw [h₂]
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst_5 : SMul M Y₁
f : MulActionHom.{u_2, u_2, u_5, u_8} (M := M) id X Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y₁)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y₁)
m : M
x : Y₁
⊢ g (HSMul.hSMul (β := Y₁) m ((f : (a : X) → Y₁) (g x) : Y₁)) = g ((f : (a : X) → Y₁) (m • g x))

Tactic:
simp only [map_smul]

Premises used: map_smul
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst_5 : SMul M Y₁
f : MulActionHom.{u_2, u_2, u_5, u_8} (M := M) id X Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y₁)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y₁)
m : M
x : Y₁
rw rw₁ : m • g x = m • g x
⊢ g ((f : (a : X) → Y₁) (m • g x)) = m • g x

Tactic:
rw [h₁]
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst_5 : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y)
m : N
x : Y
rw rw₁ : g (m • x) = g (m • x)
⊢ g (m • x) = g (HSMul.hSMul (β := Y) m ((f : (a : X) → Y) (g x) : Y))

Tactic:
rw [h₂]
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst_5 : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y)
m : N
x : Y
rw rw₁ :
  g (HSMul.hSMul (β := Y) m ((f : (a : X) → Y) (g x) : Y)) = g (HSMul.hSMul (β := Y) m ((f : (a : X) → Y) (g x) : Y))
⊢ g (HSMul.hSMul (β := Y) m ((f : (a : X) → Y) (g x) : Y)) =
    g (HSMul.hSMul (β := Y) (φ (φ' m)) ((f : (a : X) → Y) (g x) : Y))

Tactic:
rw [k]
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst_5 : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y)
m : N
x : Y
rw rw₁ :
  g (HSMul.hSMul (β := Y) (φ (φ' m)) ((f : (a : X) → Y) (g x) : Y)) =
    g (HSMul.hSMul (β := Y) (φ (φ' m)) ((f : (a : X) → Y) (g x) : Y))
⊢ g (HSMul.hSMul (β := Y) (φ (φ' m)) ((f : (a : X) → Y) (g x) : Y)) = g ((f : (a : X) → Y) (φ' m • g x))

Tactic:
rw [map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst : SMul M X
inst_1 : SMul M' X
Y : Type u_6
inst_2 : SMul N Y
inst_3 : SMul M' Y
Z : Type u_7
inst_4 : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst_5 : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y)
m : N
x : Y
rw rw₁ : φ' m • g x = φ' m • g x
⊢ g ((f : (a : X) → Y) (φ' m • g x)) = φ' m • g x

Tactic:
rw [h₁]
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
X : Type u_5
inst : SMul M X
Y₁ : Type u_8
inst_1 : SMul M Y₁
f : MulActionHom.{u_2, u_2, u_5, u_8} (M := M) id X Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y₁)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y₁)
⊢ f.inverse g h₁ h₂ = f.inverse' g ⋯ h₁ h₂

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y)
⊢ (f.inverse' g k₂ h₁ h₂).inverse' (⇑f : (a : X) → Y) k₁ h₂ h₁ = f

Tactic:
ext fun _ => rfl

Premises used: MulActionHom.ext, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y)
a :
  ∀ (x : X),
    Eq (α := X) (((f.inverse' g k₂ h₁ h₂).comp f : (a : X) → X) x : X) ((MulActionHom.id M : (a : X) → X) x : X)
⊢ (f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y)
x : X
⊢ Eq (α := X) (((f.inverse' g k₂ h₁ h₂).comp f : (a : X) → X) x : X) ((MulActionHom.id M : (a : X) → X) x : X)

Tactic:
simpa using h₁.eq _

Premises used: Function.LeftInverse.eq
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y)
a :
  ∀ (x : Y),
    Eq (α := Y) ((f.comp (f.inverse' g k₂ h₁ h₂) : (a : Y) → Y) x : Y) ((MulActionHom.id N : (a : Y) → Y) x : Y)
⊢ f.comp (f.inverse' g k₂ h₁ h₂) = MulActionHom.id N

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst : SMul M X
Y : Type u_6
inst_1 : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g (⇑f : (a : X) → Y)
h₂ : Function.RightInverse g (⇑f : (a : X) → Y)
x : Y
⊢ Eq (α := Y) ((f.comp (f.inverse' g k₂ h₁ h₂) : (a : Y) → Y) x : Y) ((MulActionHom.id N : (a : Y) → Y) x : Y)

Tactic:
simpa using h₂.eq _

Premises used: Function.RightInverse.eq
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
γ : Type u_5
δ : Type u_6
inst : SMul M α
inst_1 : SMul N γ
inst_2 : SMul N δ
σ : M → N
f : α →ₑ[σ] γ
g : α →ₑ[σ] δ
⊢ comp (fst N γ δ) (f.prod g) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
γ : Type u_5
δ : Type u_6
inst : SMul M α
inst_1 : SMul N γ
inst_2 : SMul N δ
σ : M → N
f : α →ₑ[σ] γ
g : α →ₑ[σ] δ
⊢ comp (snd N γ δ) (f.prod g) = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
⊢ Eq (α := MulActionHom (M := M) id (α × β) (α × β)) (prod (fst M α β) (snd M α β)) (MulActionHom.id M)

Tactic:
rfl

Premises used: MulActionHom.prod, rfl
-- 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 : SMul N Y
inst_2 : SMul R Y
inst_3 : SMulCommClass N R Y
h : R
f : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X),
    HSMul.hSMul (β := (a : X) → Y) h (⇑f : (a : X) → Y) (m • x) =
      σ m • HSMul.hSMul (β := (a : X) → Y) h (⇑f : (a : X) → Y) x

Tactic:
simp [smul_comm _ h]

Premises used: SMulCommClass.smul_comm
-- 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 : SMul N Y
inst_2 : SMul R Y
inst_3 : SMulCommClass N R Y
f : X →ₑ[σ] Y
r : R
⊢ (⇑(r • f) : (a : X) → Y) = HSMul.hSMul (β := (a : X) → Y) r (⇑f : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- 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 : Zero Y
inst_2 : SMulZeroClass N Y
⊢ ∀ (m : M) (x : X), 0 (m • x) = HSMul.hSMul (β := Y) (σ m) (0 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 : Zero Y
inst_2 : SMulZeroClass N Y
⊢ Eq (α := (a : X) → Y) (⇑0 : (a : X) → Y) 0

Tactic:
rfl

Premises used: rfl
-- 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 : AddZeroClass Y
inst_2 : DistribSMul N Y
f g : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X),
    HAdd.hAdd (α := (a : X) → Y) (β := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y) (m • x) =
      σ m • HAdd.hAdd (α := (a : X) → Y) (β := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y) x

Tactic:
simp [smul_add]

Premises used: smul_add
-- 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 : AddZeroClass Y
inst_2 : DistribSMul N Y
f g : X →ₑ[σ] Y
⊢ (⇑(f + g) : (a : X) → Y) = HAdd.hAdd (α := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- 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 : AddGroup Y
inst_2 : DistribSMul N Y
f : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (-(⇑f : (a : X) → Y)) (m • x) = HSMul.hSMul (β := Y) (σ m) ((-(⇑f : (a : X) → Y)) x : Y)

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 : AddGroup Y
inst_2 : DistribSMul N Y
f g : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X),
    HSub.hSub (α := (a : X) → Y) (β := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y) (m • x) =
      σ m • HSub.hSub (α := (a : X) → Y) (β := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y) x

Tactic:
simp [smul_sub]

Premises used: smul_sub
-- 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 : AddGroup Y
inst_2 : DistribSMul N Y
f : X →ₑ[σ] Y
⊢ Eq (α := (a : X) → Y) (⇑(-f) : (a : X) → Y) (-(⇑f : (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 : AddGroup Y
inst_2 : DistribSMul N Y
f g : X →ₑ[σ] Y
⊢ (⇑(f - g) : (a : X) → Y) = HSub.hSub (α := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y)

Tactic:
rfl

Premises used: rfl