awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Even
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
r : α
h_1 : b = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) r : β) ((f : (a : α) → β) r : β)
⊢ Membership.mem (γ := Set α) {a : α | IsSquare a} (r * r) ∧ (f : (a : α) → β) (r * r) = b

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Even
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
r : α
h_1 : 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:
exact ⟨r * r, by simp [*]⟩
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Monoid α
a : α
⊢ IsSquare a ↔ ∃ (r : α), a = HPow.hPow (β := ℕ) r 2

Tactic:
simp [IsSquare, pow_two]

Premises used: pow_two, IsSquare
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Monoid α
r : α
⊢ IsSquare (HPow.hPow (β := ℕ) r 2)

Tactic:
⟨r, pow_two _⟩

Premises used: pow_two, IsSquare, Exists.intro
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Monoid α
a : α
n : ℕ
ha : IsSquare a
⊢ IsSquare (a ^ n)

Tactic:
aesop (add simp Commute.mul_pow)

Premises used: Commute.mul_pow
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
hn : Even n
⊢ ∀ (a : α), IsSquare (a ^ n)

Tactic:
aesop (add simp pow_add)

Premises used: pow_add
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : CommSemigroup α
a b : α
h : IsSquare a
h_1 : IsSquare b
r : α
h_2 : a = r * r
s : α
h_3 : b = s * s
⊢ a * b = r * s * (r * s)

Tactic:
simp_all [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
mp : IsSquare a⁻¹ → IsSquare a
mpr : IsSquare a → IsSquare a⁻¹
⊢ IsSquare a⁻¹ ↔ IsSquare a

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a

Tactic:
simpa using (isSquare_op_iff.mpr h).map (MulEquiv.inv' α).symm

Premises used: Iff.mpr, IsSquare.map, MulEquiv.inv', isSquare_op_iff, MulEquiv.symm
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹

Tactic:
simpa using (isSquare_op_iff.mpr h).map (MulEquiv.inv' α).symm

Premises used: Iff.mpr, IsSquare.map, MulEquiv.inv', isSquare_op_iff, MulEquiv.symm
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
n : ℤ
⊢ IsSquare a → IsSquare (a ^ n)

Tactic:
aesop (add simp Commute.mul_zpow)

Premises used: Commute.mul_zpow
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a / b)

Tactic:
aesop (add simp div_eq_mul_inv)

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Group α
n : ℤ
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)

Tactic:
aesop (add simp zpow_add)

Premises used: zpow_add
-- Module: Mathlib.Algebra.Group.Even
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst : CommGroup G
a b c d e : G
ha : IsSquare a
n : ℕ
k : ℤ
hk : Even k
⊢ IsSquare (a * (b * b) / HPow.hPow (β := ℕ) c 2 * d ^ k * e ^ (n + n))

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Even
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst : AddCommGroup G
a b c d e : G
ha : Even a
n : ℕ
k : ℤ
hk : Even k
⊢ Even (a + (b + b) - HSMul.hSMul (α := ℕ) 2 c + k • d + (n + n) • e)

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
b : β
⊢ Function.Even.{u_1, u_2} (β := β) fun (x : α) ↦ b

Tactic:
fun _ ↦ rfl

Premises used: Function.Even, rfl
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
inst_1 : Zero β
⊢ Function.Even.{u_1, u_2} (β := β) fun (x : α) ↦ 0

Tactic:
Even.const 0

Premises used: Function.Even.const, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
inst_1 : NegZeroClass β
⊢ Function.Odd.{u_1, u_2} (β := β) fun (x : α) ↦ 0

Tactic:
fun _ ↦ neg_zero.symm

Premises used: Function.Odd, Eq.symm, neg_zero
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
γ : Type u_3
g : α → β
hg : Function.Even g
f : β → γ
⊢ Function.Even (f ∘ g)

Tactic:
(congr_arg f <| hg ·)

Premises used: Function.Even, congr_arg
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
γ : Type u_3
inst_1 : Neg β
f : β → γ
hf : Function.Even f
g : α → β
hg : Function.Odd g
a : α
⊢ (f ∘ g) (-a) = (f ∘ g) a

Tactic:
simp only [comp_apply, hg a, hf _]

Premises used: Function.comp_apply
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
γ : Type u_3
inst_1 : Neg β
inst_2 : Neg γ
f : β → γ
hf : Function.Odd f
g : α → β
hg : Function.Odd g
a : α
⊢ (f ∘ g) (-a) = -(f ∘ g) a

Tactic:
simp only [comp_apply, hg a, hf _]

Premises used: Function.comp_apply
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
inst_1 : Add β
f g : α → β
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f + g) (-a) = (f + g) a

