awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
⊢ 1 = a⁻¹ ↔ a = 1

Tactic:
eq_comm.trans inv_eq_one

Premises used: inv_eq_one, eq_comm, Iff.trans
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
⊢ a⁻¹ ≠ 1 ↔ a ≠ 1

Tactic:
inv_eq_one.not

Premises used: inv_eq_one, Iff.not
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
rw : 1 / (1 / a) = b
rw₁ : 1 / (1 / b) = b
rw₂ rw₃ : b = b
⊢ a = b

Tactic:
rw [← one_div_one_div a, h, one_div_one_div]

Premises used: one_div_one_div
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
rw : a ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) a (↑(m * n) : ℤ)
⊢ a ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) a (↑m : ℤ)) (↑n : ℤ)

Tactic:
rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast]

Premises used: zpow_natCast, pow_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) a (↑(m * n) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
rw : a ^ ((↑m : ℤ) * Int.negSucc n) = (a ^ m) ^ Int.negSucc n
rw₁ : a ^ ((↑m : ℤ) * Int.negSucc n) = ((a ^ m) ^ (n + 1))⁻¹
rw₂ : a ^ ((↑m : ℤ) * Int.negSucc n) = (a ^ (m * (n + 1)))⁻¹
rw₃ : HPow.hPow (β := ℤ) a (-(↑(m * n.succ) : ℤ)) = (a ^ (m * (n + 1)))⁻¹
rw₄ : (HPow.hPow (β := ℤ) a (↑(m * n.succ) : ℤ))⁻¹ = (a ^ (m * (n + 1)))⁻¹
rw₅ : HPow.hPow (β := ℤ) a (↑(m * n.succ) : ℤ) = a ^ (m * (n + 1))
rw₆ rw₇ : HPow.hPow (β := ℤ) a (↑(m * n.succ) : ℤ) = HPow.hPow (β := ℤ) a (↑(m * (n + 1)) : ℤ)
⊢ a ^ ((↑m : ℤ) * Int.negSucc n) = HPow.hPow (β := ℤ) a (↑m : ℤ) ^ Int.negSucc n

Tactic:
rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]

Premises used: zpow_natCast, zpow_negSucc, Int.ofNat_mul_negSucc, pow_mul, inv_inj, zpow_neg
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
rw : a ^ (Int.negSucc m * (↑n : ℤ)) = (a ^ Int.negSucc m) ^ n
rw₁ : a ^ (Int.negSucc m * (↑n : ℤ)) = (a ^ (m + 1))⁻¹ ^ n
rw₂ : a ^ (Int.negSucc m * (↑n : ℤ)) = (a⁻¹ ^ (m + 1)) ^ n
rw₃ : a ^ (Int.negSucc m * (↑n : ℤ)) = a⁻¹ ^ ((m + 1) * n)
rw₄ : HPow.hPow (β := ℤ) a (-(↑(m.succ * n) : ℤ)) = a⁻¹ ^ ((m + 1) * n)
rw₅ : (HPow.hPow (β := ℤ) a (↑(m.succ * n) : ℤ))⁻¹ = a⁻¹ ^ ((m + 1) * n)
rw₆ : (HPow.hPow (β := ℤ) a (↑(m.succ * n) : ℤ))⁻¹ = (a ^ ((m + 1) * n))⁻¹
rw₇ : HPow.hPow (β := ℤ) a (↑(m.succ * n) : ℤ) = a ^ ((m + 1) * n)
rw₈ rw₉ : HPow.hPow (β := ℤ) a (↑(m.succ * n) : ℤ) = HPow.hPow (β := ℤ) a (↑((m + 1) * n) : ℤ)
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)

Tactic:
rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]

Premises used: zpow_natCast, Int.negSucc_mul_ofNat, zpow_negSucc, inv_pow, pow_mul, inv_inj, zpow_neg
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
rw : a ^ HMul.hMul (α := ℤ) (↑m.succ : ℤ) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) a (↑((m + 1) * (n + 1)) : ℤ)
⊢ a ^ (Int.negSucc m * Int.negSucc n) = (a ^ Int.negSucc m) ^ Int.negSucc n

Tactic:
rw [zpow_negSucc, zpow_negSucc, Int.negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ←
      zpow_natCast]

