awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℕ
rw : HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ)) = (a ^ (n + 1))⁻¹
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹

Tactic:
rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right]

Premises used: Int.neg_add_cancel_right, Int.neg_add, Int.negSucc_eq
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℕ
⊢ HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ)) = (a ^ (n + 1))⁻¹

Tactic:
zpow_negSucc _ _

Premises used: zpow_negSucc, Int.neg, Int.negOfNat
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℕ
⊢ HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ)) = (a ^ (n + 1))⁻¹

Tactic:
exact zpow_negSucc _ _

Premises used: zpow_negSucc
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
rw : a ^ (n - 1 + 1) * a⁻¹ = a ^ n * a⁻¹
rw₁ rw₂ : a ^ n * a⁻¹ = a ^ n * a⁻¹
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹

Tactic:
rw [← zpow_add_one, Int.sub_add_cancel]

Premises used: zpow_add_one, Int.sub_add_cancel
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
m : ℤ
⊢ a ^ (m + 0) = a ^ m * HPow.hPow (β := ℤ) a 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + (↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (↑n : ℤ)
⊢ a ^ (m + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = a ^ m * a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1

Tactic:
simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]

Premises used: mul_assoc, Int.add_assoc, zpow_add_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -(↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ))
pred : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * (HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹)
pred₁ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹
pred₂ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + -(↑n : ℤ)) * a⁻¹
pred₃ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + -(↑n : ℤ) - 1)
pred₄ pred₅ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1

Tactic:
rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]