Tactic:
simp only [hf a, hg a, Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
inst_1 : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f + g) (-a) = -(f + g) a

Tactic:
simp only [hf a, hg a, Pi.add_apply, neg_add]

Premises used: neg_add, Pi.add_apply
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst_1 : SMul β γ
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f • g) (-a) = (f • g) a

Tactic:
simp only [Pi.smul_apply', hf a, hg a]

Premises used: Pi.smul_apply'
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst_1 : Monoid β
inst_2 : AddGroup γ
inst_3 : DistribMulAction β γ
hf : Function.Even f
hg : Function.Odd g
a : α
⊢ (f • g) (-a) = -(f • g) a

Tactic:
simp only [Pi.smul_apply', hf a, hg a, smul_neg]

Premises used: Pi.smul_apply', smul_neg
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst_1 : Ring β
inst_2 : AddCommGroup γ
inst_3 : Module β γ
hf : Function.Odd f
hg : Function.Even g
a : α
⊢ (f • g) (-a) = -(f • g) a

Tactic:
simp only [Pi.smul_apply', hf a, hg a, neg_smul]

Premises used: neg_smul, Pi.smul_apply'
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst_1 : Ring β
inst_2 : AddCommGroup γ
inst_3 : Module β γ
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f • g) (-a) = (f • g) a

Tactic:
simp only [Pi.smul_apply', hf a, hg a, smul_neg, neg_smul, neg_neg]

Premises used: neg_smul, Pi.smul_apply', neg_neg, smul_neg
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
γ : Type u_3
g : α → γ
inst_1 : SMul β γ
hg : Function.Even g
r : β
a : α
⊢ (r • g) (-a) = (r • g) a

Tactic:
simp only [Pi.smul_apply, hg a]

Premises used: Pi.smul_apply
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
β : Type u_2
inst : Neg α
γ : Type u_3
g : α → γ
inst_1 : Monoid β
inst_2 : AddGroup γ
inst_3 : DistribMulAction β γ
hg : Function.Odd g
r : β
a : α
⊢ (r • g) (-a) = -(r • g) a

Tactic:
simp only [Pi.smul_apply, hg a, smul_neg]

Premises used: smul_neg, Pi.smul_apply
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
inst : Neg α
R : Type u_3
inst_1 : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f * g) (-a) = (f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a]

Premises used: Pi.mul_apply
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
inst : Neg α
R : Type u_3
inst_1 : Mul R
f g : α → R
inst_2 : HasDistribNeg R
hf : Function.Even f
hg : Function.Odd g
a : α
⊢ (f * g) (-a) = -(f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a, mul_neg]

Premises used: Pi.mul_apply, mul_neg
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
inst : Neg α
R : Type u_3
inst_1 : Mul R
f g : α → R
inst_2 : HasDistribNeg R
hf : Function.Odd f
hg : Function.Even g
a : α
⊢ (f * g) (-a) = -(f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a, neg_mul]

Premises used: Pi.mul_apply, neg_mul
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_1
inst : Neg α
R : Type u_3
inst_1 : Mul R
f g : α → R
inst_2 : HasDistribNeg R
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f * g) (-a) = (f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a, mul_neg, neg_mul, neg_neg]

Premises used: Pi.mul_apply, neg_neg, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_3
β : Type u_4
inst : AddCommGroup β
inst_1 : IsAddTorsionFree β
f : α → β
inst_2 : Neg α
he : Function.Even f
ho : Function.Odd f
h : ∀ (r : α), f r = 0 r
⊢ f = 0

Tactic:
ext r
-- Module: Mathlib.Algebra.Group.EvenFunction
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
h₃ h₄ : f r = f r
⊢ f r = 0 r

Tactic:
rw [Pi.zero_apply, ← neg_eq_self, ← ho, he]

Premises used: neg_eq_self, Pi.zero_apply
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_3
β : Type u_4
inst : AddCommGroup β
inst_1 : IsAddTorsionFree β
inst_2 : InvolutiveNeg α
f : α → β
hf : Function.Odd f
s : Finset α
hs : Finset.map (Equiv.toEmbedding (Equiv.neg α)) s = s
⊢ s.sum f = 0

Tactic:
simpa [neg_eq_self, funext hf, hs] using (Finset.sum_map s (Equiv.neg α).toEmbedding f).symm

Premises used: neg_eq_self, Equiv.neg, Finset.sum_map, funext, Equiv.toEmbedding, Eq.symm
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_3
β : Type u_4
inst : AddCommGroup β
inst_1 : IsAddTorsionFree β
inst_2 : Fintype α
inst_3 : InvolutiveNeg α
f : α → β
hf : Function.Odd f
⊢ Eq.{u_4 + 1} (α := β) (∑ a : α, f a) 0

Tactic:
hf.finsetSum_eq_zero <| Finset.map_univ_equiv (Equiv.neg α)

Premises used: Equiv.neg, Finset.map_univ_equiv, Function.Odd.finsetSum_eq_zero
-- Module: Mathlib.Algebra.Group.EvenFunction
Goal:
α : Type u_3
β : Type u_4
inst : AddCommGroup β
inst_1 : IsAddTorsionFree β
f : α → β
inst_2 : NegZeroClass α
hf : Function.Odd f
⊢ f 0 = 0

Tactic:
simp [← neg_eq_self, ← hf 0]

Premises used: neg_eq_self, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
m₁ m₂ : Monoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := MulOneClass M) toMulOneClass toMulOneClass

