awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
      m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
bit : m * n * npowRec' k' (n * n) = m * (npowRec' (2 * k') n * n)
bit₁ : m * n * npowRec' k' (n * n) = m * (npowRec' k' (n * n) * n)
bit₂ : m * n * npowRec' (2 * k') n = m * (npowRec' (2 * k') n * n)
bit₃ : m * n * npowRec' (2 * k') n = m * (n * npowRec' (2 * k') n)
bit₄ bit₅ : m * (n * npowRec' (2 * k') n) = m * (n * npowRec' (2 * k') n)
⊢ m * n * npowRec' k' (n * n) = m * npowRec' (2 * k' + 1) n

Tactic:
rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]

Premises used: npowRec'_two_mul, npowRec'_succ, mul_assoc, npowRec'_mul_comm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
k' : ℕ
hk : k' ≠ 0
zero :
  ∀ (m n : M) (hk : Ne (α := ℕ) 0 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) 0 m n =
      m * npowRec' 0 n
one :
  ∀ (m n : M) (hk : Ne (α := ℕ) 1 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) 1 m n =
      m * npowRec' 1 n
bit :
  ∀ (b : Bool) (k' : ℕ) (k'0 : k' ≠ 0)
    (ih :
      ∀ (m n : M) (hk : k' ≠ 0),
        Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
            (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
          m * npowRec' k' n)
    (m n : M) (hk : Nat.bit b k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) (Nat.bit b k') m
        n =
      m * npowRec' (Nat.bit b k') n
⊢ Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
      (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
    m * npowRec' k' n

Tactic:
induction k' using Nat.binaryRecFromOne generalizing n m with
  | zero => simp at hk
  | one => simp [npowRec']
  | bit b k' k'0 ih =>
    rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]
    cases b <;> simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]
    rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]

Premises used: Nat.bit, npowRec'_two_mul, npowRec', npowRec'_succ, mul_assoc, npowRec'_mul_comm, cond_true, Or.inl, cond_false, Nat.binaryRec_eq
-- Module: Mathlib.Algebra.Group.Defs
Goal:
h : ∀ (M : Type u_2) (x : Semigroup M) (x_1 : One M) (k : ℕ) (m : M), npowRecAuto k m = npowBinRecAuto k m
⊢ @npowRecAuto = @npowBinRecAuto

Tactic:
funext M _ _ k m
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
x : Semigroup M
x_1 : One M
k : ℕ
m : M
rw : 1 = npowBinRec.go 0 1 m
rw₁ :
  Eq.{u_2 + 1} (α := M) (1 : M)
    (Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x_2 : M) ↦ fn (bif bn then y * x_2 else y) (x_2 * x_2)) 0 1 m :
      M)
rw₂ rw₃ : Eq.{u_2 + 1} (α := M) 1 1
⊢ npowRec 0 m = npowBinRec.go 0 1 m

Tactic:
rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]

Premises used: npowRec, Nat.binaryRec_zero, npowBinRec.go
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
x : Semigroup M
x_1 : One M
k_1 : ℕ
m : M
k : ℕ
rw : npowRec (k + 1) m = 1 * npowRec' (k + 1) m
rw₁ rw₂ : 1 * npowRec' (k + 1) m = 1 * npowRec' (k + 1) m
⊢ npowRec (k + 1) m = npowBinRec.go (k + 1) 1 m

Tactic:
rw [npowBinRec.go_spec, npowRec_eq]

Premises used: npowBinRec.go_spec, npowRec_eq
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
x : Semigroup M
x_1 : One M
k : ℕ
m : M
⊢ npowRec k m = npowBinRec.go k 1 m

Tactic:
match k with
  | 0 => rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
  | k + 1 => rw [npowBinRec.go_spec, npowRec_eq]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
m : M
⊢ npowBinRec 0 m = 1

Tactic:
rfl

Premises used: WellFounded.Nat.fix, npowBinRec, dite, WellFounded.Nat.fix.go, npowBinRec.go, Nat.binaryRec, rfl
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
n : ℕ
m : M
rw : npowRecAuto (n + 1) m = npowBinRec n m * m
⊢ npowBinRec (n + 1) m = npowBinRec n m * m

