awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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))⁻¹
⊢ a ^ ((↑m : ℤ) * Int.negSucc n) = HPow.hPow (β := ℤ) a (↑m : ℤ) ^ Int.negSucc n
have rw₂ : a ^ ((↑m : ℤ) * Int.negSucc n) = (a ^ (m * (n + 1)))⁻¹
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)))⁻¹
⊢ a ^ ((↑m : ℤ) * Int.negSucc n) = HPow.hPow (β := ℤ) a (↑m : ℤ) ^ Int.negSucc n
have rw₃ : HPow.hPow (β := ℤ) a (-(↑(m * n.succ) : ℤ)) = (a ^ (m * (n + 1)))⁻¹
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)))⁻¹
⊢ a ^ ((↑m : ℤ) * Int.negSucc n) = HPow.hPow (β := ℤ) a (↑m : ℤ) ^ Int.negSucc n
have rw₄ : (HPow.hPow (β := ℤ) a (↑(m * n.succ) : ℤ))⁻¹ = (a ^ (m * (n + 1)))⁻¹
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)))⁻¹
⊢ a ^ ((↑m : ℤ) * Int.negSucc n) = HPow.hPow (β := ℤ) a (↑m : ℤ) ^ Int.negSucc n
have rw₅ : HPow.hPow (β := ℤ) a (↑(m * n.succ) : ℤ) = a ^ (m * (n + 1))
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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))
⊢ a ^ ((↑m : ℤ) * Int.negSucc n) = HPow.hPow (β := ℤ) a (↑m : ℤ) ^ Int.negSucc n
have rw₆ : HPow.hPow (β := ℤ) a (↑(m * n.succ) : ℤ) = HPow.hPow (β := ℤ) a (↑(m * (n + 1)) : ℤ)
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)
have rw : a ^ (Int.negSucc m * (↑n : ℤ)) = (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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
rw : a ^ (Int.negSucc m * (↑n : ℤ)) = (a ^ Int.negSucc m) ^ n
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)
have rw₁ : a ^ (Int.negSucc m * (↑n : ℤ)) = (a ^ (m + 1))⁻¹ ^ n
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)
have rw₂ : a ^ (Int.negSucc m * (↑n : ℤ)) = (a⁻¹ ^ (m + 1)) ^ n
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)
have rw₃ : a ^ (Int.negSucc m * (↑n : ℤ)) = a⁻¹ ^ ((m + 1) * n)
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)
have rw₄ : HPow.hPow (β := ℤ) a (-(↑(m.succ * n) : ℤ)) = a⁻¹ ^ ((m + 1) * n)
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)
have rw₅ : (HPow.hPow (β := ℤ) a (↑(m.succ * n) : ℤ))⁻¹ = a⁻¹ ^ ((m + 1) * n)
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)
have rw₆ : (HPow.hPow (β := ℤ) a (↑(m.succ * n) : ℤ))⁻¹ = (a ^ ((m + 1) * n))⁻¹
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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))⁻¹
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)
have rw₇ : HPow.hPow (β := ℤ) a (↑(m.succ * n) : ℤ) = a ^ ((m + 1) * n)
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ a ^ (Int.negSucc m * (↑n : ℤ)) = HPow.hPow (β := ℤ) (a ^ Int.negSucc m) (↑n : ℤ)
have rw₈ : HPow.hPow (β := ℤ) a (↑(m.succ * n) : ℤ) = HPow.hPow (β := ℤ) a (↑((m + 1) * n) : ℤ)
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (Int.negSucc m * Int.negSucc n) = (a ^ Int.negSucc m) ^ Int.negSucc n
have rw : a ^ HMul.hMul (α := ℤ) (↑m.succ : ℤ) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) a (↑((m + 1) * (n + 1)) : ℤ)
Tactic: rw [zpow_negSucc, zpow_negSucc, Int.negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ←
      zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℤ
⊢ a ^ (m * n) = (a ^ n) ^ m
have rw : a ^ (n * m) = (a ^ n) ^ m
Tactic: rw [Int.mul_comm, zpow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℤ
rw : a ^ (n * m) = (a ^ n) ^ m
⊢ a ^ (m * n) = (a ^ n) ^ m
have rw₁ : (a ^ n) ^ m = (a ^ n) ^ m
Tactic: rw [Int.mul_comm, zpow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℤ
⊢ (a ^ m) ^ n = (a ^ n) ^ m
have rw : a ^ (m * n) = (a ^ n) ^ m
Tactic: rw [← zpow_mul, zpow_mul']
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℤ
rw : a ^ (m * n) = (a ^ n) ^ m
⊢ (a ^ m) ^ n = (a ^ n) ^ m
have rw₁ : (a ^ n) ^ m = (a ^ n) ^ m
Tactic: rw [← zpow_mul, zpow_mul']
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
n : ℕ
⊢ HPow.hPow (β := ℤ) (a * b) (↑n : ℤ) = HPow.hPow (β := ℤ) a (↑n : ℤ) * HPow.hPow (β := ℤ) b (↑n : ℤ)
have simp_rw : (a * b) ^ n = a ^ n * b ^ n
Tactic: simp_rw [zpow_natCast, mul_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n
have simp_rw : ((a * b) ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * (b ^ (n + 1))⁻¹
Tactic: simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionCommMonoid α
a b : α
n : ℕ
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
have simp_rw₁ : (a * b)⁻¹ ^ (n + 1) = a⁻¹ ^ (n + 1) * b⁻¹ ^ (n + 1)
Tactic: simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n
have simp_rw₂ : (a⁻¹ * b⁻¹) ^ (n + 1) = a⁻¹ ^ (n + 1) * b⁻¹ ^ (n + 1)
Tactic: simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a / b = b⁻¹ ↔ a = 1
have rw : a * b⁻¹ = b⁻¹ ↔ a = 1
Tactic: rw [div_eq_mul_inv, mul_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a * b⁻¹ = b⁻¹ ↔ a = 1
⊢ a / b = b⁻¹ ↔ a = 1
have rw₁ : a = 1 ↔ a = 1
Tactic: rw [div_eq_mul_inv, mul_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b = a⁻¹ * c
⊢ a * b = c
have rw : a * (a⁻¹ * c) = c
Tactic: rw [h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b = a⁻¹ * c
rw : a * (a⁻¹ * c) = c
⊢ a * b = c
have rw₁ : c = c
Tactic: rw [h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
h : a = b⁻¹
⊢ a * b = 1
have rw : b⁻¹ * b = 1
Tactic: rw [h, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
h : a = b⁻¹
rw : b⁻¹ * b = 1
⊢ a * b = 1
have rw₁ : Eq.{u_3 + 1} (α := G) 1 1
Tactic: rw [h, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a * b = 1 ↔ a⁻¹ = b
have rw : a = b⁻¹ ↔ a⁻¹ = b
Tactic: rw [mul_eq_one_iff_eq_inv, inv_eq_iff_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a = b⁻¹ ↔ a⁻¹ = b
⊢ a * b = 1 ↔ a⁻¹ = b
have rw₁ : a = b⁻¹ ↔ a = b⁻¹
Tactic: rw [mul_eq_one_iff_eq_inv, inv_eq_iff_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a * b = 1 ↔ b = a⁻¹
have rw : a⁻¹ = b ↔ b = a⁻¹
Tactic: rw [mul_eq_one_iff_inv_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a⁻¹ = b ↔ b = a⁻¹
⊢ a * b = 1 ↔ b = a⁻¹
have rw₁ : b = a⁻¹ ↔ b = a⁻¹
Tactic: rw [mul_eq_one_iff_inv_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a * b = 1 ↔ b⁻¹ = a
have rw : a = b⁻¹ ↔ b⁻¹ = a
Tactic: rw [mul_eq_one_iff_eq_inv, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a = b⁻¹ ↔ b⁻¹ = a
⊢ a * b = 1 ↔ b⁻¹ = a
have rw₁ : b⁻¹ = a ↔ b⁻¹ = a
Tactic: rw [mul_eq_one_iff_eq_inv, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = b * c⁻¹
⊢ a * c = b
have rw : b * c⁻¹ * c = b
Tactic: rw [h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = b * c⁻¹
rw : b * c⁻¹ * c = b
⊢ a * c = b
have rw₁ : b = b
Tactic: rw [h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a * c = b
⊢ a = b * c⁻¹
have rw : a = a * c * c⁻¹
Tactic: rw [← h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a * c = b
rw : a = a * c * c⁻¹
⊢ a = b * c⁻¹
have rw₁ : a = a
Tactic: rw [← h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = b⁻¹ * c
⊢ b * a = c
have rw : b * (b⁻¹ * c) = c
Tactic: rw [h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = b⁻¹ * c
rw : b * (b⁻¹ * c) = c
⊢ b * a = c
have rw₁ : c = c
Tactic: rw [h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b * a = c
⊢ a = b⁻¹ * c
have rw : a = b⁻¹ * (b * a)
Tactic: rw [← h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b * a = c
rw : a = b⁻¹ * (b * a)
⊢ a = b⁻¹ * c
have rw₁ : a = a
Tactic: rw [← h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a⁻¹ * b = c
⊢ b = a * c
have rw : b = a * (a⁻¹ * b)
Tactic: rw [← h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a⁻¹ * b = c
rw : b = a * (a⁻¹ * b)
⊢ b = a * c
have rw₁ : b = b
Tactic: rw [← h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b = a * c
⊢ a⁻¹ * b = c
have rw : a⁻¹ * (a * c) = c
Tactic: rw [h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : b = a * c
rw : a⁻¹ * (a * c) = c
⊢ a⁻¹ * b = c
have rw₁ : c = c
Tactic: rw [h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a * b⁻¹ = c
⊢ a = c * b
have rw : a = a * b⁻¹ * b
Tactic: rw [← h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a * b⁻¹ = c
rw : a = a * b⁻¹ * b
⊢ a = c * b
have rw₁ : a = a
Tactic: rw [← h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = c * b
⊢ a * b⁻¹ = c
have rw : c * b * b⁻¹ = c
Tactic: rw [h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
h : a = c * b
rw : c * b * b⁻¹ = c
⊢ a * b⁻¹ = c
have rw₁ : c = c
Tactic: rw [h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a * b⁻¹ = 1 ↔ a = b
have rw : a = b⁻¹⁻¹ ↔ a = b
Tactic: rw [mul_eq_one_iff_eq_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a = b⁻¹⁻¹ ↔ a = b
⊢ a * b⁻¹ = 1 ↔ a = b
have rw₁ : a = b ↔ a = b
Tactic: rw [mul_eq_one_iff_eq_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a⁻¹ * b = 1 ↔ a = b
have rw : a⁻¹ = b⁻¹ ↔ a = b
Tactic: rw [mul_eq_one_iff_eq_inv, inv_inj]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a⁻¹ = b⁻¹ ↔ a = b
⊢ a⁻¹ * b = 1 ↔ a = b
have rw₁ : a = b ↔ a = b
Tactic: rw [mul_eq_one_iff_eq_inv, inv_inj]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a * b * a⁻¹ = 1 ↔ b = 1
have rw : a * b = a ↔ b = 1
Tactic: rw [mul_inv_eq_one, mul_eq_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
rw : a * b = a ↔ b = 1
⊢ a * b * a⁻¹ = 1 ↔ b = 1
have rw₁ : b = 1 ↔ b = 1
Tactic: rw [mul_inv_eq_one, mul_eq_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
b : G
⊢ Injective (β := G) fun (a : G) ↦ a / b
have simp : Injective (β := G) fun (a : G) ↦ a * b⁻¹
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
b : G
⊢ Injective (β := G) fun (a : G) ↦ b / a
have simp : Injective (β := G) fun (a : G) ↦ b * a⁻¹
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a / (b * a) = b⁻¹
have rw : (b * a / a)⁻¹ = b⁻¹
Tactic: rw [← inv_div, mul_div_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
rw : (b * a / a)⁻¹ = b⁻¹
⊢ a / (b * a) = b⁻¹
have rw₁ : b⁻¹ = b⁻¹
Tactic: rw [← inv_div, mul_div_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ a * c / (b * c) = a / b
have rw : a * c / c / b = a / b
Tactic: rw [div_mul_eq_div_div_swap]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ b / a = c / a ↔ b = c
have rw : b * a⁻¹ = c * a⁻¹ ↔ b = c
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ a / b * (b / c) = a / c
have rw : a / b * b / c = a / c
Tactic: rw [← mul_div_assoc, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : a / b * b / c = a / c
⊢ a / b * (b / c) = a / c
have rw₁ : a / c = a / c
Tactic: rw [← mul_div_assoc, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ a * b * (b⁻¹ * c) = a * c
have rw : a * (b * (b⁻¹ * c)) = a * c
Tactic: rw [mul_assoc, ← mul_assoc b, mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : a * (b * (b⁻¹ * c)) = a * c
⊢ a * b * (b⁻¹ * c) = a * c
have rw₁ : a * (b * b⁻¹ * c) = a * c
Tactic: rw [mul_assoc, ← mul_assoc b, mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a * b * (b⁻¹ * c) = a * c
have rw₂ : a * (1 * c) = a * c
Tactic: rw [mul_assoc, ← mul_assoc b, mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a * b * (b⁻¹ * c) = a * c
have rw₃ : a * c = a * c
Tactic: rw [mul_assoc, ← mul_assoc b, mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ a * b⁻¹ * (b * c) = a * c
have rw : a * (b⁻¹ * (b * c)) = a * c
Tactic: rw [mul_assoc, ← mul_assoc b⁻¹, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
rw : a * (b⁻¹ * (b * c)) = a * c
⊢ a * b⁻¹ * (b * c) = a * c
have rw₁ : a * (b⁻¹ * b * c) = a * c
Tactic: rw [mul_assoc, ← mul_assoc b⁻¹, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a * b⁻¹ * (b * c) = a * c
have rw₂ : a * (1 * c) = a * c
Tactic: rw [mul_assoc, ← mul_assoc b⁻¹, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a * b⁻¹ * (b * c) = a * c
have rw₃ : a * c = a * c
Tactic: rw [mul_assoc, ← mul_assoc b⁻¹, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ a / c / (b / c) = a / b
have rw : a / c / (c / b)⁻¹ = a / b
Tactic: rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
have rw₁ : a / c * (c / b) = a / b
Tactic: rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a / c / (b / c) = a / b
have rw₂ : a / b = a / b
Tactic: rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
h : a = b
⊢ a / b = 1
have rw : b / b = 1
Tactic: rw [h, div_self']
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
h : a = b
rw : b / b = 1
⊢ a / b = 1
have rw₁ : Eq.{u_3 + 1} (α := G) 1 1
Tactic: rw [h, div_self']
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b : G
⊢ a / b = a ↔ b = 1
have rw : a * b⁻¹ = a ↔ b = 1
Tactic: rw [div_eq_mul_inv, mul_eq_left, inv_eq_one]