awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Add A
inst_1 : AddGroup G
g₁ g₂ : G
⊢ Eq.{u_3 + 1} (α := AddAut G)
    ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
        ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
          { toFun := fun (h : G) ↦ g₁ + g₂ + h + -(g₁ + g₂), invFun := fun (h : G) ↦ -(g₁ + g₂) + h + (g₁ + g₂),
            left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) :
      AddAut G)
    ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
        (HAdd.hAdd (α := Additive (AddAut G)) (β := Additive (AddAut G))
          ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
              { toFun := fun (h : G) ↦ g₁ + h + -g₁, invFun := fun (h : G) ↦ -g₁ + h + g₁, left_inv := ⋯,
                right_inv := ⋯, map_add' := ⋯ } :
            Additive (AddAut G))
          ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
              { toFun := fun (h : G) ↦ g₂ + h + -g₂, invFun := fun (h : G) ↦ -g₂ + h + g₂, left_inv := ⋯,
                right_inv := ⋯, map_add' := ⋯ } :
            Additive (AddAut G))) :
      AddAut G)
have a : ∀ (h : G),
  Eq (α := G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
              ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                { toFun := fun (h : G) ↦ g₁ + g₂ + h + -(g₁ + g₂), invFun := fun (h : G) ↦ -(g₁ + g₂) + h + (g₁ + g₂),
                  left_inv := sorry, right_inv := sorry, map_add' := sorry }) :
            AddAut G) :
          (a : G) → G)
        h :
      G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
              (HAdd.hAdd (α := Additive (AddAut G)) (β := Additive (AddAut G))
                ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                    { toFun := fun (h : G) ↦ g₁ + h + -g₁, invFun := fun (h : G) ↦ -g₁ + h + g₁, left_inv := sorry,
                      right_inv := sorry, map_add' := sorry } :
                  Additive (AddAut G))
                ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                    { toFun := fun (h : G) ↦ g₂ + h + -g₂, invFun := fun (h : G) ↦ -g₂ + h + g₂, left_inv := sorry,
                      right_inv := sorry, map_add' := sorry } :
                  Additive (AddAut G))) :
            AddAut G) :
          (a : G) → G)
        h :
      G)
Tactic: ext h
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Add A
inst_1 : AddGroup G
g₁ g₂ h : G
⊢ Eq (α := G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
              ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                { toFun := fun (h : G) ↦ g₁ + g₂ + h + -(g₁ + g₂), invFun := fun (h : G) ↦ -(g₁ + g₂) + h + (g₁ + g₂),
                  left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) :
            AddAut G) :
          (a : G) → G)
        h :
      G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
              (HAdd.hAdd (α := Additive (AddAut G)) (β := Additive (AddAut G))
                ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                    { toFun := fun (h : G) ↦ g₁ + h + -g₁, invFun := fun (h : G) ↦ -g₁ + h + g₁, left_inv := ⋯,
                      right_inv := ⋯, map_add' := ⋯ } :
                  Additive (AddAut G))
                ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                    { toFun := fun (h : G) ↦ g₂ + h + -g₂, invFun := fun (h : G) ↦ -g₂ + h + g₂, left_inv := ⋯,
                      right_inv := ⋯, map_add' := ⋯ } :
                  Additive (AddAut G))) :
            AddAut G) :
          (a : G) → G)
        h :
      G)
have a : g₁ + g₂ + h + -(g₁ + g₂) = g₁ + (g₂ + h + -g₂) + -g₁
Tactic: change g₁ + g₂ + h + -(g₁ + g₂) = g₁ + (g₂ + h + -g₂) + -g₁
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N_1 : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P_1 : Type u_12
Q_1 : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst_1 : Mul P
inst_2 : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
⊢ (fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P))
      ((fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q)) h) =
    h
have h₁ : ∀ (x : M),
  (fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P))
      ((fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q)) h) x =
    h x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N_1 : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P_1 : Type u_12
Q_1 : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst_1 : Mul P
inst_2 : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
⊢ (fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q))
      ((fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P)) k) =
    k
have h : ∀ (x : N),
  (fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q))
      ((fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P)) k) x =
    k x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N_1 : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P_1 : Type u_12
Q_1 : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst_1 : Mul P
inst_2 : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
⊢ (fun (n : N) ↦ (g : (a : P) → Q) ((h * k) ((f.symm : (a : N) → M) n))) =
    HMul.hMul (α := N → Q) (fun (n : N) ↦ (g : (a : P) → Q) (h ((f.symm : (a : N) → M) n))) fun (n : N) ↦
      (g : (a : P) → Q) (k ((f.symm : (a : N) → M) n))
