awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → MulOneClass (α i)
inst_1 : (i : ι) → Pow (α i) ℕ
inst_2 : ∀ (i : ι), NatPowAssoc.{u_3} (α i)
x : (i : ι) → α i
h : ∀ (x_1 : ι), HPow.hPow (β := ℕ) x 1 x_1 = x x_1
⊢ HPow.hPow (β := ℕ) x 1 = x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → MulOneClass (α i)
inst_1 : (i : ι) → Pow (α i) ℕ
inst_2 : ∀ (i : ι), NatPowAssoc.{u_3} (α i)
x : (i : ι) → α i
x_1 : ι
⊢ HPow.hPow (β := ℕ) x 1 x_1 = x x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x x_1 : ℕ
x_2 : M × N
fst : (x_2 ^ (x + x_1)).1 = (x_2 ^ x * x_2 ^ x_1).1
snd : (x_2 ^ (x + x_1)).2 = (x_2 ^ x * x_2 ^ x_1).2
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x x_1 : ℕ
x_2 : M × N
⊢ (x_2 ^ (x + x_1)).1 = (x_2 ^ x * x_2 ^ x_1).1

Tactic:
simp [npow_add]

Premises used: npow_add
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x x_1 : ℕ
x_2 : M × N
⊢ (x_2 ^ (x + x_1)).2 = (x_2 ^ x * x_2 ^ x_1).2

Tactic:
simp [npow_add]

Premises used: npow_add
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
fst : (HPow.hPow (β := ℕ) x 0).1 = 1.1
snd : (HPow.hPow (β := ℕ) x 0).2 = 1.2
⊢ HPow.hPow (β := ℕ) x 0 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
⊢ (HPow.hPow (β := ℕ) x 0).1 = 1.1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
⊢ (HPow.hPow (β := ℕ) x 0).2 = 1.2

Tactic:
simp
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
fst : (HPow.hPow (β := ℕ) x 1).1 = x.1
snd : (HPow.hPow (β := ℕ) x 1).2 = x.2
⊢ HPow.hPow (β := ℕ) x 1 = x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
⊢ (HPow.hPow (β := ℕ) x 1).1 = x.1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
⊢ (HPow.hPow (β := ℕ) x 1).2 = x.2

Tactic:
simp
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℕ
⊢ (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0

Tactic:
simp only [pow_zero, Nat.cast_one, npow_zero]

Premises used: npow_zero, pow_zero, Nat.cast_one
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
ih : (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
succ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
succ₁ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₂ :
  HMul.hMul (α := R) (↑(n ^ m) : R) (↑(HPow.hPow (β := ℕ) n 1) : R) =
    HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₃ :
  HPow.hPow (α := R) (↑n : R) m * (↑(HPow.hPow (β := ℕ) n 1) : R) =
    HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₄ :
  HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₅ succ₆ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * (↑n : R)
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)

Tactic:
rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]

Premises used: npow_one, Nat.cast_mul, npow_add
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
zero : (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
succ :
  ∀ (m : ℕ) (ih : (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m),
    (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
⊢ (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m

Tactic:
induction m with
  | zero => simp only [pow_zero, Nat.cast_one, npow_zero]
  | succ m ih => rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]

Premises used: npow_one, npow_zero, pow_zero, Nat.cast_mul, npow_add, Nat.zero, Nat.succ, Nat.cast_one
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
rw : (↑1 : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
rw₁ : Eq.{u_2 + 1} (α := R) (↑1 : R) 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := R) 1 1
⊢ (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0

Tactic:
rw [pow_zero, npow_zero, Int.cast_one]

Premises used: npow_zero, pow_zero, Int.cast_one
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
m : ℕ
rw : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₁ : (↑(n ^ m * n) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₂ : HMul.hMul (α := R) (↑(n ^ m) : R) (↑n : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₃ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₄ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
rw₅ rw₆ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * (↑n : R)
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)

Tactic:
rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]

Premises used: npow_one, Int.cast_mul, npow_add
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : AddZeroClass α
⊢ Eq.{u_1 + 1} (α := α) (unop 0) 0

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : AddZeroClass α
⊢ Eq.{u_1 + 1} (α := α) (unop 0) 0

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : AddMonoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 0) 0

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : AddMonoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 0) 0

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : SubNegMonoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 0) 0

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : SubNegMonoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 0) 0

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : AddGroup α
⊢ Eq.{u_1 + 1} (α := α) (unop 0) 0

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : AddGroup α
⊢ Eq.{u_1 + 1} (α := α) (unop 0) 0

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : DivInvMonoid α
x : ℕ
x_1 : αᵐᵒᵖ
rw : HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₁ : unop x_1 ^ x.succ = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₂ : unop x_1 * unop x_1 ^ x = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₃ : unop x_1 * unop x_1 ^ x = unop x_1 * unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)))
rw₄ : unop x_1 * unop x_1 ^ x = unop x_1 * HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)
rw₅ rw₆ : unop x_1 * unop x_1 ^ x = unop x_1 * unop x_1 ^ x
⊢ unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ))) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)

