awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : α
b : p → β
c : ¬p → β
⊢ HPow.hPow.{u_1, u_2, u_1} (β := β) a (if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h
have pos : ∀ (h : p), a ^ b h = a ^ b h
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : α
b : p → β
c : ¬p → β
pos : ∀ (h : p), a ^ b h = a ^ b h
⊢ HPow.hPow.{u_1, u_2, u_1} (β := β) a (if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h
have neg : ∀ (h : ¬p), a ^ c h = a ^ c h
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
c : β
⊢ HPow.hPow (α := α) (if h : p then a h else b h) c = if h : p then a h ^ c else b h ^ c
have pos : ∀ (h : p), a h ^ c = a h ^ c
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
c : β
pos : ∀ (h : p), a h ^ c = a h ^ c
⊢ HPow.hPow (α := α) (if h : p then a h else b h) c = if h : p then a h ^ c else b h ^ c
have neg : ∀ (h : ¬p), b h ^ c = b h ^ c
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : Semigroup α
x y : α
⊢ Eq.{u_1 + 1} (α := α → α) ((fun (x_1 : α) ↦ x * x_1) ∘ fun (x : α) ↦ y * x) fun (x_1 : α) ↦ x * y * x_1
have h : ∀ (z : α), ((fun (x_1 : α) ↦ x * x_1) ∘ fun (x : α) ↦ y * x) z = x * y * z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : Semigroup α
x y : α
⊢ Eq.{u_1 + 1} (α := α → α) ((fun (x_1 : α) ↦ x_1 * x) ∘ fun (x : α) ↦ x * y) fun (x_1 : α) ↦ x_1 * (y * x)
have h : ∀ (z : α), ((fun (x_1 : α) ↦ x_1 * x) ∘ fun (x : α) ↦ x * y) z = z * (y * x)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : MulOneClass M
P : Prop
inst_1 : Decidable P
a b : M
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
have pos : ∀ (h : P), (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : MulOneClass M
P : Prop
inst_1 : Decidable P
a b : M
pos : ∀ (h : P), (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
have neg : ∀ (h : ¬P), (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : MulOneClass M
P : Prop
inst_1 : Decidable P
a b : M
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
have pos : ∀ (h : P), (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : MulOneClass M
P : Prop
inst_1 : Decidable P
a b : M
pos : ∀ (h : P), (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
have neg : ∀ (h : ¬P), (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 ↔ b = 1
have mp : a = 1 → b = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : MulOneClass M
a b : M
h : a * b = 1
mp : a = 1 → b = 1
⊢ a = 1 ↔ b = 1
have mpr : b = 1 → a = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommSemigroup G
a b c : G
⊢ a * (b * c) = b * (a * c)
have rw : a * b * c = b * (a * c)
Tactic: rw [← mul_assoc, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommSemigroup G
a b c : G
rw : a * b * c = b * (a * c)
⊢ a * (b * c) = b * (a * c)
have rw₁ : b * a * c = b * (a * c)
Tactic: rw [← mul_assoc, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommSemigroup G
a b c : G
rw : a * b * c = b * (a * c)
rw₁ : b * a * c = b * (a * c)
⊢ a * (b * c) = b * (a * c)
have rw₂ : b * (a * c) = b * (a * c)
Tactic: rw [← mul_assoc, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommSemigroup G
a b c : G
⊢ a * b * c = a * c * b
have rw : a * (b * c) = a * c * b
Tactic: rw [mul_assoc, mul_comm b, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommSemigroup 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 [mul_assoc, mul_comm b, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : CommSemigroup G
a b c : G
rw : a * (b * c) = a * c * b
rw₁ : a * (c * b) = a * c * b
⊢ a * b * c = a * c * b
have rw₂ : a * (c * b) = a * (c * b)
Tactic: rw [mul_assoc, mul_comm b, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ m * a ^ (n - m) = a ^ n
have rw : a ^ (m + (n - m)) = a ^ n
Tactic: rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
m n : ℕ
a : M
h : m ≤ n
rw : a ^ (m + (n - m)) = a ^ n
⊢ a ^ m * a ^ (n - m) = a ^ n
have rw₁ : a ^ (n - m + m) = a ^ n
Tactic: rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
m n : ℕ
a : M
h : m ≤ n
rw : a ^ (m + (n - m)) = a ^ n
rw₁ : a ^ (n - m + m) = a ^ n
⊢ a ^ m * a ^ (n - m) = a ^ n
have rw₂ : a ^ n = a ^ n
Tactic: rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ (n - m) * a ^ m = a ^ n
have rw : a ^ (n - m + m) = a ^ n
Tactic: rw [← pow_add, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
m n : ℕ
a : M
h : m ≤ n
rw : a ^ (n - m + m) = a ^ n
⊢ a ^ (n - m) * a ^ m = a ^ n
have rw₁ : a ^ n = a ^ n
Tactic: rw [← pow_add, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a * a ^ (n - 1) = a ^ n
have rw : a ^ (n - 1 + 1) = a ^ n
Tactic: rw [← pow_succ', Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
hn : n ≠ 0
a : M
rw : a ^ (n - 1 + 1) = a ^ n
⊢ a * a ^ (n - 1) = a ^ n
have rw₁ : a ^ n = a ^ n
Tactic: rw [← pow_succ', Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ (n - 1) * a = a ^ n
have rw : a ^ (n - 1 + 1) = a ^ n
Tactic: rw [← pow_succ, Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
hn : n ≠ 0
a : M
rw : a ^ (n - 1 + 1) = a ^ n
⊢ a ^ (n - 1) * a = a ^ n
have rw₁ : a ^ n = a ^ n
Tactic: rw [← pow_succ, Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ (m % n + n * (m / n))
have rw : a ^ m = a ^ m
Tactic: rw [Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ (m % n)
have a₁ : a ^ m = a ^ (m % n + n * (m / n))
Tactic: calc
    a ^ m = a ^ (m % n + n * (m / n)) := by rw [Nat.mod_add_div]
    _ = a ^ (m % n) := by simp [pow_add, pow_mul, ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
a₁ : a ^ m = a ^ (m % n + n * (m / n))
⊢ a ^ m = a ^ (m % n)
have a₂ : a ^ (m % n + n * (m / n)) = a ^ (m % n)
Tactic: calc
    a ^ m = a ^ (m % n + n * (m / n)) := by rw [Nat.mod_add_div]
    _ = a ^ (m % n) := by simp [pow_add, pow_mul, ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)
have rw : a ^ n * a * b ^ n.succ = a ^ n * a * (b * b ^ n)
Tactic: rw [pow_succ, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
a b : M
n : ℕ
h : a * b = 1
rw : a ^ n * a * b ^ n.succ = a ^ n * a * (b * b ^ n)
⊢ a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)
have rw₁ : a ^ n * a * (b * b ^ n) = a ^ n * a * (b * b ^ n)
Tactic: rw [pow_succ, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
a : M
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ a * x)^[0] fun (x : M) ↦ HPow.hPow (β := ℕ) a 0 * x
have h : ∀ (x : M), (fun (x : M) ↦ a * x)^[0] x = HPow.hPow (β := ℕ) a 0 * x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
a : M
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ x * a)^[0] fun (x : M) ↦ x * HPow.hPow (β := ℕ) a 0
have h : ∀ (x : M), (fun (x : M) ↦ x * a)^[0] x = x * HPow.hPow (β := ℕ) a 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
k : ℕ
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ x ^ k)^[0] fun (x : M) ↦ x ^ HPow.hPow (β := ℕ) k 0
have h : ∀ (x : M), (fun (x : M) ↦ x ^ k)^[0] x = x ^ HPow.hPow (β := ℕ) k 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
k n : ℕ
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ x ^ k)^[n + 1] fun (x : M) ↦ x ^ k ^ (n + 1)
have h : ∀ (x : M), (fun (x : M) ↦ x ^ k)^[n + 1] x = x ^ k ^ (n + 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a b : M
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
have rw : 1 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
Tactic: rw [pow_zero, pow_zero, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a b : M
rw : 1 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
have rw₁ : 1 = 1 * HPow.hPow (β := ℕ) b 0
Tactic: rw [pow_zero, pow_zero, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a b : M
rw : 1 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
rw₁ : 1 = 1 * HPow.hPow (β := ℕ) b 0
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
have rw₂ : 1 = HMul.hMul (α := M) 1 1
Tactic: rw [pow_zero, pow_zero, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a b : M
rw : 1 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
rw₁ : 1 = 1 * HPow.hPow (β := ℕ) b 0
rw₂ : 1 = HMul.hMul (α := M) 1 1
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
have rw₃ : Eq.{u_4 + 1} (α := M) 1 1
Tactic: rw [pow_zero, pow_zero, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a b : M
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)
have rw : a * b * (a * b) ^ n = a ^ (n + 1) * b ^ (n + 1)
Tactic: rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a b : M
n : ℕ
rw : a * b * (a * b) ^ n = a ^ (n + 1) * b ^ (n + 1)
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)
have rw₁ : a * b * (a * b) ^ n = a * a ^ n * b ^ (n + 1)
Tactic: rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a b : M
n : ℕ
rw : a * b * (a * b) ^ n = a ^ (n + 1) * b ^ (n + 1)
rw₁ : a * b * (a * b) ^ n = a * a ^ n * b ^ (n + 1)
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)
have rw₂ : a * b * (a * b) ^ n = a * a ^ n * (b * b ^ n)
Tactic: rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a b : M
n : ℕ
rw : a * b * (a * b) ^ n = a ^ (n + 1) * b ^ (n + 1)
rw₁ : a * b * (a * b) ^ n = a * a ^ n * b ^ (n + 1)
rw₂ : a * b * (a * b) ^ n = a * a ^ n * (b * b ^ n)
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)
have rw₃ : a * b * (a ^ n * b ^ n) = a * a ^ n * (b * b ^ n)
Tactic: rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a b : M
n : ℕ
rw : a * b * (a * b) ^ n = a ^ (n + 1) * b ^ (n + 1)
rw₁ : a * b * (a * b) ^ n = a * a ^ n * b ^ (n + 1)
rw₂ : a * b * (a * b) ^ n = a * a ^ n * (b * b ^ n)
rw₃ : a * b * (a ^ n * b ^ n) = a * a ^ n * (b * b ^ n)
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)
have rw₄ : a * a ^ n * (b * b ^ n) = a * a ^ n * (b * b ^ n)
Tactic: rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsLeftCancelMul M
a b : M
⊢ a * b = a ↔ a * b = a * 1
have rw : a * b = a ↔ a * b = a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsRightCancelMul M
a b : M
⊢ a * b = b ↔ a * b = 1 * b
have rw : a * b = b ↔ a * b = b
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : DivInvMonoid G
x y : G
⊢ x * (1 / y) = x / y
have rw : x * (1 * y⁻¹) = x / y
Tactic: rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : DivInvMonoid G
x y : G
rw : x * (1 * y⁻¹) = x / y
⊢ x * (1 / y) = x / y
have rw₁ : x * y⁻¹ = x / y
Tactic: rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : DivInvMonoid G
x y : G
rw : x * (1 * y⁻¹) = x / y
rw₁ : x * y⁻¹ = x / y
⊢ x * (1 / y) = x / y
have rw₂ : x * y⁻¹ = x * y⁻¹
Tactic: rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : DivInvMonoid G
a b : G
⊢ a / b = a * (1 / b)
have rw : a * b⁻¹ = a * (1 / b)
Tactic: rw [div_eq_mul_inv, one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
G : Type u_3
inst : DivInvMonoid G
a b : G
rw : a * b⁻¹ = a * (1 / b)
⊢ a / b = a * (1 / b)
have rw₁ : a * b⁻¹ = a * b⁻¹
Tactic: rw [div_eq_mul_inv, one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : b * a = 1
⊢ b = 1 / a
have rw : a⁻¹ = 1 / a
Tactic: rw [eq_inv_of_mul_eq_one_left h, one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : b * a = 1
rw : a⁻¹ = 1 / a
⊢ b = 1 / a
have rw₁ : a⁻¹ = a⁻¹
Tactic: rw [eq_inv_of_mul_eq_one_left h, one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : a * b = 1
⊢ b = 1 / a
have rw : a⁻¹ = 1 / a
Tactic: rw [eq_inv_of_mul_eq_one_right h, one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : a * b = 1
rw : a⁻¹ = 1 / a
⊢ b = 1 / a
have rw₁ : a⁻¹ = a⁻¹
Tactic: rw [eq_inv_of_mul_eq_one_right h, one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
⊢ HPow.hPow (β := ℕ) a⁻¹ 0 = (HPow.hPow (β := ℕ) a 0)⁻¹
have rw : 1 = (HPow.hPow (β := ℕ) a 0)⁻¹
Tactic: rw [pow_zero, pow_zero, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
rw : 1 = (HPow.hPow (β := ℕ) a 0)⁻¹
⊢ HPow.hPow (β := ℕ) a⁻¹ 0 = (HPow.hPow (β := ℕ) a 0)⁻¹
have rw₁ : Eq.{u_1 + 1} (α := α) 1 1⁻¹
Tactic: rw [pow_zero, pow_zero, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
rw : 1 = (HPow.hPow (β := ℕ) a 0)⁻¹
rw₁ : Eq.{u_1 + 1} (α := α) 1 1⁻¹
⊢ HPow.hPow (β := ℕ) a⁻¹ 0 = (HPow.hPow (β := ℕ) a 0)⁻¹
have rw₂ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [pow_zero, pow_zero, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹
have rw : a⁻¹ * a⁻¹ ^ n = (a ^ (n + 1))⁻¹
Tactic: rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : a⁻¹ * a⁻¹ ^ n = (a ^ (n + 1))⁻¹
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹
have rw₁ : a⁻¹ * a⁻¹ ^ n = (a ^ n * a)⁻¹
Tactic: rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : a⁻¹ * a⁻¹ ^ n = (a ^ (n + 1))⁻¹
rw₁ : a⁻¹ * a⁻¹ ^ n = (a ^ n * a)⁻¹
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹
have rw₂ : a⁻¹ * (a ^ n)⁻¹ = (a ^ n * a)⁻¹
Tactic: rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : a⁻¹ * a⁻¹ ^ n = (a ^ (n + 1))⁻¹
rw₁ : a⁻¹ * a⁻¹ ^ n = (a ^ n * a)⁻¹
rw₂ : a⁻¹ * (a ^ n)⁻¹ = (a ^ n * a)⁻¹
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹
have rw₃ : a⁻¹ * (a ^ n)⁻¹ = a⁻¹ * (a ^ n)⁻¹
Tactic: rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
n : ℕ
⊢ HPow.hPow (α := α) (β := ℤ) 1 (↑n : ℤ) = 1
have rw : HPow.hPow (α := α) 1 n = 1
Tactic: rw [zpow_natCast, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
n : ℕ
rw : HPow.hPow (α := α) 1 n = 1
⊢ HPow.hPow (α := α) (β := ℤ) 1 (↑n : ℤ) = 1
have rw₁ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [zpow_natCast, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
n : ℕ
⊢ HPow.hPow (α := α) 1 (Int.negSucc n) = 1
have rw : (HPow.hPow (α := α) 1 (n + 1))⁻¹ = 1
Tactic: rw [zpow_negSucc, one_pow, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
n : ℕ
rw : (HPow.hPow (α := α) 1 (n + 1))⁻¹ = 1
⊢ HPow.hPow (α := α) 1 (Int.negSucc n) = 1
have rw₁ : Eq.{u_1 + 1} (α := α) 1⁻¹ 1
Tactic: rw [zpow_negSucc, one_pow, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
n : ℕ
rw : (HPow.hPow (α := α) 1 (n + 1))⁻¹ = 1
rw₁ : Eq.{u_1 + 1} (α := α) 1⁻¹ 1
⊢ HPow.hPow (α := α) 1 (Int.negSucc n) = 1
have rw₂ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [zpow_negSucc, one_pow, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = (a ^ Int.negSucc n)⁻¹
have rw : a ^ (-Int.negSucc n) = HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ)
Tactic: rw [zpow_negSucc, inv_inv, ← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
⊢ HPow.hPow (β := ℤ) a⁻¹ (↑n : ℤ) = (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹
have rw : a⁻¹ ^ n = (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹
Tactic: rw [zpow_natCast, zpow_natCast, inv_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : a⁻¹ ^ n = (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹
⊢ HPow.hPow (β := ℤ) a⁻¹ (↑n : ℤ) = (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹
have rw₁ : a⁻¹ ^ n = (a ^ n)⁻¹
Tactic: rw [zpow_natCast, zpow_natCast, inv_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : a⁻¹ ^ n = (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹
rw₁ : a⁻¹ ^ n = (a ^ n)⁻¹
⊢ HPow.hPow (β := ℤ) a⁻¹ (↑n : ℤ) = (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹
have rw₂ : (a ^ n)⁻¹ = (a ^ n)⁻¹
Tactic: rw [zpow_natCast, zpow_natCast, inv_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹
have rw : (a⁻¹ ^ (n + 1))⁻¹ = (a ^ Int.negSucc n)⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, inv_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : (a⁻¹ ^ (n + 1))⁻¹ = (a ^ Int.negSucc n)⁻¹
⊢ a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹
have rw₁ : (a⁻¹ ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, inv_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : (a⁻¹ ^ (n + 1))⁻¹ = (a ^ Int.negSucc n)⁻¹
rw₁ : (a⁻¹ ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹⁻¹
⊢ a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹
have rw₂ : (a ^ (n + 1))⁻¹⁻¹ = (a ^ (n + 1))⁻¹⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, inv_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℤ
⊢ a⁻¹ ^ n = a ^ (-n)
have rw : (a ^ n)⁻¹ = a ^ (-n)
Tactic: rw [inv_zpow, zpow_neg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℤ
rw : (a ^ n)⁻¹ = a ^ (-n)
⊢ a⁻¹ ^ n = a ^ (-n)
have rw₁ : (a ^ n)⁻¹ = (a ^ n)⁻¹
Tactic: rw [inv_zpow, zpow_neg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
⊢ a = b
have rw : 1 / (1 / a) = b
Tactic: rw [← one_div_one_div a, h, one_div_one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
rw : 1 / (1 / a) = b
⊢ a = b
have rw₁ : 1 / (1 / b) = b
Tactic: rw [← one_div_one_div a, h, one_div_one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
rw : 1 / (1 / a) = b
rw₁ : 1 / (1 / b) = b
⊢ a = b
have rw₂ : b = b
Tactic: rw [← one_div_one_div a, h, one_div_one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) a (↑m : ℤ)) (↑n : ℤ)
have rw : a ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) a (↑(m * n) : ℤ)
Tactic: rw [zpow_natCast, zpow_natCast, ← 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 : ℤ) * Int.negSucc n) = HPow.hPow (β := ℤ) a (↑m : ℤ) ^ Int.negSucc n
have rw : a ^ ((↑m : ℤ) * Int.negSucc n) = (a ^ m) ^ Int.negSucc n
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
⊢ 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]