Premises used: zpow_sub_one, mul_assoc, Int.add_sub_assoc
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℤ
zero : a ^ (m + 0) = a ^ m * HPow.hPow (β := ℤ) a 0
succ :
  ∀ (n : ℕ) (ihn : a ^ (m + (↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (↑n : ℤ)),
    a ^ (m + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = a ^ m * a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
pred :
  ∀ (n : ℕ) (ihn : a ^ (m + -(↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ))),
    a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
induction n with
  | zero => simp
  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]

Premises used: zpow_sub_one, mul_assoc, Int.add_assoc, zpow_add_one, Int.add_sub_assoc
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
rw : HPow.hPow (β := ℤ) a 1 * a ^ n = a * a ^ n
rw₁ rw₂ : a * a ^ n = a * a ^ n
⊢ a ^ (1 + n) = a * a ^ n

Tactic:
rw [zpow_add, zpow_one]

Premises used: zpow_add, zpow_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
rw : a * a ^ n = a ^ (1 + n)
rw₁ : a * a ^ n = HPow.hPow (β := ℤ) a 1 * a ^ n
rw₂ rw₃ : a * a ^ n = a * a ^ n
⊢ a * a ^ n = a ^ (n + 1)

Tactic:
rw [Int.add_comm, zpow_add, zpow_one]

Premises used: zpow_add, zpow_one, Int.add_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
⊢ a ^ n * a = a ^ (n + 1)

Tactic:
(zpow_add_one ..).symm

Premises used: zpow_add_one, Eq.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℤ
rw : a ^ (m + -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 [Int.sub_eq_add_neg, zpow_add, zpow_neg]

Premises used: zpow_add, Int.sub_eq_add_neg, zpow_neg
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℕ
⊢ a ^ HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ) = a ^ m / a ^ n

Tactic:
simpa [div_eq_mul_inv] using zpow_sub a m n

Premises used: div_eq_mul_inv, Nat.cast, zpow_sub
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℕ
⊢ a ^ HSub.hSub (α := ℤ) (↑n : ℤ) 1 = a ^ n / a

Tactic:
simpa [div_eq_mul_inv] using zpow_sub a n 1

Premises used: div_eq_mul_inv, Nat.cast, OfNat.ofNat, zpow_sub
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
n : ℕ
⊢ a ^ HSub.hSub (α := ℤ) 1 (↑n : ℤ) = a / a ^ n

Tactic:
simpa [div_eq_mul_inv] using zpow_sub a 1 n

Premises used: div_eq_mul_inv, Nat.cast, OfNat.ofNat, zpow_sub
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℤ
rw : a ^ (m + n) = a ^ n * a ^ m
rw₁ : a ^ (n + m) = a ^ n * a ^ m
rw₂ rw₃ : a ^ n * a ^ m = a ^ n * a ^ m
⊢ a ^ m * a ^ n = a ^ n * a ^ m

Tactic:
rw [← zpow_add, Int.add_comm, zpow_add]

Premises used: zpow_add, Int.add_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
n : ℕ
⊢ HPow.hPow (β := ℤ) (a * b) (↑n : ℤ) * a = a * HPow.hPow (β := ℤ) (b * a) (↑n : ℤ)

Tactic:
simp [mul_pow_mul]

Premises used: mul_pow_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
a b : G
n : ℕ
⊢ (a * b) ^ Int.negSucc n * a = a * (b * a) ^ Int.negSucc n

Tactic:
simp [inv_mul_eq_iff_eq_mul, eq_mul_inv_iff_mul_eq, mul_assoc, mul_pow_mul]

Premises used: mul_assoc, mul_pow_mul, eq_mul_inv_iff_mul_eq, inv_mul_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
x : G
m n : ℤ
h : x ^ n = 1
rw rw₁ : x ^ m = x ^ m
⊢ x ^ m = x ^ (m % n + n * (m / n))

Tactic:
rw [Int.emod_add_mul_ediv]

Premises used: Int.emod_add_mul_ediv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
x : G
m n : ℤ
h : x ^ n = 1
⊢ x ^ (m % n + n * (m / n)) = x ^ (m % n)

Tactic:
simp [zpow_add, zpow_mul, h]

Premises used: zpow_add, zpow_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
⊢ HPow.hPow (β := ℤ) x (↑n : ℤ) = 1

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
k : ℤ
h : ∀ (x : G), (fun (x : G) ↦ x ^ k)^[0] x = x ^ HPow.hPow (β := ℕ) k 0
⊢ Eq.{u_3 + 1} (α := G → G) (fun (x : G) ↦ x ^ k)^[0] fun (x : G) ↦ x ^ HPow.hPow (β := ℕ) k 0

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
k : ℤ
x : G
⊢ (fun (x : G) ↦ x ^ k)^[0] x = x ^ HPow.hPow (β := ℕ) k 0

Tactic:
simp [Int.pow_zero]

Premises used: Int.pow_zero
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
k : ℤ
n : ℕ
h : ∀ (x : G), (fun (x : G) ↦ x ^ k)^[n + 1] x = x ^ k ^ (n + 1)
⊢ Eq.{u_3 + 1} (α := G → G) (fun (x : G) ↦ x ^ k)^[n + 1] fun (x : G) ↦ x ^ k ^ (n + 1)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
k : ℤ
n : ℕ
x : G
⊢ (fun (x : G) ↦ x ^ k)^[n + 1] x = x ^ k ^ (n + 1)

Tactic:
simp [zpow_iterate, Int.pow_succ', zpow_mul]

Premises used: Int.pow_succ', zpow_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
zero zero₁ zero₂ zero₃ : P 1
⊢ P (HPow.hPow (β := ℤ) g 0)

Tactic:
rwa [zpow_zero]

Premises used: zpow_zero
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))
succ : P (g * HPow.hPow (β := ℤ) g (↑n : ℤ))
⊢ P (g ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
rw [Int.add_comm, zpow_add, zpow_one]

Premises used: zpow_add, zpow_one, Int.add_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))
⊢ P (g * HPow.hPow (β := ℤ) g (↑n : ℤ))

Tactic:
h_mul _ ih
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))
⊢ P (g * HPow.hPow (β := ℤ) g (↑n : ℤ))

Tactic:
exact h_mul _ ih
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))
pred : P (g⁻¹ * HPow.hPow (β := ℤ) g (-(↑n : ℤ)))
⊢ P (g ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]

Premises used: zpow_add, zpow_neg_one, Int.sub_eq_add_neg, Int.add_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))
⊢ P (g⁻¹ * HPow.hPow (β := ℤ) g (-(↑n : ℤ)))