Tactic:
rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]

Premises used: zpow_natCast, MulOpposite.unop_mul, MulOpposite.unop_op, pow_succ'
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Monoid α
x : α
n : ℕ
⊢ op (x ^ n) = op x ^ n

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Monoid α
x : αᵐᵒᵖ
n : ℕ
⊢ unop (x ^ n) = unop x ^ n

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : DivInvMonoid α
x : α
z : ℤ
⊢ op (x ^ z) = op x ^ z

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : DivInvMonoid α
x : αᵐᵒᵖ
z : ℤ
⊢ unop (x ^ z) = unop x ^ z

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : DivInvMonoid α
x y : αᵐᵒᵖ
⊢ unop (x / y) = (unop y)⁻¹ * unop x

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : DivInvMonoid α
x y : α
⊢ op (x / y) = (op y)⁻¹ * op x

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Mul α
a x y : α
⊢ SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y

Tactic:
simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]

Premises used: SemiconjBy, eq_comm, MulOpposite.op_inj, MulOpposite.op_mul
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Mul α
a x y : αᵐᵒᵖ
rw : SemiconjBy (unop a) (unop y) (unop x)
| SemiconjBy a x y

Tactic:
rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]

Premises used: MulOpposite.op_unop, MulOpposite.semiconjBy_op
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Mul α
a x y : αᵐᵒᵖ
conv_rhs : SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
conv_rhs₁ : SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy (unop a) (unop y) (unop x)
⊢ SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y

Tactic:
conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]

Premises used: MulOpposite.op_unop, MulOpposite.semiconjBy_op
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Mul α
a x y : α
h : SemiconjBy a x y
⊢ SemiconjBy (op a) (op y) (op x)

Tactic:
semiconjBy_op.2 h

Premises used: Iff.mpr, MulOpposite.semiconjBy_op
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Mul α
a x y : αᵐᵒᵖ
h : SemiconjBy a x y
⊢ SemiconjBy (unop a) (unop y) (unop x)

Tactic:
semiconjBy_unop.2 h

Premises used: Iff.mpr, MulOpposite.semiconjBy_unop
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Mul α
x y : α
h : Commute x y
⊢ Commute (op x) (op y)

Tactic:
SemiconjBy.op h

Premises used: Commute, SemiconjBy.op
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Mul α
x y : αᵐᵒᵖ
h : Commute x y
⊢ Commute (unop x) (unop y)

Tactic:
h.unop

Premises used: SemiconjBy.unop, Commute
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Mul α
x y : α
⊢ Commute (op x) (op y) ↔ Commute x y

Tactic:
semiconjBy_op

Premises used: Commute, MulOpposite.semiconjBy_op
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Mul α
x y : αᵐᵒᵖ
⊢ Commute (unop x) (unop y) ↔ Commute x y

Tactic:
semiconjBy_unop

Premises used: Commute, MulOpposite.semiconjBy_unop
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : MulOne α
simp_rw :
  (∀ (a a_1 : α),
      HMul.hMul (α := αᵐᵒᵖ) (β := αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a : αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a_1 : αᵐᵒᵖ) =
          1 →
        HMul.hMul (α := αᵐᵒᵖ) (β := αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a_1 : αᵐᵒᵖ)
            ((opEquiv : (a : α) → αᵐᵒᵖ) a : αᵐᵒᵖ) =
          1) ↔
    ∀ {a b : α}, a * b = 1 → b * a = 1
⊢ IsDedekindFiniteMonoid.{u_1} αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α

Tactic:
simp_rw [isDedekindFiniteMonoid_iff, ← opEquiv.forall_congr_right]

Premises used: MulOpposite.opEquiv, isDedekindFiniteMonoid_iff, Equiv.forall_congr_right
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : MulOne α
⊢ (∀ (a a_1 : α),
      HMul.hMul (α := αᵐᵒᵖ) (β := αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a : αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a_1 : αᵐᵒᵖ) =
          1 →
        HMul.hMul (α := αᵐᵒᵖ) (β := αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a_1 : αᵐᵒᵖ)
            ((opEquiv : (a : α) → αᵐᵒᵖ) a : αᵐᵒᵖ) =
          1) ↔
    ∀ {a b : α}, a * b = 1 → b * a = 1