Tactic:
rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]

Premises used: npowRec_eq_npowBinRec, npowBinRecAuto
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
n : ℕ
m : M
rw : npowRecAuto (n + 1) m = npowRecAuto n m * m
⊢ npowRecAuto (n + 1) m = npowBinRec n m * m

Tactic:
rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]

Premises used: npowRec_eq_npowBinRec, npowBinRecAuto
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
n : ℕ
m : M
iterate : npowRecAuto (n + 1) m = npowRecAuto n m * m
⊢ npowBinRec (n + 1) m = npowBinRec n m * m

Tactic:
iterate 2 rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]

Premises used: npowRec_eq_npowBinRec, npowBinRecAuto
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowRecAuto n m * m

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
x : M
⊢ Monoid.npow n x = x ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
rw : b = 1 * c
rw₁ : b = b * a * c
rw₂ : b = b * (a * c)
rw₃ : b = b * 1
rw₄ rw₅ : b = b
⊢ b = c

Tactic:
rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]

Premises used: mul_assoc, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
⊢ HPow.hPow (β := ℕ) a 0 = 1

Tactic:
Monoid.npow_zero _

Premises used: Monoid.npow_zero
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
Monoid.npow_succ n a

Premises used: Monoid.npow_succ
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
rw : HPow.hPow (β := ℕ) a 0 * a = a
rw₁ : 1 * a = a
rw₂ rw₃ : a = a
⊢ HPow.hPow (β := ℕ) a 1 = a

Tactic:
rw [pow_succ, pow_zero, one_mul]

Premises used: pow_succ, pow_zero, one_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
⊢ a ^ HAdd.hAdd (α := ℕ) 0 1 = a * HPow.hPow (β := ℕ) a 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
rw : a ^ (n + 1 + 1) = a * (a ^ n * a)
rw₁ : a ^ (n + 1) * a = a * (a ^ n * a)
rw₂ : a * a ^ n * a = a * (a ^ n * a)
rw₃ rw₄ : a * (a ^ n * a) = a * (a ^ n * a)
⊢ a ^ (n + 1 + 1) = a * a ^ (n + 1)

Tactic:
rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a b : M
⊢ HPow.hPow (β := ℕ) (a * b) 0 * a = a * HPow.hPow (β := ℕ) (b * a) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a b : M
n : ℕ
ih : (a * b) ^ n * a = a * (b * a) ^ n
⊢ (a * b) ^ (n + 1) * a = a * (b * a) ^ (n + 1)