Tactic:
h_inv _ ih
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))
⊢ P (g⁻¹ * HPow.hPow (β := ℤ) g (-(↑n : ℤ)))

Tactic:
exact h_inv _ ih
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℤ
zero : P (HPow.hPow (β := ℤ) g 0)
succ : ∀ (n : ℕ) (ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))), P (g ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
pred : ∀ (n : ℕ) (ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))), P (g ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ P (g ^ n)

Tactic:
induction n with
  | zero => rwa [zpow_zero]
  | succ n ih =>
    rw [Int.add_comm, zpow_add, zpow_one]
    exact h_mul _ ih
  | pred n ih =>
    rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
    exact h_inv _ ih

Premises used: zpow_add, zpow_neg_one, zpow_zero, zpow_one, Int.sub_eq_add_neg, Int.add_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
zero zero₁ zero₂ zero₃ : P 1
⊢ P (HPow.hPow (β := ℤ) g 0)

Tactic:
rwa [zpow_zero]

Premises used: zpow_zero
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))
succ : P (HPow.hPow (β := ℤ) g (↑n : ℤ) * g)
⊢ P (g ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
rw [zpow_add_one]

Premises used: zpow_add_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))
⊢ P (HPow.hPow (β := ℤ) g (↑n : ℤ) * g)

Tactic:
h_mul _ ih
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))
⊢ P (HPow.hPow (β := ℤ) g (↑n : ℤ) * g)

Tactic:
exact h_mul _ ih
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))
pred : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)) * g⁻¹)
⊢ P (g ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
rw [zpow_sub_one]

Premises used: zpow_sub_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))
⊢ P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)) * g⁻¹)

Tactic:
h_inv _ ih
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))
⊢ P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)) * g⁻¹)