Tactic:
simpa [← op_one, ← op_mul] using forall_comm

Premises used: forall_comm, MulOpposite.op_one, MulOpposite.op_mul
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : MulOne α
inst_1 : IsDedekindFiniteMonoid α
⊢ IsDedekindFiniteMonoid.{u_1} αᵐᵒᵖ

Tactic:
MulOpposite.isDedekindFiniteMonoid_iff.mpr ‹_›

Premises used: Iff.mpr, MulOpposite.isDedekindFiniteMonoid_iff
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : MulOneClass α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : MulOneClass α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : β
⊢ op (a ^ b) = op a ^ b

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : αᵃᵒᵖ
b : β
⊢ unop (a ^ b) = unop a ^ b

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Monoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Monoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : CommMonoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : DivInvMonoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : DivInvMonoid α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Group α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Group α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : CommGroup α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : CommGroup α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Opposite
Goal:
α : Type u_1
inst : Monoid α
inst_1 : IsMulTorsionFree α
⊢ IsMulTorsionFree.{u_1} αᵐᵒᵖ

Tactic:
⟨fun _ h ↦ op_injective.comp <| (pow_left_injective h).comp <| unop_injective⟩

Premises used: pow_left_injective, IsMulTorsionFree.mk, AddOpposite.op_injective, Function.Injective.comp, AddOpposite.unop_injective
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
k n : ℕ+
x : M
⊢ x ^ (k + n) = x ^ k * x ^ n

Tactic:
PNatPowAssoc.ppow_add k n x

Premises used: PNatPowAssoc.ppow_add
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
⊢ HPow.hPow (β := ℕ+) x 1 = x

Tactic:
PNatPowAssoc.ppow_one x

Premises used: PNatPowAssoc.ppow_one
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
k m n : ℕ+
x : M
⊢ x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)

Tactic:
simp only [← ppow_add, add_assoc]

Premises used: add_assoc, ppow_add
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
m n : ℕ+
x : M
⊢ x ^ m * x ^ n = x ^ n * x ^ m

Tactic:
simp only [← ppow_add, add_comm]

Premises used: add_comm, ppow_add
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m : ℕ+
one : x ^ (m * 1) = x ^ m
one₁ one₂ : x ^ m = x ^ m
⊢ x ^ (m * 1) = HPow.hPow (β := ℕ+) (x ^ m) 1

Tactic:
rw [ppow_one, mul_one]

Premises used: ppow_one, mul_one
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
succ : x ^ (m * (k + 1)) = (x ^ m) ^ k * HPow.hPow (β := ℕ+) (x ^ m) 1
succ₁ : x ^ (m * (k + 1)) = (x ^ m) ^ k * x ^ m
succ₂ : x ^ (m * k + m * 1) = (x ^ m) ^ k * x ^ m
succ₃ : x ^ (m * k) * x ^ (m * 1) = (x ^ m) ^ k * x ^ m
succ₄ : x ^ (m * k) * x ^ m = (x ^ m) ^ k * x ^ m
succ₅ succ₆ : (x ^ m) ^ k * x ^ m = (x ^ m) ^ k * x ^ m
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)

Tactic:
rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]

Premises used: ppow_one, mul_add, mul_one, ppow_add
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m n : ℕ+
one : x ^ (m * 1) = HPow.hPow (β := ℕ+) (x ^ m) 1
succ : ∀ (k : ℕ+) (hk : x ^ (m * k) = (x ^ m) ^ k), x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)
⊢ x ^ (m * n) = (x ^ m) ^ n

Tactic:
induction n with
  | one => rw [ppow_one, mul_one]
  | succ k hk => rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]

Premises used: ppow_one, mul_add, mul_one, ppow_add
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m n : ℕ+
rw : x ^ (n * m) = (x ^ n) ^ m
⊢ x ^ (m * n) = (x ^ n) ^ m

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (n * m) = (x ^ n) ^ m

Tactic:
ppow_mul x n m

Premises used: ppow_mul
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (n * m) = (x ^ n) ^ m

Tactic:
exact ppow_mul x n m

Premises used: ppow_mul
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Mul (α i)
inst_1 : (i : ι) → Pow (α i) ℕ+
inst_2 : ∀ (i : ι), PNatPowAssoc.{u_3} (α i)
x x_1 : ℕ+
x_2 : (i : ι) → α i
h : ∀ (x_3 : ι), (x_2 ^ (x + x_1)) x_3 = (x_2 ^ x * x_2 ^ x_1) x_3
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Mul (α i)
inst_1 : (i : ι) → Pow (α i) ℕ+
inst_2 : ∀ (i : ι), PNatPowAssoc.{u_3} (α i)
x x_1 : ℕ+
x_2 : (i : ι) → α i
x_3 : ι
⊢ (x_2 ^ (x + x_1)) x_3 = (x_2 ^ x * x_2 ^ x_1) x_3