Tactic:
simp [pow_succ', ← ih, mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a b : M
n : ℕ
zero : HPow.hPow (β := ℕ) (a * b) 0 * a = a * HPow.hPow (β := ℕ) (b * a) 0
succ : ∀ (n : ℕ) (ih : (a * b) ^ n * a = a * (b * a) ^ n), (a * b) ^ (n + 1) * a = a * (b * a) ^ (n + 1)
⊢ (a * b) ^ n * a = a * (b * a) ^ n

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [pow_succ', ← ih, mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
rw : a ^ (n + 1) = a * a ^ n
rw₁ rw₂ : a * a ^ n = a * a ^ n
⊢ a ^ n * a = a * a ^ n

Tactic:
rw [← pow_succ, pow_succ']

Premises used: pow_succ, pow_succ'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
rw : HPow.hPow (β := ℕ) a 1 * a = a * a
rw₁ rw₂ : a * a = a * a
⊢ HPow.hPow (β := ℕ) a 2 = a * a

Tactic:
rw [pow_succ, pow_one]

Premises used: pow_succ, pow_one
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
rw : HPow.hPow (β := ℕ) a 2 * a = a * a * a
rw₁ rw₂ : a * a * a = a * a * a
⊢ HPow.hPow (β := ℕ) a 3 = a * a * a

Tactic:
rw [pow_succ, pow_two]

Premises used: pow_two, pow_succ
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
rw : a * HPow.hPow (β := ℕ) a 2 = a * (a * a)
rw₁ rw₂ : a * (a * a) = a * (a * a)
⊢ HPow.hPow (β := ℕ) a 3 = a * (a * a)

Tactic:
rw [pow_succ', pow_two]

Premises used: pow_two, pow_succ'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
rw : HPow.hPow (α := M) 1 n * 1 = 1
rw₁ : HMul.hMul (α := M) 1 1 = 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := M) 1 1
⊢ HPow.hPow (α := M) 1 (n + 1) = 1

Tactic:
rw [pow_succ, one_pow, one_mul]

Premises used: pow_succ, one_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
m : ℕ
rw : a ^ m = a ^ m * HPow.hPow (β := ℕ) a 0
rw₁ : a ^ m = a ^ m * 1
rw₂ rw₃ : a ^ m = a ^ m
⊢ a ^ (m + 0) = a ^ m * HPow.hPow (β := ℕ) a 0

Tactic:
rw [Nat.add_zero, pow_zero, mul_one]

Premises used: pow_zero, Nat.add_zero, mul_one
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m + (n + 1)) = a ^ m * (a ^ n * a)
rw₁ : a ^ (m + (n + 1)) = a ^ m * a ^ n * a
rw₂ : a ^ (m + (n + 1)) = a ^ (m + n) * a
rw₃ : a ^ (m + (n + 1)) = a ^ (m + n + 1)
rw₄ rw₅ : a ^ (m + (n + 1)) = a ^ (m + (n + 1))
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]

Premises used: pow_succ, mul_assoc, Nat.add_assoc
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m + n) = a ^ n * a ^ m
rw₁ : a ^ (m + n) = a ^ (n + m)
rw₂ rw₃ : a ^ (n + m) = a ^ (n + m)
⊢ a ^ m * a ^ n = a ^ n * a ^ m

Tactic:
rw [← pow_add, ← pow_add, Nat.add_comm]

Premises used: pow_add, Nat.add_comm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
m : ℕ
rw : HPow.hPow (β := ℕ) a 0 = HPow.hPow (β := ℕ) (a ^ m) 0
rw₁ : 1 = HPow.hPow (β := ℕ) (a ^ m) 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := M) 1 1
⊢ a ^ (m * 0) = HPow.hPow (β := ℕ) (a ^ m) 0

Tactic:
rw [Nat.mul_zero, pow_zero, pow_zero]

Premises used: pow_zero, Nat.mul_zero
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m * n + m) = (a ^ m) ^ (n + 1)
rw₁ : a ^ (m * n) * a ^ m = (a ^ m) ^ (n + 1)
rw₂ : a ^ (m * n) * a ^ m = (a ^ m) ^ n * a ^ m
rw₃ rw₄ : (a ^ m) ^ n * a ^ m = (a ^ m) ^ n * a ^ m
⊢ a ^ (m * (n + 1)) = (a ^ m) ^ (n + 1)

Tactic:
rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]

Premises used: Nat.mul_succ, pow_succ, pow_add
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (n * m) = (a ^ n) ^ m
rw₁ rw₂ : (a ^ n) ^ m = (a ^ n) ^ m
⊢ a ^ (m * n) = (a ^ n) ^ m

Tactic:
rw [Nat.mul_comm, pow_mul]

Premises used: Nat.mul_comm, pow_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m * n) = (a ^ n) ^ m
rw₁ : a ^ (n * m) = (a ^ n) ^ m
rw₂ rw₃ : (a ^ n) ^ m = (a ^ n) ^ m
⊢ (a ^ m) ^ n = (a ^ n) ^ m

Tactic:
rw [← pow_mul, Nat.mul_comm, pow_mul]

Premises used: Nat.mul_comm, pow_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a b : M
reg : IsLeftRegular a
eq : a * b = 1
⊢ Eq.{u_2 + 1} (α := M) ((fun (x : M) ↦ a * x) (b * a)) ((fun (x : M) ↦ a * x) 1)

Tactic:
simp [← mul_assoc, eq]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
a b : M
reg : IsRightRegular a
eq : b * a = 1
⊢ Eq.{u_2 + 1} (α := M) ((fun (x : M) ↦ x * a) (a * b)) ((fun (x : M) ↦ x * a) 1)