Premises used: zpow_natCast, zpow_negSucc, inv_pow, pow_mul, inv_inv, Int.negSucc_mul_negSucc
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ HMul.hMul (α := ℤ) (↑m.succ : ℤ) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) a (↑((m + 1) * (n + 1)) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
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 [Int.mul_comm, zpow_mul]

Premises used: zpow_mul, Int.mul_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℤ
rw : a ^ (m * n) = (a ^ n) ^ m
rw₁ rw₂ : (a ^ n) ^ m = (a ^ n) ^ m
⊢ (a ^ m) ^ n = (a ^ n) ^ m

Tactic:
rw [← zpow_mul, zpow_mul']

Premises used: zpow_mul', zpow_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b c : α
⊢ a / (b / c) = a * c / b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
⊢ a / b⁻¹ = a * b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b c : α
⊢ a / (b * c) = a / c / b

Tactic:
simp only [mul_assoc, mul_inv_rev, div_eq_mul_inv]

Premises used: mul_assoc, div_eq_mul_inv, mul_inv_rev
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ (a / b)⁻¹ = a⁻¹ / b⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ a / b = b⁻¹ * a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ a⁻¹ * b = b / a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ a⁻¹ / b = b⁻¹ / a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ (a * b)⁻¹ = a⁻¹ / b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ a⁻¹ / b⁻¹ = b / a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ (a⁻¹ / b⁻¹)⁻¹ = a / b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ 1 / a * (1 / b) = 1 / (a * b)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a / b / c = a / c / b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a / b / c = a / (b * c)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a / b * c = a / (b / c)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a * (b / c) = b * (a / c)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a * b / c = a / c * b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a / (b * c) = a / b / c

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a / b * c = a * c / b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
⊢ 1 / a * b = b / a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a / b * c = a * (c / b)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a / b * c = c / b * a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c : α
⊢ a / (b * c) = a / b * (1 / c)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a * d / (b * c)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a / c / (b / d)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c d : α
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b c d : α
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
n : ℕ
simp_rw : (a * b) ^ n = a ^ n * b ^ n
⊢ HPow.hPow (β := ℤ) (a * b) (↑n : ℤ) = HPow.hPow (β := ℤ) a (↑n : ℤ) * HPow.hPow (β := ℤ) b (↑n : ℤ)

Tactic:
simp_rw [zpow_natCast, mul_pow]

Premises used: zpow_natCast, mul_pow
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
n : ℕ
simp_rw : ((a * b) ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * (b ^ (n + 1))⁻¹
simp_rw₁ : (a * b)⁻¹ ^ (n + 1) = a⁻¹ ^ (n + 1) * b⁻¹ ^ (n + 1)
simp_rw₂ : (a⁻¹ * b⁻¹) ^ (n + 1) = a⁻¹ ^ (n + 1) * b⁻¹ ^ (n + 1)
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n

Tactic:
simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]

Premises used: zpow_negSucc, mul_inv, inv_pow, mul_pow
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a / b) ^ n = a ^ n / b ^ n

Tactic:
simp only [div_eq_mul_inv, mul_pow, inv_pow]

Premises used: inv_pow, div_eq_mul_inv, mul_pow
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
n : ℤ
⊢ (a / b) ^ n = a ^ n / b ^ n

Tactic:
simp only [div_eq_mul_inv, mul_zpow, inv_zpow]

Premises used: inv_zpow, mul_zpow, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a * b⁻¹ = b⁻¹ ↔ a = 1
rw₁ rw₂ : a = 1 ↔ a = 1
⊢ a / b = b⁻¹ ↔ a = 1

Tactic:
rw [div_eq_mul_inv, mul_eq_right]

Premises used: mul_eq_right, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
⊢ Surjective (β := G) fun (x : G) ↦ a * x

Tactic:
fun x ↦ ⟨a⁻¹ * x, mul_inv_cancel_left a x⟩

Premises used: HMul.hMul, Inv.inv, Exists.intro, mul_inv_cancel_left, Function.Surjective
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
⊢ Surjective (β := G) fun (x : G) ↦ x * a

Tactic:
fun x ↦
  ⟨x * a⁻¹, inv_mul_cancel_right x a⟩

Premises used: HMul.hMul, Inv.inv, Exists.intro, inv_mul_cancel_right, Function.Surjective
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a * c = b
⊢ a = b * c⁻¹

Tactic:
simp [h.symm]

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b * a = c
⊢ a = b⁻¹ * c

Tactic:
simp [h.symm]

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b = a * c
⊢ a⁻¹ * b = c

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = c * b
⊢ a * b⁻¹ = c

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a * c⁻¹ = b
⊢ a = b * c

Tactic:
simp [h.symm]

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b⁻¹ * a = c
⊢ a = b * c

Tactic:
simp [h.symm, mul_inv_cancel_left]

Premises used: Eq.symm, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b = a⁻¹ * c
rw : a * (a⁻¹ * c) = c
rw₁ rw₂ : c = c
⊢ a * b = c

Tactic:
rw [h, mul_inv_cancel_left]

Premises used: mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = c * b⁻¹
⊢ a * b = c

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
h : a = b⁻¹
rw : b⁻¹ * b = 1
rw₁ rw₂ : Eq.{u_3 + 1} (α := G) 1 1
⊢ a * b = 1

Tactic:
rw [h, inv_mul_cancel]

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a = b⁻¹ ↔ a⁻¹ = b
rw₁ rw₂ : a = b⁻¹ ↔ a = b⁻¹
⊢ a * b = 1 ↔ a⁻¹ = b

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_eq_iff_eq_inv]