have h₁ : ∀ (x : N),
  (g : (a : P) → Q) ((h * k) ((f.symm : (a : N) → M) x)) =
    HMul.hMul (α := N → Q) (β := N → Q) (fun (n : N) ↦ (g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)))
      (fun (n : N) ↦ (g : (a : P) → Q) (k ((f.symm : (a : N) → M) n))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : M₁ ≃* M₂
f : M₁ →* N
⊢ (fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) ((fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) f) = f
have h : ∀ (x : M₁),
  Eq.{u_8 + 1} (α := N)
    (((fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) ((fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) f) : (a : M₁) → N) x :
      N)
    ((f : (a : M₁) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : M₁ ≃* M₂
f : M₂ →* N
⊢ (fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) ((fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) f) = f
have h : ∀ (x : M₂),
  Eq.{u_8 + 1} (α := N)
    (((fun (f : M₁ →* N) ↦ f.comp e.symm.toMonoidHom) ((fun (f : M₂ →* N) ↦ f.comp e.toMonoidHom) f) : (a : M₂) → N) x :
      N)
    ((f : (a : M₂) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₁
⊢ e.symm.toMonoidHom.comp (e.toMonoidHom.comp f) = f
have h : ∀ (x : M),
  Eq.{u_9 + 1} (α := N₁) ((e.symm.toMonoidHom.comp (e.toMonoidHom.comp f) : (a : M) → N₁) x : N₁)
    ((f : (a : M) → N₁) x : N₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : Monoid N
inst_6 : Monoid N₁
inst_7 : Monoid N₂
inst_8 : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₂
⊢ e.toMonoidHom.comp (e.symm.toMonoidHom.comp f) = f
have h : ∀ (x : M),
  Eq.{u_10 + 1} (α := N₂) ((e.toMonoidHom.comp (e.symm.toMonoidHom.comp f) : (a : M) → N₂) x : N₂)
    ((f : (a : M) → N₂) x : N₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : CommMonoid N
inst_6 : CommMonoid N₁
inst_7 : CommMonoid N₂
inst_8 : CommMonoid N₃
e : M₁ ≃* M₂
f g : M₁ →* N
⊢ Equiv.toFun e.monoidHomCongrLeftEquiv (f * g) =
    Equiv.toFun e.monoidHomCongrLeftEquiv f * Equiv.toFun e.monoidHomCongrLeftEquiv g
have h : ∀ (x : M₂),
  Eq.{u_8 + 1} (α := N) ((Equiv.toFun e.monoidHomCongrLeftEquiv (f * g) : (a : M₂) → N) x : N)
    ((Equiv.toFun e.monoidHomCongrLeftEquiv f * Equiv.toFun e.monoidHomCongrLeftEquiv g : (a : M₂) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : MulOneClass M
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : MulOneClass M₃
inst_5 : CommMonoid N
inst_6 : CommMonoid N₁
inst_7 : CommMonoid N₂
inst_8 : CommMonoid N₃
e : N₁ ≃* N₂
f g : M →* N₁
⊢ Equiv.toFun e.monoidHomCongrRightEquiv (f * g) =
    Equiv.toFun e.monoidHomCongrRightEquiv f * Equiv.toFun e.monoidHomCongrRightEquiv g
have h : ∀ (x : M),
  Eq.{u_10 + 1} (α := N₂) ((Equiv.toFun e.monoidHomCongrRightEquiv (f * g) : (a : M) → N₂) x : N₂)
    ((Equiv.toFun e.monoidHomCongrRightEquiv f * Equiv.toFun e.monoidHomCongrRightEquiv g : (a : M) → N₂) x : N₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F M N
inst_1 : MulOneClass M
inst_2 : MulOneClass N
inst_3 : MulEquivClass F M N
e : F
⊢ HMul.hMul (α := N) (β := N) ((e : (a : M) → N) 1 : N) ((e : (a : M) → N) (EquivLike.inv e 1) : N) =
    (e : (a : M) → N) (EquivLike.inv e 1)
have rw : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) (1 * EquivLike.inv e 1) : N) ((e : (a : M) → N) (EquivLike.inv e 1) : N)
Tactic: rw [← map_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F M N
inst_1 : MulOneClass M
inst_2 : MulOneClass N
inst_3 : MulEquivClass F M N
e : F
rw : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) (1 * EquivLike.inv e 1) : N) ((e : (a : M) → N) (EquivLike.inv e 1) : N)
⊢ HMul.hMul (α := N) (β := N) ((e : (a : M) → N) 1 : N) ((e : (a : M) → N) (EquivLike.inv e 1) : N) =
    (e : (a : M) → N) (EquivLike.inv e 1)
have rw₁ : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) (EquivLike.inv e 1) : N) ((e : (a : M) → N) (EquivLike.inv e 1) : N)
Tactic: rw [← map_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
f g : M ≃* N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g
have mk : ∀ (toEquiv : M ≃ N) (map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
  (h₁ : { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.toFun = g.toFun)
  (h₂ : { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.invFun = g.invFun),
  { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N } = g
Tactic: cases f
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
g : M ≃* N
toEquiv : M ≃ N
map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
h₁ : { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.toFun = g.toFun
h₂ : { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.invFun = g.invFun
⊢ { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N } = g
have mk : ∀ (toEquiv_1 : M ≃ N) (map_mul'_1 : ∀ (x y : M), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y)
  (h₁ :
    { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.toFun =
      { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.toFun)
  (h₂ :
    { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.invFun =
      { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.invFun),
  { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N } = { toEquiv := toEquiv_1, map_mul' := map_mul'_1 }
Tactic: cases g
Cleared hypotheses: g, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
toEquiv : M ≃ N
map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
toEquiv_1 : M ≃ N
map_mul'_1 : ∀ (x y : M), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y
h₁ :
  { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.toFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.toFun
h₂ :
  { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N }.invFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1 : M ≃* N }.invFun
⊢ { toEquiv := toEquiv, map_mul' := map_mul' : M ≃* N } = { toEquiv := toEquiv_1, map_mul' := map_mul'_1 }
have mk : toEquiv = toEquiv_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
h1 : M ≃* N
h2 : N ≃* P
x y : M
⊢ (h2 : (a : N) → P) ((h1 : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
      ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P)
have rw : (h2 : (a : N) → P) (HMul.hMul (α := N) (β := N) ((h1 : (a : M) → N) x : N) ((h1 : (a : M) → N) y : N)) =
  HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
    ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P)
Tactic: rw [map_mul, map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
h1 : M ≃* N
h2 : N ≃* P
x y : M
rw :
  (h2 : (a : N) → P) (HMul.hMul (α := N) (β := N) ((h1 : (a : M) → N) x : N) ((h1 : (a : M) → N) y : N)) =
    HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
      ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P)
⊢ (h2 : (a : N) → P) ((h1 : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
      ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P)
have rw₁ : HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
    ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P) =
  HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
    ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P)
Tactic: rw [map_mul, map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
ι : Type u_9
M : ι → Type u_10
inst_1 : (i : ι) → Mul (M i)
i j : ι
h : i = j
x x_1 : M i
⊢ (Equiv.cast ⋯).toFun (x * x_1) = (Equiv.cast ⋯).toFun x * (Equiv.cast ⋯).toFun x_1
have refl : (Equiv.cast sorry).toFun (x * x_1) = (Equiv.cast sorry).toFun x * (Equiv.cast sorry).toFun x_1
Tactic: cases h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
e : M ≃* N
⊢ Eq (α := N →* N) (MonoidHom.comp (↑e : M →* N) (↑e.symm : N →* M)) (MonoidHom.id N)
have h : ∀ (x : N),
  Eq (α := N) ((MonoidHom.comp (↑e : M →* N) (↑e.symm : N →* M) : (a : N) → N) x : N)
    ((MonoidHom.id N : (a : N) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Equiv.Defs (goal)
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
e : M ≃* N
⊢ Eq (α := M →* M) (MonoidHom.comp (↑e.symm : N →* M) (↑e : M →* N)) (MonoidHom.id M)
have h : ∀ (x : M),
  Eq (α := M) ((MonoidHom.comp (↑e.symm : N →* M) (↑e : M →* N) : (a : M) → M) x : M)
    ((MonoidHom.id M : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Even (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
b : β
h : Membership.mem (γ := Set β) {b : β | IsSquare b} b
s : β
h_1 : b = s * s
⊢ Membership.mem (γ := Set β) (Set.image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) {a : α | IsSquare a}) b
have rcases : ∀ (r : α),
  b = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) r : β) ((f : (a : α) → β) r : β) →
    Membership.mem (γ := Set β) (Set.image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) {a : α | IsSquare a}) b
Tactic: rcases hf s with ⟨r, rfl⟩
Cleared hypotheses: s, h_1
-- Lean 4 proof step from Mathlib.Algebra.Group.Even (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ ↔ IsSquare a
have mp : IsSquare a⁻¹ → IsSquare a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Even (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
mp : IsSquare a⁻¹ → IsSquare a
⊢ IsSquare a⁻¹ ↔ IsSquare a
have mpr : IsSquare a → IsSquare a⁻¹
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.EvenFunction (goal)
Goal:
α : Type u_3
β : Type u_4
inst : AddCommGroup β
inst_1 : IsAddTorsionFree β
f : α → β
inst_2 : Neg α
he : Function.Even f
ho : Function.Odd f
⊢ f = 0
have h : ∀ (r : α), f r = 0 r
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.Group.EvenFunction (goal)
Goal:
α : Type u_3
β : Type u_4
inst : AddCommGroup β
inst_1 : IsAddTorsionFree β
f : α → β
inst_2 : Neg α
he : Function.Even f
ho : Function.Odd f
r : α
⊢ f r = 0 r
have h : f r = 0
Tactic: rw [Pi.zero_apply, ← neg_eq_self, ← ho, he]
-- Lean 4 proof step from Mathlib.Algebra.Group.EvenFunction (goal)
Goal:
α : Type u_3
β : Type u_4
inst : AddCommGroup β
inst_1 : IsAddTorsionFree β
f : α → β
inst_2 : Neg α
he : Function.Even f
ho : Function.Odd f
r : α
h : f r = 0
⊢ f r = 0 r
have h₁ : -f r = f r
Tactic: rw [Pi.zero_apply, ← neg_eq_self, ← ho, he]
-- Lean 4 proof step from Mathlib.Algebra.Group.EvenFunction (goal)
Goal:
α : Type u_3
β : Type u_4
inst : AddCommGroup β
inst_1 : IsAddTorsionFree β
f : α → β
inst_2 : Neg α
he : Function.Even f
ho : Function.Odd f
r : α
h : f r = 0
h₁ : -f r = f r
⊢ f r = 0 r
have h₂ : f (-r) = f r
Tactic: rw [Pi.zero_apply, ← neg_eq_self, ← ho, he]
-- Lean 4 proof step from Mathlib.Algebra.Group.EvenFunction (goal)
Goal:
α : Type u_3
β : Type u_4
inst : AddCommGroup β
inst_1 : IsAddTorsionFree β
f : α → β
inst_2 : Neg α
he : Function.Even f
ho : Function.Odd f
r : α
h : f r = 0
h₁ : -f r = f r
h₂ : f (-r) = f r
⊢ f r = 0 r
have h₃ : f r = f r
Tactic: rw [Pi.zero_apply, ← neg_eq_self, ← ho, he]
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (hypothesis)
Goal:
M : Type u
m₁ m₂ : Monoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
⊢ m₁ = m₂
have this : Eq.{u + 1} (α := MulOneClass M) toMulOneClass toMulOneClass
Tactic: have : m₁.toMulOneClass = m₂.toMulOneClass := MulOneClass.ext h_mul
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (hypothesis)
Goal:
M : Type u
m₁ m₂ : Monoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
this : Eq.{u + 1} (α := MulOneClass M) toMulOneClass toMulOneClass
⊢ m₁ = m₂
have h₁ : Eq.{u + 1} (α := M) One.one One.one
Tactic: have h₁ : m₁.one = m₂.one := congr_arg (·.one) this
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
Goal:
M : Type u
m₁ m₂ : Monoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
this : Eq.{u + 1} (α := MulOneClass M) toMulOneClass toMulOneClass
h₁ : Eq.{u + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ Eq.{u + 1} (α := ℕ → M → M) Monoid.npow Monoid.npow
have h : ∀ (n : ℕ) (x : M), Monoid.npow n x = Monoid.npow n x
Tactic: ext n x
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (hypothesis)
Goal:
M : Type u
m₁ m₂ : Monoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
this : Eq.{u + 1} (α := MulOneClass M) toMulOneClass toMulOneClass
h₁ : Eq.{u + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ m₁ = m₂
have this₁ : Eq.{u + 1} (α := ℕ → M → M) Monoid.npow Monoid.npow
Tactic: have : m₁.npow = m₂.npow := by
    ext n x
    exact @MonoidHom.map_pow M M m₁ m₂ f x n
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
Goal:
M : Type u
m₁ m₂ : Monoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
this_1 : Eq.{u + 1} (α := MulOneClass M) toMulOneClass toMulOneClass
h₁ : Eq.{u + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Eq.{u + 1} (α := ℕ → M → M) Monoid.npow Monoid.npow
⊢ m₁ = m₂
have rcases : ∀ (npow : ℕ → M → M) (mul : M → M → M) (mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c))
  (npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x) (one : M) (npow_zero : ∀ (x : M), npow 0 x = 1)
  (one_mul : ∀ (a : M), 1 * a = a) (mul_one : ∀ (a : M), a * 1 = a) (h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul)
  (this : Eq.{u + 1} (α := MulOneClass M) toMulOneClass toMulOneClass) (h₁ : Eq.{u + 1} (α := M) One.one One.one)
  (this : Eq.{u + 1} (α := ℕ → M → M) Monoid.npow Monoid.npow),
  { mul := mul, mul_assoc := mul_assoc, one := one, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ : Monoid M } =
    m₂
Tactic: rcases m₁ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩
Cleared hypotheses: m₁, h_mul, this_1, h₁, f, this