Tactic:
simp [mul_assoc, eq]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), y * z = 1
x y : M
h : x * y = 1
have : ∀ (z : M) (hz : y * z = 1), y * x = 1
⊢ y * x = 1

Tactic:
have ⟨z, hz⟩ := ex x y h
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), y * z = 1
x y : M
h : x * y = 1
z : M
hz : y * z = 1
⊢ x = z

Tactic:
simpa [← mul_assoc, h] using congr_arg (x * ·) hz.symm

Premises used: HMul.hMul, mul_assoc, congr_arg, Eq.symm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), y * z = 1
x y : M
h : x * y = 1
z : M
hz : y * z = 1
rwa rwa₁ rwa₂ rwa₃ : y * z = 1
⊢ y * x = 1

Tactic:
rwa [show x = z by simpa [← mul_assoc, h] using congr_arg (x * ·) hz.symm]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), z * x = 1
x y : M
h : x * y = 1
have : ∀ (z : M) (hz : z * x = 1), y * x = 1
⊢ y * x = 1

Tactic:
have ⟨z, hz⟩ := ex x y h
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
⊢ y = z

Tactic:
simpa [mul_assoc, h] using congr_arg (· * y) hz.symm

Premises used: HMul.hMul, mul_assoc, congr_arg, Eq.symm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
rwa rwa₁ rwa₂ rwa₃ : z * x = 1
⊢ y * x = 1

Tactic:
rwa [show y = z by simpa [mul_assoc, h] using congr_arg (· * y) hz.symm]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
M : Type u_2
inst : CommMonoid M
⊢ IsDedekindFiniteMonoid M

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : InvolutiveInv G
a : G
⊢ a⁻¹⁻¹ = a

Tactic:
InvolutiveInv.inv_inv _

Premises used: InvolutiveInv.inv_inv
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_2
inst : Pow G ℤ
inst_1 : IsCyclic G
⊢ ∃ (g : G), Surjective.{1, u_2 + 1} (β := G) fun (x : ℤ) ↦ g ^ x

Tactic:
IsCyclic.exists_zpow_surjective

Premises used: IsCyclic.exists_zpow_surjective
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
n : ℤ
x : G
⊢ DivInvMonoid.zpow n x = x ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
⊢ HPow.hPow (β := ℤ) a 0 = 1

Tactic:
DivInvMonoid.zpow_zero' a

Premises used: DivInvMonoid.zpow_zero'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
n : ℕ
⊢ HPow.hPow (β := ℤ) a (OfNat.ofNat n) = HPow.hPow (β := ℕ) a (OfNat.ofNat n)

Tactic:
zpow_natCast ..

Premises used: zpow_natCast
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
n : ℕ
rw : a ^ Int.negSucc n = (HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ))⁻¹
⊢ a ^ Int.negSucc n = (a ^ (n + 1))⁻¹

Tactic:
rw [← zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ))⁻¹

Tactic:
DivInvMonoid.zpow_neg' n a

Premises used: DivInvMonoid.zpow_neg'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ))⁻¹

Tactic:
exact DivInvMonoid.zpow_neg' n a

Premises used: DivInvMonoid.zpow_neg'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_2
inst : SubNegMonoid G
a : G
n : ℕ
rw : Int.negSucc n • a = -HSMul.hSMul (α := ℤ) (↑(n + 1) : ℤ) a
⊢ Int.negSucc n • a = -((n + 1) • a)

Tactic:
rw [← natCast_zsmul]

Premises used: natCast_zsmul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_2
inst : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -HSMul.hSMul (α := ℤ) (↑(n + 1) : ℤ) a

Tactic:
SubNegMonoid.zsmul_neg' n a

Premises used: SubNegMonoid.zsmul_neg'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_2
inst : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -HSMul.hSMul (α := ℤ) (↑(n + 1) : ℤ) a

Tactic:
exact SubNegMonoid.zsmul_neg' n a

Premises used: SubNegMonoid.zsmul_neg'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a b : G
⊢ a / b = a * b⁻¹