Tactic:
exact h_inv _ ih
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℤ
zero : P (HPow.hPow (β := ℤ) g 0)
succ : ∀ (n : ℕ) (ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))), P (g ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
pred : ∀ (n : ℕ) (ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))), P (g ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ P (g ^ n)

Tactic:
induction n with
  | zero => rwa [zpow_zero]
  | succ n ih =>
    rw [zpow_add_one]
    exact h_mul _ ih
  | pred n ih =>
    rw [zpow_sub_one]
    exact h_inv _ ih

Premises used: zpow_sub_one, zpow_zero, zpow_add_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
h : a = b * c
rw : b * c / b = c
rw₁ : b * c * b⁻¹ = c
rw₂ : b⁻¹ * (b * c) = c
rw₃ rw₄ : c = c
⊢ a / b = c

Tactic:
rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, div_eq_mul_inv, mul_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
⊢ c * a / (c * b) = a / b

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

Tactic:
simp [h.symm]

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

Tactic:
simp [h.symm]

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

Tactic:
rw [h, div_eq_mul_inv, mul_comm c, mul_inv_cancel_left]

Premises used: div_eq_mul_inv, mul_comm, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b : G
⊢ a / (a / b) = b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
⊢ a / b = c / b * (a / c)

Tactic:
simp [mul_left_comm c]

Premises used: mul_left_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b : G
⊢ a / (a / b) = b

Tactic:
div_div_self' a b

Premises used: div_div_self'
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b : G
⊢ a / b / a = b⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
rw : a * c = b ↔ c * a = b
rw₁ rw₂ : c * a = b ↔ c * a = b
⊢ a = b / c ↔ c * a = b

Tactic:
rw [eq_div_iff_mul_eq', mul_comm]

Premises used: eq_div_iff_mul_eq', mul_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
rw : a = c * b ↔ a = b * c
rw₁ rw₂ : a = b * c ↔ a = b * c
⊢ a / b = c ↔ a = b * c

Tactic:
rw [div_eq_iff_eq_mul, mul_comm]

Premises used: div_eq_iff_eq_mul, mul_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
rw : a = b * c ↔ a / c = b
rw₁ rw₂ : a = b * c ↔ a = b * c
⊢ a / b = c ↔ a / c = b

Tactic:
rw [div_eq_iff_eq_mul', div_eq_iff_eq_mul]

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

Tactic:
rw [div_eq_inv_mul, inv_mul_cancel_left]

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

Tactic:
rw [← mul_div_assoc, mul_div_cancel_left]

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

Tactic:
rw [← inv_div, mul_div_cancel_left]

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

Tactic:
rw [← div_eq_mul_inv, mul_div_cancel a b]

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

Tactic:
rw [mul_assoc, mul_div_cancel]

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

Tactic:
rw [mul_left_comm, div_mul_cancel, mul_comm]

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

Tactic:
rw [mul_comm]

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

Tactic:
apply div_mul_div_cancel

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

Tactic:
rw [← div_mul, mul_div_cancel_left]

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

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

Premises used: mul_comm, inv_div, div_inv_eq_mul, div_mul_div_cancel
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b c d : G
rw : c * b = d * a ↔ a * d = c * b
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']

Premises used: div_eq_iff_eq_mul', div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b c d : G
⊢ c * b = d * a ↔ a * d = c * b

Tactic:
simp only [mul_comm, eq_comm]

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

Tactic:
rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_eq_div_iff_mul_eq_mul]

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

Tactic:
rw [← div_eq_inv_mul, ← div_eq_inv_mul, div_eq_div_iff_mul_eq_mul]

Premises used: div_eq_div_iff_mul_eq_mul, div_eq_inv_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a b c d : G
rw : a = c / d * b ↔ a / c = b / d
rw₁ : a = c * b / d ↔ a / c = b / d
rw₂ : a = c * b / d ↔ a = c * (b / d)
rw₃ rw₄ : a = c * (b / d) ↔ a = c * (b / d)
⊢ a / b = c / d ↔ a / c = b / d

Tactic:
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, div_eq_iff_eq_mul', mul_div_assoc]

Premises used: div_eq_iff_eq_mul', mul_div_assoc, div_mul_eq_mul_div, div_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommGroup G
a : G
⊢ Involutive fun (x : G) ↦ a / x

Tactic:
fun _ ↦ div_div_cancel ..

Premises used: Function.Involutive, div_div_cancel
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b_1 c_1 : α
pab_1 : p a b_1
pbc_1 : p b_1 c_1
pac_1 : p a c_1
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
inl : ∀ (rab : r a b), f a c = f a b * f b c
inr : ∀ (rba : r b a), f a c = f a b * f b c
⊢ f a c = f a b * f b c

Tactic:
obtain rab | rba := total_of r a b

Premises used: total_of
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b_1 c_1 : α
pab_1 : p a b_1
pbc_1 : p b_1 c_1
pac_1 : p a c_1
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rab : r a b
⊢ f a c = f a b * f b c

Tactic:
hmul rab rbc pab pbc pac
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b_1 c_1 : α
pab_1 : p a b_1
pbc_1 : p b_1 c_1
pac_1 : p a c_1
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rab : r a b
⊢ f a c = f a b * f b c

Tactic:
exact hmul rab rbc pab pbc pac
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b_1 c_1 : α
pab_1 : p a b_1
pbc_1 : p b_1 c_1
pac_1 : p a c_1
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
inr : f a b * (f b a * f a c) = f a b * f b c
⊢ f a c = f a b * f b c

Tactic:
rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]

Premises used: mul_assoc, one_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b_1 c_1 : α
pab_1 : p a b_1
pbc_1 : p b_1 c_1
pac_1 : p a c_1
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
inr : ∀ (rac : r a c), f a b * (f b a * f a c) = f a b * f b c
inr₁ : ∀ (rca : r c a), f a b * (f b a * f a c) = f a b * f b c
⊢ f a b * (f b a * f a c) = f a b * f b c

Tactic:
obtain rac | rca := total_of r a c

Premises used: total_of
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b_1 c_1 : α
pab_1 : p a b_1
pbc_1 : p b_1 c_1
pac_1 : p a c_1
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rac : r a c
inr inr₁ : f a b * (f b a * f a c) = f a b * (f b a * f a c)
⊢ f a b * (f b a * f a c) = f a b * f b c

Tactic:
rw [hmul rba rac (hsymm pab) pac pbc]