Premises used: mul_eq_one_iff_eq_inv, inv_eq_iff_eq_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a⁻¹ = b ↔ b = a⁻¹
rw₁ rw₂ : b = a⁻¹ ↔ b = a⁻¹
⊢ a * b = 1 ↔ b = a⁻¹

Tactic:
rw [mul_eq_one_iff_inv_eq, eq_comm]

Premises used: mul_eq_one_iff_inv_eq, eq_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a = b⁻¹ ↔ b⁻¹ = a
rw₁ rw₂ : b⁻¹ = a ↔ b⁻¹ = a
⊢ a * b = 1 ↔ b⁻¹ = a

Tactic:
rw [mul_eq_one_iff_eq_inv, eq_comm]

Premises used: mul_eq_one_iff_eq_inv, eq_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a = b⁻¹ ↔ a * b = 1

Tactic:
mul_eq_one_iff_eq_inv.symm

Premises used: mul_eq_one_iff_eq_inv, Iff.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a⁻¹ = b ↔ a * b = 1

Tactic:
mul_eq_one_iff_inv_eq.symm

Premises used: mul_eq_one_iff_inv_eq, Iff.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = b * c⁻¹
rw : b * c⁻¹ * c = b
rw₁ rw₂ : b = b
⊢ a * c = b

Tactic:
rw [h, inv_mul_cancel_right]

Premises used: inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a * c = b
rw : a = a * c * c⁻¹
rw₁ rw₂ : a = a
⊢ a = b * c⁻¹

