awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
inst_2 : FaithfulSMul M α
m : M
simp_rw : (∀ (x : α), x ∈ fixedBy α m) ↔ ∀ (x : α), m • x = HSMul.hSMul.{u_3, u_1, u_1} (α := M) 1 x
⊢ (∀ (x : α), x ∈ fixedBy α m) ↔
    Eq.{u_1 + 1} (α := α → α) (fun (x2 : α) ↦ m • x2) fun (x2 : α) ↦ HSMul.hSMul.{u_3, u_1, u_1} (α := M) 1 x2
have simp_rw₁ : (∀ (x : α), x ∈ fixedBy α m) ↔ ∀ (x : α), m • x = x
Tactic: simp_rw [funext_iff, one_smul, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
g h : G
ne_one : g ≠ 1
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
⊢ ¬Commute g h
have contrapose : ∀ (comm : Commute g h), g = 1
Tactic: contrapose ne_one with comm
Cleared hypotheses: ne_one
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
⊢ g = 1
have rwa : ∀ (disjoint : Disjoint (fixedBy α g)ᶜ (fixedBy α g)ᶜ) (comm : Commute g h), g = 1
Tactic: rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
    compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint
Cleared hypotheses: disjoint, comm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
rwa : ∀ (disjoint : Disjoint (fixedBy α g)ᶜ (fixedBy α g)ᶜ) (comm : Commute g h), g = 1
⊢ g = 1
have rwa₁ : ∀ (disjoint : (fixedBy α g)ᶜ = ⊥) (comm : Commute g h), g = 1
Tactic: rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
    compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint
Cleared hypotheses: disjoint, comm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
rwa : ∀ (disjoint : Disjoint (fixedBy α g)ᶜ (fixedBy α g)ᶜ) (comm : Commute g h), g = 1
rwa₁ : ∀ (disjoint : (fixedBy α g)ᶜ = ⊥) (comm : Commute g h), g = 1
⊢ g = 1
have rwa₂ : ∀ (disjoint : (fixedBy α g)ᶜ = ∅) (comm : Commute g h), g = 1
Tactic: rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
    compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint
Cleared hypotheses: disjoint, comm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
rwa : ∀ (disjoint : Disjoint (fixedBy α g)ᶜ (fixedBy α g)ᶜ) (comm : Commute g h), g = 1
rwa₁ : ∀ (disjoint : (fixedBy α g)ᶜ = ⊥) (comm : Commute g h), g = 1
rwa₂ : ∀ (disjoint : (fixedBy α g)ᶜ = ∅) (comm : Commute g h), g = 1
⊢ g = 1
have rwa₃ : ∀ (disjoint : (fixedBy α g)ᶜ = Set.univᶜ) (comm : Commute g h), g = 1
Tactic: rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
    compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint
Cleared hypotheses: disjoint, comm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
rwa : ∀ (disjoint : Disjoint (fixedBy α g)ᶜ (fixedBy α g)ᶜ) (comm : Commute g h), g = 1
rwa₁ : ∀ (disjoint : (fixedBy α g)ᶜ = ⊥) (comm : Commute g h), g = 1
rwa₂ : ∀ (disjoint : (fixedBy α g)ᶜ = ∅) (comm : Commute g h), g = 1
rwa₃ : ∀ (disjoint : (fixedBy α g)ᶜ = Set.univᶜ) (comm : Commute g h), g = 1
⊢ g = 1
have rwa₄ : ∀ (disjoint : fixedBy α g = Set.univ) (comm : Commute g h), g = 1
Tactic: rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
    compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint
Cleared hypotheses: disjoint, comm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
rwa : ∀ (disjoint : Disjoint (fixedBy α g)ᶜ (fixedBy α g)ᶜ) (comm : Commute g h), g = 1
rwa₁ : ∀ (disjoint : (fixedBy α g)ᶜ = ⊥) (comm : Commute g h), g = 1
rwa₂ : ∀ (disjoint : (fixedBy α g)ᶜ = ∅) (comm : Commute g h), g = 1
rwa₃ : ∀ (disjoint : (fixedBy α g)ᶜ = Set.univᶜ) (comm : Commute g h), g = 1
rwa₄ : ∀ (disjoint : fixedBy α g = Set.univ) (comm : Commute g h), g = 1
⊢ g = 1
have rwa₅ : ∀ (disjoint : g = 1) (comm : Commute g h), g = 1
Tactic: rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
    compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint
Cleared hypotheses: disjoint, comm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : Set α
x y : M
hx : Membership.mem (γ := Set M) {ϕ : M | ∀ (x : (↑s : Type u_2)), ϕ • (↑x : α) = (↑x : α)} x
hy : Membership.mem (γ := Set M) {ϕ : M | ∀ (x : (↑s : Type u_2)), ϕ • (↑x : α) = (↑x : α)} y
z : (↑s : Type u_2)
⊢ (x * y) • (↑z : α) = (↑z : α)
have rw : x • y • (↑z : α) = (↑z : α)
Tactic: rw [mul_smul, hy z, hx z]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : Set α
x y : M
hx : Membership.mem (γ := Set M) {ϕ : M | ∀ (x : (↑s : Type u_2)), ϕ • (↑x : α) = (↑x : α)} x
hy : Membership.mem (γ := Set M) {ϕ : M | ∀ (x : (↑s : Type u_2)), ϕ • (↑x : α) = (↑x : α)} y
z : (↑s : Type u_2)
rw : x • y • (↑z : α) = (↑z : α)
⊢ (x * y) • (↑z : α) = (↑z : α)
have rw₁ : x • (↑z : α) = (↑z : α)
Tactic: rw [mul_smul, hy z, hx z]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : Set α
x y : M
hx : Membership.mem (γ := Set M) {ϕ : M | ∀ (x : (↑s : Type u_2)), ϕ • (↑x : α) = (↑x : α)} x
hy : Membership.mem (γ := Set M) {ϕ : M | ∀ (x : (↑s : Type u_2)), ϕ • (↑x : α) = (↑x : α)} y
z : (↑s : Type u_2)
rw : x • y • (↑z : α) = (↑z : α)
rw₁ : x • (↑z : α) = (↑z : α)
⊢ (x * y) • (↑z : α) = (↑z : α)
have rw₂ : (↑z : α) = (↑z : α)
Tactic: rw [mul_smul, hy z, hx z]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x : M
hx : x ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (fixingSubmonoid M s))
z : (↑s : Type u_2)
⊢ x⁻¹ • (↑z : α) = (↑z : α)
have rw : (↑z : α) = x • (↑z : α)
Tactic: rw [inv_smul_eq_iff, hx z]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x : M
hx : x ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (fixingSubmonoid M s))
z : (↑s : Type u_2)
rw : (↑z : α) = x • (↑z : α)
⊢ x⁻¹ • (↑z : α) = (↑z : α)
have rw₁ : (↑z : α) = (↑z : α)
Tactic: rw [inv_smul_eq_iff, hx z]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
m : M
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m ↔ s ⊆ fixedBy α m
have simp_rw : (∀ y ∈ s, m • y = y) ↔ s ⊆ fixedBy α m
Tactic: simp_rw [mem_fixingSubgroup_iff, Set.subset_def, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
m : M
simp_rw : (∀ y ∈ s, m • y = y) ↔ s ⊆ fixedBy α m
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m ↔ s ⊆ fixedBy α m
have simp_rw₁ : (∀ y ∈ s, m • y = y) ↔ ∀ x ∈ s, x ∈ fixedBy α m
Tactic: simp_rw [mem_fixingSubgroup_iff, Set.subset_def, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
m : M
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M sᶜ) m ↔ (fixedBy α m)ᶜ ⊆ s
have rw : sᶜ ⊆ fixedBy α m ↔ (fixedBy α m)ᶜ ⊆ s
Tactic: rw [mem_fixingSubgroup_iff_subset_fixedBy, Set.compl_subset_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
m : M
rw : sᶜ ⊆ fixedBy α m ↔ (fixedBy α m)ᶜ ⊆ s
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M sᶜ) m ↔ (fixedBy α m)ᶜ ⊆ s
have rw₁ : (fixedBy α m)ᶜ ⊆ s ↔ (fixedBy α m)ᶜ ⊆ s
Tactic: rw [mem_fixingSubgroup_iff_subset_fixedBy, Set.compl_subset_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
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
⊢ b ∈ s
have let : ∀ (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),
  b ∈ s
Tactic: let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (hypothesis)
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
⊢ b ∈ s
have g_eq₁ : g • a = b
Tactic: rw [Submonoid.mk_smul] at g_eq
Cleared hypotheses: g_eq
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (hypothesis)
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
⊢ b ∈ s
have g_fixing₁ : (fixedBy α g)ᶜ ⊆ s
Tactic: rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing
Cleared hypotheses: g_fixing, g_eq
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixingSubgroup (goal)
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
⊢ b ∈ s
have rwa : g • a ∈ s
Tactic: rwa [← g_eq, smul_mem_of_set_mem_fixedBy (set_mem_fixedBy_of_movedBy_subset g_fixing)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ { toFun := toFun, map_smul' := map_smul' : X →ₑ[φ] Y } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
have rw : (f : (a : X) → Y) (m • x * 1) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
have rw₁ : (f : (a : X) → Y) (HSMul.hSMul (β := X) (m • x) 1) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
have rw₂ : HSMul.hSMul (β := Y) (m • x) ((f : (a : X) → Y) 1 : Y) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
have rw₃ : m • HSMul.hSMul (β := Y) x ((f : (a : X) → Y) 1 : Y) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
have 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)
Tactic: rw [← mul_one (m • x), ← smul_eq_mul, map_smul, smul_assoc, ← map_smul,
      smul_eq_mul, mul_one, id_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
have rw₅ : HSMul.hSMul (β := Y) m ((f : (a : X) → Y) (x * 1) : Y) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
have rw₆ : HSMul.hSMul (β := Y) m ((f : (a : X) → Y) x : Y) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ (f : (a : X) → Y) (m • x) = HSMul.hSMul (β := Y) (id m) ((f : (a : X) → Y) x : Y)
have rw₇ : HSMul.hSMul (β := Y) m ((f : (a : X) → Y) x : Y) = HSMul.hSMul (β := Y) 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ Eq.{u_6 + 1} (α := Y) ((f : (a : X) → Y) (x • m) : Y) ((f : (a : X) → Y) (x_1 • m) : Y)
have simp_rw : HSMul.hSMul (β := Y) x ((f : (a : X) → Y) m : Y) = HSMul.hSMul (β := Y) x_1 ((f : (a : X) → Y) m : Y)
Tactic: simp_rw [map_smul, h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ 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)
have 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)
Tactic: rw [map_smulₛₗ]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ (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)
have 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)
Tactic: rw [map_smulₛₗ]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ 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)
have 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)
Tactic: rw [κ.comp_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ Eq.{u_6 + 1} (α := Y) ((comp (MulActionHom.id N) f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)
have 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)
Tactic: rw [comp_apply, id_apply]