awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)
Tactic: rw [comp_apply, id_apply]
-- 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) ((f.comp (MulActionHom.id M) : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)
have 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)
Tactic: rw [comp_apply, id_apply]
-- 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
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)
⊢ Eq.{u_6 + 1} (α := Y) ((f.comp (MulActionHom.id M) : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)
have rw₁ : Eq.{u_6 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)
Tactic: rw [comp_apply, id_apply]
-- 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
φ' : 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 (m • x) = g (HSMul.hSMul (β := Y₁) m ((f : (a : X) → Y₁) (g x) : Y₁))
have rw : g (m • x) = g (m • x)
Tactic: rw [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
φ' : 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 ((f : (a : X) → Y₁) (m • g x)) = m • g x
have rw : m • g x = m • g x
Tactic: rw [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
φ' : 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
⊢ g (m • x) = g (HSMul.hSMul (β := Y) m ((f : (a : X) → Y) (g x) : Y))
have rw : g (m • x) = g (m • x)
Tactic: rw [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
φ' : 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
⊢ g (HSMul.hSMul (β := Y) m ((f : (a : X) → Y) (g x) : Y)) =
    g (HSMul.hSMul (β := Y) (φ (φ' m)) ((f : (a : X) → Y) (g x) : Y))
have 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))
Tactic: rw [k]
-- 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
φ' : 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
⊢ g (HSMul.hSMul (β := Y) (φ (φ' m)) ((f : (a : X) → Y) (g x) : Y)) = g ((f : (a : X) → Y) (φ' m • g x))
have 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))
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
φ' : 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
⊢ g ((f : (a : X) → Y) (φ' m • g x)) = φ' m • g x
have rw : φ' m • g x = φ' m • g x
Tactic: rw [h₁]
-- 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
φ' : 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₂).comp f = MulActionHom.id M
have 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)
Tactic: ext
-- 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
φ' : 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)
⊢ f.comp (f.inverse' g k₂ h₁ h₂) = MulActionHom.id N
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ f = g
have 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
Tactic: rcases f with ⟨tF, _, _⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' : A →ₑ*[φ] B } = g
have 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 }
Tactic: rcases g with ⟨tG, _, _⟩
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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 })
⊢ { toMulActionHom := tF, map_one' := map_one', map_mul' := map_mul' : A →ₑ*[φ] B } =
    { toMulActionHom := tG, map_one' := map_one'_1, map_mul' := map_mul'_1 }
have 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 }
Tactic: cases tF
Cleared hypotheses: tF, map_one', map_mul', h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ f = g
have a : ∀ (a : A), Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ f = g
have a : ∀ (a : A), Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ Eq.{u_5 + 1} (α := B) ((comp (MulDistribMulActionHom.id N) f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
have 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)
Tactic: rw [comp_apply, id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ Eq.{u_5 + 1} (α := B) ((comp (MulDistribMulActionHom.id N) f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
have rw₁ : Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
Tactic: rw [comp_apply, id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ Eq.{u_5 + 1} (α := B) ((f.comp (MulDistribMulActionHom.id M) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
have 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)
Tactic: rw [comp_apply, id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ Eq.{u_5 + 1} (α := B) ((f.comp (MulDistribMulActionHom.id M) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
have rw₁ : Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
Tactic: rw [comp_apply, id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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')
⊢ f = g
have a : ∀ (x : R), Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') x : N') ((g : (a : R) → N') x : N')
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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
⊢ Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') x : N') ((g : (a : R) → N') x : N')
have a : Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') (x * 1) : N') ((g : (a : R) → N') (x * 1) : N')
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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')
⊢ Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') x : N') ((g : (a : R) → N') x : N')
have 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')
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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')
⊢ Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') x : N') ((g : (a : R) → N') x : N')
have 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)
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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)
⊢ Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') x : N') ((g : (a : R) → N') x : N')
have 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')
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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')
⊢ Eq.{u_13 + 1} (α := N') ((f : (a : R) → N') x : N') ((g : (a : R) → N') x : N')
have 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')
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
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'
R : Type u_10
inst_15 : Semiring R
inst_16 : MulSemiringAction M R
R' : Type u_11
inst_17 : Ring R'
inst_18 : MulSemiringAction M R'
S : Type u_12
inst_19 : Semiring S
inst_20 : MulSemiringAction N S
S' : Type u_13
inst_21 : Ring S'
inst_22 : MulSemiringAction N S'
T : Type u_14
inst_23 : Semiring T
inst_24 : MulSemiringAction P T
f g : R →ₑ+*[φ] S
h : Eq (α := (a : R) → S) ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun) f) ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun) g)
⊢ f = g
have rcases : ∀ (tF : MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S) (map_zero' : tF.toFun 0 = 0)
  (map_add' : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y)
  (map_one' : { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun 1 = 1)
  (map_mul' :
    ∀ (x y : R),
      { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun (x * y) =
        { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun x *
          { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun y)
  (h :
    Eq (α := (a : R) → S)
      ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun)
        { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add', map_one' := map_one',
          map_mul' := map_mul' })
      ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun) g)),
  { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add', map_one' := map_one', map_mul' := map_mul' :
      R →ₑ+*[φ] S } =
    g
Tactic: rcases f with ⟨⟨tF, _, _⟩, _, _⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ Eq.{u_12 + 1} (α := S) ((comp (MulSemiringActionHom.id N) f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
have rw : Eq.{u_12 + 1} (α := S) ((MulSemiringActionHom.id N : (a : S) → S) ((f : (a : R) → S) x : S) : S)
  ((f : (a : R) → S) x : S)
Tactic: rw [comp_apply, id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
rw :
  Eq.{u_12 + 1} (α := S) ((MulSemiringActionHom.id N : (a : S) → S) ((f : (a : R) → S) x : S) : S)
    ((f : (a : R) → S) x : S)
⊢ Eq.{u_12 + 1} (α := S) ((comp (MulSemiringActionHom.id N) f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
have rw₁ : Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
Tactic: rw [comp_apply, id_apply]