Tactic:
rw [← h, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = b⁻¹ * c
rw : b * (b⁻¹ * c) = c
rw₁ rw₂ : c = c
⊢ b * a = c

Tactic:
rw [h, mul_inv_cancel_left]

Premises used: mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b * a = c
rw : a = b⁻¹ * (b * a)
rw₁ rw₂ : a = a
⊢ a = b⁻¹ * c

Tactic:
rw [← h, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a⁻¹ * b = c
rw : b = a * (a⁻¹ * b)
rw₁ rw₂ : b = b
⊢ b = a * c

Tactic:
rw [← h, mul_inv_cancel_left]

Premises used: mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b = a * c
rw : a⁻¹ * (a * c) = c
rw₁ rw₂ : c = c
⊢ a⁻¹ * b = c

Tactic:
rw [h, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a * b⁻¹ = c
rw : a = a * b⁻¹ * b
rw₁ rw₂ : a = a
⊢ a = c * b

Tactic:
rw [← h, inv_mul_cancel_right]

Premises used: inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = c * b
rw : c * b * b⁻¹ = c
rw₁ rw₂ : c = c
⊢ a * b⁻¹ = c

Tactic:
rw [h, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a = b⁻¹⁻¹ ↔ a = b
rw₁ rw₂ : a = b ↔ a = b
⊢ a * b⁻¹ = 1 ↔ a = b

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_inv]

Premises used: mul_eq_one_iff_eq_inv, inv_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a⁻¹ = b⁻¹ ↔ a = b
rw₁ rw₂ : a = b ↔ a = b
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_inj]

Premises used: mul_eq_one_iff_eq_inv, inv_inj
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a * b = a ↔ b = 1
rw₁ rw₂ : b = 1 ↔ b = 1
⊢ a * b * a⁻¹ = 1 ↔ b = 1

Tactic:
rw [mul_inv_eq_one, mul_eq_left]

Premises used: mul_inv_eq_one, mul_eq_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
b : G
simp : Injective (β := G) fun (a : G) ↦ a * b⁻¹
⊢ Injective (β := G) fun (a : G) ↦ a / b

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
b : G
⊢ Injective (β := G) fun (a : G) ↦ a * b⁻¹

Tactic:
fun a a' h ↦ mul_left_injective b⁻¹ h

Premises used: Inv.inv, mul_left_injective, Function.Injective
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
b : G
⊢ Injective (β := G) fun (a : G) ↦ a * b⁻¹

Tactic:
exact fun a a' h ↦ mul_left_injective b⁻¹ h

Premises used: Inv.inv, mul_left_injective
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
b : G
simp : Injective (β := G) fun (a : G) ↦ b * a⁻¹
⊢ Injective (β := G) fun (a : G) ↦ b / a

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
b : G
⊢ Injective (β := G) fun (a : G) ↦ b * a⁻¹

Tactic:
fun a a' h ↦ inv_injective (mul_right_injective b h)

Premises used: inv_injective, Function.Injective, mul_right_injective
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
b : G
⊢ Injective (β := G) fun (a : G) ↦ b * a⁻¹

Tactic:
exact fun a a' h ↦ inv_injective (mul_right_injective b h)

Premises used: inv_injective, mul_right_injective
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
rw : (b * a / a)⁻¹ = b⁻¹
rw₁ rw₂ : b⁻¹ = b⁻¹
⊢ a / (b * a) = b⁻¹

Tactic:
rw [← inv_div, mul_div_cancel_right]

Premises used: inv_div, mul_div_cancel_right
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : a * c / c / b = a / b
⊢ a * c / (b * c) = a / b

Tactic:
rw [div_mul_eq_div_div_swap]

Premises used: div_mul_eq_div_div_swap
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ a * c / c / b = a / b

Tactic:
simp only [mul_div_cancel_right]

Premises used: mul_div_cancel_right
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a * c = b
⊢ a = b / c

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = c * b
⊢ a / b = c

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a / c = b
⊢ a = b * c

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = c / b
⊢ a * b = c

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ a / b = a / c ↔ b = c

Tactic:
div_right_injective.eq_iff

Premises used: Function.Injective.eq_iff, div_right_injective
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : b * a⁻¹ = c * a⁻¹ ↔ b = c
⊢ b / a = c / a ↔ b = c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ b * a⁻¹ = c * a⁻¹ ↔ b = c

Tactic:
mul_left_inj _

Premises used: mul_left_inj
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ b * a⁻¹ = c * a⁻¹ ↔ b = c

Tactic:
exact mul_left_inj _

Premises used: mul_left_inj
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : a / b * b / c = a / c
rw₁ rw₂ : a / c = a / c
⊢ a / b * (b / c) = a / c

Tactic:
rw [← mul_div_assoc, div_mul_cancel]

Premises used: mul_div_assoc, div_mul_cancel
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : a * (b * (b⁻¹ * c)) = a * c
rw₁ : a * (b * b⁻¹ * c) = a * c
rw₂ : a * (1 * c) = a * c
rw₃ rw₄ : a * c = a * c
⊢ a * b * (b⁻¹ * c) = a * c

Tactic:
rw [mul_assoc, ← mul_assoc b, mul_inv_cancel, one_mul]

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

Tactic:
rw [mul_assoc, ← mul_assoc b⁻¹, inv_mul_cancel, one_mul]

Premises used: inv_mul_cancel, mul_assoc, Inv.inv, one_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : a / c / (c / b)⁻¹ = a / b
rw₁ : a / c * (c / b) = a / b
rw₂ rw₃ : a / b = a / b
⊢ a / c / (b / c) = a / b

Tactic:
rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel]

Premises used: inv_div, div_inv_eq_mul, div_mul_div_cancel
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
h : a = b
rw : b / b = 1
rw₁ rw₂ : Eq.{u_3 + 1} (α := G) 1 1
⊢ a / b = 1

Tactic:
rw [h, div_self']

Premises used: div_self'
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a / b ≠ 1 ↔ a ≠ b

Tactic:
not_congr div_eq_one

Premises used: div_eq_one, not_congr
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a * b⁻¹ = a ↔ b = 1
rw₁ : b⁻¹ = 1 ↔ b = 1
rw₂ rw₃ : b = 1 ↔ b = 1
⊢ a / b = a ↔ b = 1

Tactic:
rw [div_eq_mul_inv, mul_eq_left, inv_eq_one]

Premises used: inv_eq_one, div_eq_mul_inv, mul_eq_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : a = b * c⁻¹ ↔ a * c = b
rw₁ rw₂ : a * c = b ↔ a * c = b
⊢ a = b / c ↔ a * c = b

Tactic:
rw [div_eq_mul_inv, eq_mul_inv_iff_mul_eq]

Premises used: div_eq_mul_inv, eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : a * b⁻¹ = c ↔ a = c * b
rw₁ rw₂ : a = c * b ↔ a = c * b
⊢ a / b = c ↔ a = c * b

Tactic:
rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul]

Premises used: div_eq_mul_inv, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b c d : G
H : a / b = c / d
rw : a / b = 1 ↔ c = d
rw₁ : c / d = 1 ↔ c = d
rw₂ rw₃ : c = d ↔ c = d
⊢ a = b ↔ c = d

Tactic:
rw [← div_eq_one, H, div_eq_one]

Premises used: div_eq_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
c : G
⊢ LeftInverse (fun (x : G) ↦ x / c) fun (x : G) ↦ x * c

Tactic:
fun x ↦ mul_div_cancel_right x c

Premises used: Function.LeftInverse, mul_div_cancel_right
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
c : G
⊢ LeftInverse (fun (x : G) ↦ x * c) fun (x : G) ↦ x / c

Tactic:
fun x ↦ div_mul_cancel x c

Premises used: Function.LeftInverse, div_mul_cancel
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
c : G
⊢ LeftInverse (fun (x : G) ↦ c * x) fun (x : G) ↦ c⁻¹ * x

Tactic:
fun x ↦ mul_inv_cancel_left c x

Premises used: Function.LeftInverse, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
c : G
⊢ LeftInverse (fun (x : G) ↦ c⁻¹ * x) fun (x : G) ↦ c * x

Tactic:
fun x ↦ inv_mul_cancel_left c x

Premises used: Function.LeftInverse, inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
ofNat : ∀ (a_1 : ℕ), a ^ (Int.ofNat a_1).natAbs = 1 ↔ a ^ Int.ofNat a_1 = 1
negSucc : ∀ (a_1 : ℕ), a ^ (Int.negSucc a_1).natAbs = 1 ↔ a ^ Int.negSucc a_1 = 1
⊢ a ^ n.natAbs = 1 ↔ a ^ n = 1

Tactic:
cases n
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
a_1 : ℕ
⊢ a ^ (Int.ofNat a_1).natAbs = 1 ↔ a ^ Int.ofNat a_1 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
a_1 : ℕ
⊢ a ^ (Int.negSucc a_1).natAbs = 1 ↔ a ^ Int.negSucc a_1 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℕ
h : n ≤ m
rw : a ^ (m - n + n) = a ^ m
rw₁ rw₂ : a ^ m = a ^ m
⊢ a ^ (m - n) * a ^ n = a ^ m

Tactic:
rw [← pow_add, Nat.sub_add_cancel h]

Premises used: pow_add, Nat.sub_add_cancel
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℕ
h : n ≤ m
rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
rw₁ : (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
rw₂ : (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n
rw₃ rw₄ : (a ^ m)⁻¹ * a ^ n = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]

Premises used: pow_sub, inv_pow, Inv.inv, inv_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℕ
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a

Tactic:
simp only [← Int.natCast_succ, zpow_natCast, pow_succ]

Premises used: zpow_natCast, pow_succ, Int.natCast_succ
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
⊢ a ^ HAdd.hAdd (α := ℤ) (-1) 1 = HPow.hPow (β := ℤ) a (-1) * a

Tactic:
simp [Int.add_left_neg]

Premises used: Int.add_left_neg
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℕ
rw : a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a

Tactic:
rw [zpow_negSucc, pow_succ', mul_inv_rev, inv_mul_cancel_right]

Premises used: zpow_negSucc, mul_inv_rev, inv_mul_cancel_right, pow_succ'