awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ↔ b = 1
have rw₁ : b⁻¹ = 1 ↔ b = 1
Tactic: rw [div_eq_mul_inv, mul_eq_left, inv_eq_one]
-- 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
rw₁ : b⁻¹ = 1 ↔ b = 1
⊢ a / b = a ↔ b = 1
have rw₂ : b = 1 ↔ b = 1
Tactic: rw [div_eq_mul_inv, mul_eq_left, inv_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ a = b / c ↔ a * c = b
have rw : a = b * c⁻¹ ↔ a * c = b
Tactic: rw [div_eq_mul_inv, eq_mul_inv_iff_mul_eq]
-- 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 * c⁻¹ ↔ a * c = b
⊢ a = b / c ↔ a * c = b
have rw₁ : a * c = b ↔ a * c = b
Tactic: rw [div_eq_mul_inv, eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c : G
⊢ a / b = c ↔ a = c * b
have rw : a * b⁻¹ = c ↔ a = c * b
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_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⁻¹ = c ↔ a = c * b
⊢ a / b = c ↔ a = c * b
have rw₁ : a = c * b ↔ a = c * b
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c d : G
H : a / b = c / d
⊢ a = b ↔ c = d
have rw : a / b = 1 ↔ c = d
Tactic: rw [← div_eq_one, H, div_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a b c d : G
H : a / b = c / d
rw : a / b = 1 ↔ c = d
⊢ a = b ↔ c = d
have rw₁ : c / d = 1 ↔ c = d
Tactic: rw [← div_eq_one, H, div_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a = b ↔ c = d
have rw₂ : c = d ↔ c = d
Tactic: rw [← div_eq_one, H, div_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
⊢ a ^ n.natAbs = 1 ↔ a ^ n = 1
have ofNat : ∀ (a_1 : ℕ), a ^ (Int.ofNat a_1).natAbs = 1 ↔ a ^ Int.ofNat a_1 = 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a ^ n.natAbs = 1 ↔ a ^ n = 1
have negSucc : ∀ (a_1 : ℕ), a ^ (Int.negSucc a_1).natAbs = 1 ↔ a ^ Int.negSucc a_1 = 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a ^ (m - n) * a ^ n = a ^ m
have rw : a ^ (m - n + n) = a ^ m
Tactic: rw [← pow_add, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℕ
h : n ≤ m
rw : a ^ (m - n + n) = a ^ m
⊢ a ^ (m - n) * a ^ n = a ^ m
have rw₁ : a ^ m = a ^ m
Tactic: rw [← pow_add, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℕ
h : n ≤ m
rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw₁ : (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw₂ : (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw₃ : (a ^ m)⁻¹ * a ^ n = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw : a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, pow_succ', mul_inv_rev, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹
have rw : HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ)) = (a ^ (n + 1))⁻¹
Tactic: rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
have rw : a ^ (n - 1 + 1) * a⁻¹ = a ^ n * a⁻¹
Tactic: rw [← zpow_add_one, Int.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
rw : a ^ (n - 1 + 1) * a⁻¹ = a ^ n * a⁻¹
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
have rw₁ : a ^ n * a⁻¹ = a ^ n * a⁻¹
Tactic: rw [← zpow_add_one, Int.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -(↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ))
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * (HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹)
Tactic: rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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⁻¹)
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₁ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹
Tactic: rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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⁻¹
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₂ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + -(↑n : ℤ)) * a⁻¹
Tactic: rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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⁻¹
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₃ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + -(↑n : ℤ) - 1)
Tactic: rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₄ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n
have zero : a ^ (m + 0) = a ^ m * HPow.hPow (β := ℤ) a 0
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℤ
zero : a ^ (m + 0) = a ^ m * HPow.hPow (β := ℤ) a 0
⊢ a ^ (m + n) = a ^ m * a ^ n
have 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
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a ^ (m + n) = a ^ m * a ^ n
have 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
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
⊢ a ^ (1 + n) = a * a ^ n
have rw : HPow.hPow (β := ℤ) a 1 * a ^ n = a * a ^ n
Tactic: rw [zpow_add, zpow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
rw : HPow.hPow (β := ℤ) a 1 * a ^ n = a * a ^ n
⊢ a ^ (1 + n) = a * a ^ n
have rw₁ : a * a ^ n = a * a ^ n
Tactic: rw [zpow_add, zpow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
⊢ a * a ^ n = a ^ (n + 1)
have rw : a * a ^ n = a ^ (1 + n)
Tactic: rw [Int.add_comm, zpow_add, zpow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
n : ℤ
rw : a * a ^ n = a ^ (1 + n)
⊢ a * a ^ n = a ^ (n + 1)
have rw₁ : a * a ^ n = HPow.hPow (β := ℤ) a 1 * a ^ n
Tactic: rw [Int.add_comm, zpow_add, zpow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a * a ^ n = a ^ (n + 1)
have rw₂ : a * a ^ n = a * a ^ n
Tactic: rw [Int.add_comm, zpow_add, zpow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℤ
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
have rw : a ^ (m + -n) = a ^ m * (a ^ n)⁻¹
Tactic: rw [Int.sub_eq_add_neg, zpow_add, zpow_neg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℤ
rw : a ^ (m + -n) = a ^ m * (a ^ n)⁻¹
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
have rw₁ : a ^ m * a ^ (-n) = a ^ m * (a ^ n)⁻¹
Tactic: rw [Int.sub_eq_add_neg, zpow_add, zpow_neg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)⁻¹
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
have rw₂ : a ^ m * (a ^ n)⁻¹ = a ^ m * (a ^ n)⁻¹
Tactic: rw [Int.sub_eq_add_neg, zpow_add, zpow_neg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℤ
⊢ a ^ m * a ^ n = a ^ n * a ^ m
have rw : a ^ (m + n) = a ^ n * a ^ m
Tactic: rw [← zpow_add, Int.add_comm, zpow_add]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
a : G
m n : ℤ
rw : a ^ (m + n) = a ^ n * a ^ m
⊢ a ^ m * a ^ n = a ^ n * a ^ m
have rw₁ : a ^ (n + m) = a ^ n * a ^ m
Tactic: rw [← zpow_add, Int.add_comm, zpow_add]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a ^ m * a ^ n = a ^ n * a ^ m
have rw₂ : a ^ n * a ^ m = a ^ n * a ^ m
Tactic: rw [← zpow_add, Int.add_comm, zpow_add]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
x : G
m n : ℤ
h : x ^ n = 1
⊢ x ^ m = x ^ (m % n + n * (m / n))
have rw : x ^ m = x ^ m
Tactic: rw [Int.emod_add_mul_ediv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
k : ℤ
⊢ Eq.{u_3 + 1} (α := G → G) (fun (x : G) ↦ x ^ k)^[0] fun (x : G) ↦ x ^ HPow.hPow (β := ℕ) k 0
have h : ∀ (x : G), (fun (x : G) ↦ x ^ k)^[0] x = x ^ HPow.hPow (β := ℕ) k 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : Group G
k : ℤ
n : ℕ
⊢ Eq.{u_3 + 1} (α := G → G) (fun (x : G) ↦ x ^ k)^[n + 1] fun (x : G) ↦ x ^ k ^ (n + 1)
have h : ∀ (x : G), (fun (x : G) ↦ x ^ k)^[n + 1] x = x ^ k ^ (n + 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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 ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have succ : P (g * HPow.hPow (β := ℤ) g (↑n : ℤ))
Tactic: rw [Int.add_comm, zpow_add, zpow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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 ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have pred : P (g⁻¹ * HPow.hPow (β := ℤ) g (-(↑n : ℤ)))
Tactic: rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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 : ℤ
⊢ P (g ^ n)
have zero : P (HPow.hPow (β := ℤ) g 0)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ P (g ^ n)
have succ : ∀ (n : ℕ) (ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))), P (g ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ P (g ^ n)
have pred : ∀ (n : ℕ) (ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))), P (g ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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 (g ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have succ : P (HPow.hPow (β := ℤ) g (↑n : ℤ) * g)
Tactic: rw [zpow_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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 (g ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have pred : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)) * g⁻¹)
Tactic: rw [zpow_sub_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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 : ℤ
⊢ P (g ^ n)
have zero : P (HPow.hPow (β := ℤ) g 0)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ P (g ^ n)
have succ : ∀ (n : ℕ) (ih : P (HPow.hPow (β := ℤ) g (↑n : ℤ))), P (g ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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)
⊢ P (g ^ n)
have pred : ∀ (n : ℕ) (ih : P (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))), P (g ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
h : a = b * c
⊢ a / b = c
have rw : b * c / b = c
Tactic: rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
h : a = b * c
rw : b * c / b = c
⊢ a / b = c
have rw₁ : b * c * b⁻¹ = c
Tactic: rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a / b = c
have rw₂ : b⁻¹ * (b * c) = c
Tactic: rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a / b = c
have rw₃ : c = c
Tactic: rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
h : b = c / a
⊢ a * b = c
have rw : a * (c / a) = c
Tactic: rw [h, div_eq_mul_inv, mul_comm c, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
h : b = c / a
rw : a * (c / a) = c
⊢ a * b = c
have rw₁ : a * (c * a⁻¹) = c
Tactic: rw [h, div_eq_mul_inv, mul_comm c, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a * b = c
have rw₂ : a * (a⁻¹ * c) = c
Tactic: rw [h, div_eq_mul_inv, mul_comm c, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
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
⊢ a * b = c
have rw₃ : c = c
Tactic: rw [h, div_eq_mul_inv, mul_comm c, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
⊢ a = b / c ↔ c * a = b
have rw : a * c = b ↔ c * a = b
Tactic: rw [eq_div_iff_mul_eq', mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
rw : a * c = b ↔ c * a = b
⊢ a = b / c ↔ c * a = b
have rw₁ : c * a = b ↔ c * a = b
Tactic: rw [eq_div_iff_mul_eq', mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
⊢ a / b = c ↔ a = b * c
have rw : a = c * b ↔ a = b * c
Tactic: rw [div_eq_iff_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
rw : a = c * b ↔ a = b * c
⊢ a / b = c ↔ a = b * c
have rw₁ : a = b * c ↔ a = b * c
Tactic: rw [div_eq_iff_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
⊢ a / b = c ↔ a / c = b
have rw : a = b * c ↔ a / c = b
Tactic: rw [div_eq_iff_eq_mul', div_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b c : G
rw : a = b * c ↔ a / c = b
⊢ a / b = c ↔ a / c = b
have rw₁ : a = b * c ↔ a = b * c
Tactic: rw [div_eq_iff_eq_mul', div_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b : G
⊢ a * b / a = b
have rw : a⁻¹ * (a * b) = b
Tactic: rw [div_eq_inv_mul, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b : G
rw : a⁻¹ * (a * b) = b
⊢ a * b / a = b
have rw₁ : b = b
Tactic: rw [div_eq_inv_mul, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b : G
⊢ a * (b / a) = b
have rw : a * b / a = b
Tactic: rw [← mul_div_assoc, mul_div_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b : G
rw : a * b / a = b
⊢ a * (b / a) = b
have rw₁ : b = b
Tactic: rw [← mul_div_assoc, mul_div_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b : G
⊢ a / (a * b) = b⁻¹
have rw : (a * b / a)⁻¹ = b⁻¹
Tactic: rw [← inv_div, mul_div_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b : G
rw : (a * b / a)⁻¹ = b⁻¹
⊢ a / (a * b) = b⁻¹
have rw₁ : b⁻¹ = b⁻¹
Tactic: rw [← inv_div, mul_div_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b : G
⊢ a * (b * a⁻¹) = b
have rw : a * (b / a) = b
Tactic: rw [← div_eq_mul_inv, mul_div_cancel a b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
a b : G
rw : a * (b / a) = b
⊢ a * (b * a⁻¹) = b
have rw₁ : b = b
Tactic: rw [← div_eq_mul_inv, mul_div_cancel a b]