Tactic:
have : m₁.toMulOneClass = m₂.toMulOneClass := MulOneClass.ext h_mul
-- Module: Mathlib.Algebra.Group.Ext
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
⊢ Eq.{u + 1} (α := M) One.one One.one

Tactic:
have h₁ : m₁.one = m₂.one := congr_arg (·.one) this
-- Module: Mathlib.Algebra.Group.Ext
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' := ⋯ }
h : ∀ (n : ℕ) (x : M), Monoid.npow n x = Monoid.npow n x
⊢ Eq.{u + 1} (α := ℕ → M → M) Monoid.npow Monoid.npow

Tactic:
ext n x
-- Module: Mathlib.Algebra.Group.Ext
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' := ⋯ }
n : ℕ
x : M
⊢ Monoid.npow n x = Monoid.npow n x

Tactic:
@MonoidHom.map_pow M M m₁ m₂ f x n

Premises used: MonoidHom.map_pow
-- Module: Mathlib.Algebra.Group.Ext
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' := ⋯ }
n : ℕ
x : M
⊢ Monoid.npow n x = Monoid.npow n x

Tactic:
exact @MonoidHom.map_pow M M m₁ m₂ f x n

Premises used: MonoidHom.map_pow
-- Module: Mathlib.Algebra.Group.Ext
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

Tactic:
have : m₁.npow = m₂.npow := by
    ext n x
    exact @MonoidHom.map_pow M M m₁ m₂ f x n
-- Module: Mathlib.Algebra.Group.Ext
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
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₂
⊢ m₁ = m₂