Tactic:
simp [ppow_add]

Premises used: ppow_add
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Mul (α i)
inst_1 : (i : ι) → Pow (α i) ℕ+
inst_2 : ∀ (i : ι), PNatPowAssoc.{u_3} (α i)
x : (i : ι) → α i
h : ∀ (x_1 : ι), HPow.hPow (β := ℕ+) x 1 x_1 = x x_1
⊢ HPow.hPow (β := ℕ+) x 1 = x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Mul (α i)
inst_1 : (i : ι) → Pow (α i) ℕ+
inst_2 : ∀ (i : ι), PNatPowAssoc.{u_3} (α i)
x : (i : ι) → α i
x_1 : ι
⊢ HPow.hPow (β := ℕ+) x 1 x_1 = x x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x x_1 : ℕ+
x_2 : M × N
fst : (x_2 ^ (x + x_1)).1 = (x_2 ^ x * x_2 ^ x_1).1
snd : (x_2 ^ (x + x_1)).2 = (x_2 ^ x * x_2 ^ x_1).2
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x x_1 : ℕ+
x_2 : M × N
⊢ (x_2 ^ (x + x_1)).1 = (x_2 ^ x * x_2 ^ x_1).1

Tactic:
simp [ppow_add]

Premises used: ppow_add
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x x_1 : ℕ+
x_2 : M × N
⊢ (x_2 ^ (x + x_1)).2 = (x_2 ^ x * x_2 ^ x_1).2

Tactic:
simp [ppow_add]

Premises used: ppow_add
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x : M × N
fst : (HPow.hPow (β := ℕ+) x 1).1 = x.1
snd : (HPow.hPow (β := ℕ+) x 1).2 = x.2
⊢ HPow.hPow (β := ℕ+) x 1 = x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x : M × N
⊢ (HPow.hPow (β := ℕ+) x 1).1 = x.1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x : M × N
⊢ (HPow.hPow (β := ℕ+) x 1).2 = x.2

Tactic:
simp
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
one : x = x ^ (↑1 : ℕ)
one₁ : x = HPow.hPow (β := ℕ) x 1
one₂ one₃ : x = x
⊢ HPow.hPow (β := ℕ+) x 1 = x ^ (↑1 : ℕ)

Tactic:
rw [ppow_one, PNat.one_coe, pow_one]

Premises used: PNat.one_coe, ppow_one, pow_one
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ (↑k : ℕ)
succ : x ^ k * HPow.hPow (β := ℕ+) x 1 = x ^ (↑(k + 1) : ℕ)
succ₁ : x ^ k * x = x ^ (↑(k + 1) : ℕ)
succ₂ : x ^ k * x = x ^ ((↑k : ℕ) + (↑1 : ℕ))
succ₃ : x ^ k * x = x ^ (↑k : ℕ) * x ^ (↑1 : ℕ)
succ₄ : x ^ k * x = x ^ (↑k : ℕ) * HPow.hPow (β := ℕ) x 1
succ₅ : x ^ k * x = x ^ (↑k : ℕ) * x
succ₆ succ₇ : x ^ k * x = x ^ k * x
⊢ x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)

Tactic:
rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]

Premises used: pow_add, PNat.one_coe, PNat.add_coe, ppow_one, pow_one, ppow_add
-- Module: Mathlib.Algebra.Group.PNatPowAssoc
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
n : ℕ+
one : HPow.hPow (β := ℕ+) x 1 = x ^ (↑1 : ℕ)
succ : ∀ (k : ℕ+) (hk : x ^ k = x ^ (↑k : ℕ)), x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)
⊢ x ^ n = x ^ (↑n : ℕ)

Tactic:
induction n with
  | one => rw [ppow_one, PNat.one_coe, pow_one]
  | succ k hk => rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]

Premises used: pow_add, PNat.one_coe, PNat.add_coe, ppow_one, pow_one, ppow_add
-- Module: Mathlib.Algebra.Group.PUnit
Goal:
⊢ 1 = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.PUnit
Goal:
x y : PUnit
⊢ x * y = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.PUnit
Goal:
x y : PUnit
⊢ x / y = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.PUnit
Goal:
x : PUnit
⊢ x⁻¹ = unit

Tactic:
rfl

Premises used: rfl