Tactic:
DivInvMonoid.div_eq_mul_inv _ _

Premises used: DivInvMonoid.div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
x : G
rw : x⁻¹ = 1 * x⁻¹
rw₁ rw₂ : x⁻¹ = x⁻¹
⊢ x⁻¹ = 1 / x

Tactic:
rw [div_eq_mul_inv, one_mul]

Premises used: div_eq_mul_inv, one_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a b c : G
rw : a * b * c⁻¹ = a * (b / c)
rw₁ : a * b * c⁻¹ = a * (b * c⁻¹)
rw₂ rw₃ : a * (b * c⁻¹) = a * (b * c⁻¹)
⊢ a * b / c = a * (b / c)

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _]

Premises used: mul_assoc, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
⊢ 1 / a = a⁻¹

Tactic:
(inv_eq_one_div a).symm

Premises used: inv_eq_one_div, Eq.symm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
rw : HPow.hPow (β := ℕ) a 1 = a
rw₁ rw₂ : a = a
⊢ HPow.hPow (β := ℤ) a 1 = a

Tactic:
rw [zpow_ofNat, pow_one]

Premises used: zpow_ofNat, pow_one
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
rw : HPow.hPow (β := ℕ) a 2 = a * a
rw₁ rw₂ : a * a = a * a
⊢ HPow.hPow (β := ℤ) a 2 = a * a

Tactic:
rw [zpow_ofNat, pow_two]

Premises used: pow_two, zpow_ofNat
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivInvMonoid G
x : G
⊢ HPow.hPow (β := ℤ) x (-1) = x⁻¹

Tactic:
(zpow_negSucc x 0).trans <| congr_arg Inv.inv (pow_one x)

Premises used: zpow_negSucc, congr_arg, Inv.inv, pow_one, OfNat.ofNat, Int.neg, Eq.trans, Int.negOfNat
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : InvOneClass G
⊢ Eq.{u_1 + 1} (α := G) 1⁻¹ 1

Tactic:
InvOneClass.inv_one

Premises used: InvOneClass.inv_one
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
DivisionMonoid.mul_inv_rev _ _

Premises used: DivisionMonoid.mul_inv_rev
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
⊢ a * b = 1 → a⁻¹ = b

Tactic:
DivisionMonoid.inv_eq_of_mul _ _

Premises used: DivisionMonoid.inv_eq_of_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
h : a * b = 1
rw : a⁻¹⁻¹ = a
rw₁ rw₂ : a = a
⊢ b⁻¹ = a

Tactic:
rw [← inv_eq_of_mul_eq_one_right h, inv_inv]

Premises used: inv_inv, inv_eq_of_mul_eq_one_right
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
h : a * b = 1
⊢ a = b⁻¹

Tactic:
(inv_eq_of_mul_eq_one_left h).symm

Premises used: Eq.symm, inv_eq_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a : G
⊢ a⁻¹ * a = 1

Tactic:
Group.inv_mul_cancel a

Premises used: Group.inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a b : G
h : a * b = 1
⊢ a⁻¹ = b

Tactic:
left_inv_eq_right_inv (inv_mul_cancel a) h

Premises used: inv_mul_cancel, left_inv_eq_right_inv
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a : G
rw : a * a⁻¹ = a⁻¹⁻¹ * a⁻¹
rw₁ rw₂ : a * a⁻¹ = a * a⁻¹
⊢ a * a⁻¹ = 1

Tactic:
rw [← inv_mul_cancel a⁻¹, inv_eq_of_mul (inv_mul_cancel a)]

Premises used: inv_mul_cancel, Inv.inv, _private.0.inv_eq_of_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a : G
rw : a * a⁻¹ = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := G) 1 1
⊢ a / a = 1

Tactic:
rw [div_eq_mul_inv, mul_inv_cancel a]

Premises used: div_eq_mul_inv, mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a⁻¹ * a * b = b
rw₁ : 1 * b = b
rw₂ rw₃ : b = b
⊢ a⁻¹ * (a * b) = b

Tactic:
rw [← mul_assoc, inv_mul_cancel, one_mul]