Tactic:
rcases m₁ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
m₂ : Monoid M
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_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
⊢ { 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:
congr
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toMonoid : Monoid M
mul_comm : ∀ (a b : M), a * b = b * a
toMonoid_1 : Monoid M
mul_comm_1 : ∀ (a b : M), a * b = b * a
h : Eq.{u + 1} (α := Monoid M) CommMonoid.toMonoid CommMonoid.toMonoid
⊢ { toMonoid := toMonoid, mul_comm := mul_comm : CommMonoid M } = { toMonoid := toMonoid_1, mul_comm := mul_comm_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : CommMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
⊢ m₁ = m₂

Tactic:
CommMonoid.toMonoid_injective <| Monoid.ext h_mul

Premises used: CommMonoid.toMonoid_injective, Monoid.ext
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
toIsLeftCancelMul : IsLeftCancelMul M
toSemigroup_1 : Semigroup M
toOne_1 : One M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_1 : ℕ → M → M
npow_zero_1 : ∀ (x : M), npow_1 0 x = 1
npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x * x
toIsLeftCancelMul_1 : IsLeftCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
e_toMonoid : toSemigroup = toSemigroup_1
e_toMonoid₁ : toOne = toOne_1
e_toMonoid₂ : npow = npow_1
⊢ Eq.{u + 1} (α := LeftCancelMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, toIsLeftCancelMul := toIsLeftCancelMul }
    { toSemigroup := toSemigroup_1, toOne := toOne_1, one_mul := one_mul_1, mul_one := mul_one_1, npow := npow_1,
      npow_zero := npow_zero_1, npow_succ := npow_succ_1, toIsLeftCancelMul := toIsLeftCancelMul_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
toIsLeftCancelMul : IsLeftCancelMul M
toSemigroup_1 : Semigroup M
toOne_1 : One M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_1 : ℕ → M → M
npow_zero_1 : ∀ (x : M), npow_1 0 x = 1
npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x * x
toIsLeftCancelMul_1 : IsLeftCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
⊢ toSemigroup = toSemigroup_1

Tactic:
injection h
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
toIsLeftCancelMul : IsLeftCancelMul M
toSemigroup_1 : Semigroup M
toOne_1 : One M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_1 : ℕ → M → M
npow_zero_1 : ∀ (x : M), npow_1 0 x = 1
npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x * x
toIsLeftCancelMul_1 : IsLeftCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
⊢ toOne = toOne_1

Tactic:
injection h
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
toIsLeftCancelMul : IsLeftCancelMul M
toSemigroup_1 : Semigroup M
toOne_1 : One M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_1 : ℕ → M → M
npow_zero_1 : ∀ (x : M), npow_1 0 x = 1
npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x * x
toIsLeftCancelMul_1 : IsLeftCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
⊢ npow = npow_1

Tactic:
injection h
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
m₁ m₂ : LeftCancelMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
⊢ m₁ = m₂

Tactic:
LeftCancelMonoid.toMonoid_injective <| Monoid.ext h_mul

Premises used: Monoid.ext, LeftCancelMonoid.toMonoid_injective
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
toIsRightCancelMul : IsRightCancelMul M
toSemigroup_1 : Semigroup M
toOne_1 : One M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_1 : ℕ → M → M
npow_zero_1 : ∀ (x : M), npow_1 0 x = 1
npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x * x
toIsRightCancelMul_1 : IsRightCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
e_toMonoid : toSemigroup = toSemigroup_1
e_toMonoid₁ : toOne = toOne_1
e_toMonoid₂ : npow = npow_1
⊢ Eq.{u + 1} (α := RightCancelMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, toIsRightCancelMul := toIsRightCancelMul }
    { toSemigroup := toSemigroup_1, toOne := toOne_1, one_mul := one_mul_1, mul_one := mul_one_1, npow := npow_1,
      npow_zero := npow_zero_1, npow_succ := npow_succ_1, toIsRightCancelMul := toIsRightCancelMul_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
toIsRightCancelMul : IsRightCancelMul M
toSemigroup_1 : Semigroup M
toOne_1 : One M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_1 : ℕ → M → M
npow_zero_1 : ∀ (x : M), npow_1 0 x = 1
npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x * x
toIsRightCancelMul_1 : IsRightCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
⊢ toSemigroup = toSemigroup_1

Tactic:
injection h
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
toIsRightCancelMul : IsRightCancelMul M
toSemigroup_1 : Semigroup M
toOne_1 : One M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_1 : ℕ → M → M
npow_zero_1 : ∀ (x : M), npow_1 0 x = 1
npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x * x
toIsRightCancelMul_1 : IsRightCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
⊢ toOne = toOne_1

Tactic:
injection h
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
toIsRightCancelMul : IsRightCancelMul M
toSemigroup_1 : Semigroup M
toOne_1 : One M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_1 : ℕ → M → M
npow_zero_1 : ∀ (x : M), npow_1 0 x = 1
npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x * x
toIsRightCancelMul_1 : IsRightCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
⊢ npow = npow_1

Tactic:
injection h
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
m₁ m₂ : RightCancelMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
⊢ m₁ = m₂

Tactic:
RightCancelMonoid.toMonoid_injective <| Monoid.ext h_mul

Premises used: Monoid.ext, RightCancelMonoid.toMonoid_injective
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toLeftCancelMonoid : LeftCancelMonoid M
toIsRightCancelMul : IsRightCancelMul M
toLeftCancelMonoid_1 : LeftCancelMonoid M
toIsRightCancelMul_1 : IsRightCancelMul M
h : Eq.{u + 1} (α := LeftCancelMonoid M) CancelMonoid.toLeftCancelMonoid CancelMonoid.toLeftCancelMonoid
⊢ Eq.{u + 1} (α := CancelMonoid M)
    { toLeftCancelMonoid := toLeftCancelMonoid, toIsRightCancelMul := toIsRightCancelMul }
    { toLeftCancelMonoid := toLeftCancelMonoid_1, toIsRightCancelMul := toIsRightCancelMul_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : CancelMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
⊢ m₁ = m₂

Tactic:
CancelMonoid.toLeftCancelMonoid_injective <| LeftCancelMonoid.ext h_mul

Premises used: CancelMonoid.toLeftCancelMonoid_injective, LeftCancelMonoid.ext
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
m₁ m₂ : CancelMonoid M
h : Eq.{u + 1} (α := RightCancelMonoid M) toRightCancelMonoid toRightCancelMonoid
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
⊢ m₁ = m₂

Tactic:
apply CancelMonoid.ext

Premises used: CancelMonoid.ext
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
m₁ m₂ : CancelMonoid M
h : Eq.{u + 1} (α := RightCancelMonoid M) toRightCancelMonoid toRightCancelMonoid
⊢ Eq (α := M → M → M) HMul.hMul HMul.hMul

Tactic:
congrArg (fun m : Monoid M => (letI := m; HMul.hMul : M → M → M)) <|
    congrArg (@RightCancelMonoid.toMonoid M) h

Premises used: HMul.hMul, congrArg, RightCancelMonoid.toMonoid