Premises used: inv_mul_cancel, mul_assoc, one_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * a⁻¹ * b = b
rw₁ : 1 * b = b
rw₂ rw₃ : b = b
⊢ a * (a⁻¹ * b) = b

Tactic:
rw [← mul_assoc, mul_inv_cancel, one_mul]

Premises used: mul_assoc, mul_inv_cancel, one_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * (b * b⁻¹) = a
rw₁ : a * 1 = a
rw₂ rw₃ : a = a
⊢ a * b * b⁻¹ = a

Tactic:
rw [mul_assoc, mul_inv_cancel, mul_one]

Premises used: mul_assoc, mul_inv_cancel, mul_one
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * b * b⁻¹ = a
rw₁ rw₂ : a = a
⊢ a * b / b = a

Tactic:
rw [div_eq_mul_inv, mul_inv_cancel_right a b]

Premises used: mul_inv_cancel_right, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * (b⁻¹ * b) = a
rw₁ : a * 1 = a
rw₂ rw₃ : a = a
⊢ a * b⁻¹ * b = a

Tactic:
rw [mul_assoc, inv_mul_cancel, mul_one]

Premises used: inv_mul_cancel, mul_assoc, mul_one
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * b⁻¹ * b = a
rw₁ rw₂ : a = a
⊢ a / b * b = a

Tactic:
rw [div_eq_mul_inv, inv_mul_cancel_right a b]

Premises used: div_eq_mul_inv, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a_1 b a : G
⊢ a⁻¹⁻¹ = a

Tactic:
inv_eq_of_mul (inv_mul_cancel a)

Premises used: inv_mul_cancel, _private.0.inv_eq_of_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a_1 b a : G
⊢ a⁻¹⁻¹ = a

Tactic:
exact inv_eq_of_mul (inv_mul_cancel a)

Premises used: inv_mul_cancel, _private.0.inv_eq_of_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b : G
h : a * b * (b⁻¹ * a⁻¹) = 1
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
apply inv_eq_of_mul

Premises used: _private.0.inv_eq_of_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b : G
h : a * (b * (b⁻¹ * a⁻¹)) = 1
h₁ : a * a⁻¹ = 1
h₂ h₃ : Eq.{u_1 + 1} (α := G) 1 1
⊢ a * b * (b⁻¹ * a⁻¹) = 1

Tactic:
rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]

Premises used: mul_assoc, mul_inv_cancel, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a b x x_1 : G
⊢ x * x_1 = 1 → x⁻¹ = x_1

Tactic:
inv_eq_of_mul

Premises used: _private.0.inv_eq_of_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a b x x_1 : G
⊢ x * x_1 = 1 → x⁻¹ = x_1

Tactic:
exact inv_eq_of_mul

Premises used: _private.0.inv_eq_of_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b c : G
h : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) c)
rw : a⁻¹ * (a * b) = c
rw₁ : a⁻¹ * (a * c) = c
rw₂ rw₃ : c = c
⊢ b = c

Tactic:
rw [← inv_mul_cancel_left a b, show a * b = a * c from h, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b c : G
h : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ x * a) b) ((fun (x : G) ↦ x * a) c)
rw : b * a * a⁻¹ = c
rw₁ : c * a * a⁻¹ = c
rw₂ rw₃ : c = c
⊢ b = c

Tactic:
rw [← mul_inv_cancel_right b a, show b * a = c * a from h, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : CommGroup G
a b : G
rw : a * (a⁻¹ * b) = b
rw₁ rw₂ : b = b
⊢ a⁻¹ * b * a = b

Tactic:
rw [mul_comm, mul_inv_cancel_left]

Premises used: mul_comm, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : CommGroup G
a b : G
rw : a⁻¹ * (a * b) = b
rw₁ rw₂ : b = b
⊢ a * b * a⁻¹ = b

Tactic:
rw [mul_comm, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, mul_comm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : CommGroup G
a b : G
rw : b * a * a⁻¹ = b
rw₁ rw₂ : b = b
⊢ a⁻¹ * (b * a) = b

Tactic:
rw [mul_comm, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, mul_comm