awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
c : β
h : ¬p
⊢ b h ^ c = b h ^ c

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : α
b c : β
⊢ (a ^ if p then b else c) = if p then a ^ b else a ^ c

Tactic:
pow_dite _ _ _ _

Premises used: pow_dite, ite
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a b : α
c : β
⊢ (if p then a else b) ^ c = if p then a ^ c else b ^ c

Tactic:
dite_pow _ _ _ _

Premises used: dite_pow, ite
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
inst : Semigroup α
⊢ Std.Associative fun (x1 x2 : α) ↦ x1 * x2

Tactic:
⟨mul_assoc⟩

Premises used: mul_assoc, Std.Associative.mk
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : Semigroup α
x y : α
h : ∀ (z : α), ((fun (x_1 : α) ↦ x * x_1) ∘ fun (x : α) ↦ y * x) z = x * y * z
⊢ Eq.{u_1 + 1} (α := α → α) ((fun (x_1 : α) ↦ x * x_1) ∘ fun (x : α) ↦ y * x) fun (x_1 : α) ↦ x * y * x_1

Tactic:
ext z
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : Semigroup α
x y z : α
⊢ ((fun (x_1 : α) ↦ x * x_1) ∘ fun (x : α) ↦ y * x) z = x * y * z

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : Semigroup α
x y : α
h : ∀ (z : α), ((fun (x_1 : α) ↦ x_1 * x) ∘ fun (x : α) ↦ x * y) z = z * (y * x)
⊢ Eq.{u_1 + 1} (α := α → α) ((fun (x_1 : α) ↦ x_1 * x) ∘ fun (x : α) ↦ x * y) fun (x_1 : α) ↦ x_1 * (y * x)

Tactic:
ext z
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : Semigroup α
x y z : α
⊢ ((fun (x_1 : α) ↦ x_1 * x) ∘ fun (x : α) ↦ x * y) z = z * (y * x)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Basic
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
neg : ∀ (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

Tactic:
by_cases h : P
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : MulOneClass M
P : Prop
inst_1 : Decidable P
a b : M
h : P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : MulOneClass M
P : Prop
inst_1 : Decidable P
a b : M
h : ¬P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Basic
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
neg : ∀ (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

Tactic:
by_cases h : P
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : MulOneClass M
P : Prop
inst_1 : Decidable P
a b : M
h : P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : MulOneClass M
P : Prop
inst_1 : Decidable P
a b : M
h : ¬P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : MulOneClass M
a b : M
h : a * b = 1
mp : a = 1 → b = 1
mpr : b = 1 → a = 1
⊢ a = 1 ↔ b = 1

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : MulOneClass M
b : M
h : 1 * b = 1
⊢ b = 1

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : MulOneClass M
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ 1 * x) id

Tactic:
funext one_mul

Premises used: funext, one_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : MulOneClass M
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ x * 1) id

Tactic:
funext mul_one

Premises used: funext, mul_one
-- Module: Mathlib.Algebra.Group.Basic
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)
rw₂ rw₃ : b * (a * c) = b * (a * c)
⊢ a * (b * c) = b * (a * c)

Tactic:
rw [← mul_assoc, mul_comm a, mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.Group.Basic
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
rw₂ rw₃ : a * (c * b) = a * (c * b)
⊢ a * b * c = a * c * b

Tactic:
rw [mul_assoc, mul_comm b, mul_assoc]

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

Tactic:
simp only [mul_left_comm, mul_assoc]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommSemigroup G
a b c d : G
⊢ a * b * c * d = a * c * b * d

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : CommSemigroup G
a b c : G
⊢ a * b * c = b * c * a

Tactic:
simp only [mul_left_comm, mul_comm]

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

Tactic:
simp only [mul_left_comm, mul_comm]

Premises used: mul_left_comm, mul_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
P : Prop
inst_1 : Decidable P
a : M
⊢ HPow.hPow (β := ℕ) a (if P then 1 else 0) = if P then a else 1

Tactic:
simp only [pow_ite, pow_one, pow_zero]

Premises used: pow_ite, pow_zero, pow_one
-- Module: Mathlib.Algebra.Group.Basic
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
rw₂ rw₃ : a ^ n = a ^ n
⊢ a ^ m * a ^ (n - m) = a ^ n

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

Premises used: pow_add, Nat.sub_add_cancel, Nat.add_comm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
m n : ℕ
a : M
h : m ≤ n
rw : a ^ (n - m + m) = a ^ n
rw₁ rw₂ : a ^ n = a ^ n
⊢ a ^ (n - m) * a ^ m = a ^ n

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

Premises used: pow_add, Nat.sub_add_cancel
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
hn : n ≠ 0
a : M
rw : a ^ (n - 1 + 1) = a ^ n
rw₁ rw₂ : a ^ n = a ^ n
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
rw [← pow_succ', Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]

Premises used: Iff.mpr, Nat.sub_add_cancel, Nat.one_le_iff_ne_zero, pow_succ'
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
hn : n ≠ 0
a : M
rw : a ^ (n - 1 + 1) = a ^ n
rw₁ rw₂ : a ^ n = a ^ n
⊢ a ^ (n - 1) * a = a ^ n

Tactic:
rw [← pow_succ, Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]

Premises used: Iff.mpr, pow_succ, Nat.sub_add_cancel, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
rw rw₁ : a ^ m = a ^ m
⊢ a ^ m = a ^ (m % n + n * (m / n))

Tactic:
rw [Nat.mod_add_div]

Premises used: Nat.mod_add_div
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ (m % n + n * (m / n)) = a ^ (m % n)

Tactic:
simp [pow_add, pow_mul, ha]

Premises used: pow_add, pow_mul
-- Module: Mathlib.Algebra.Group.Basic
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₂ : a ^ (m % n + n * (m / n)) = a ^ (m % n)
⊢ a ^ m = 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]

Premises used: HMul.hMul, HDiv.hDiv, HMod.hMod, HAdd.hAdd
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a b : M
h : a * b = 1
⊢ HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
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)
rw₁ rw₂ : a ^ n * a * (b * b ^ n) = a ^ n * a * (b * b ^ n)
⊢ a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)

Tactic:
rw [pow_succ, pow_succ']

Premises used: pow_succ, pow_succ'
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n * a * (b * b ^ n) = a ^ n * (a * b) * b ^ n

Tactic:
simp only [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n * (a * b) * b ^ n = 1

Tactic:
simp [h, pow_mul_pow_eq_one]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
h : ∀ (x : M), (fun (x : M) ↦ a * x)^[0] x = HPow.hPow (β := ℕ) a 0 * x
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ a * x)^[0] fun (x : M) ↦ HPow.hPow (β := ℕ) a 0 * x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a x : M
⊢ (fun (x : M) ↦ a * x)^[0] x = HPow.hPow (β := ℕ) a 0 * x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
n : ℕ
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ a * x)^[n + 1] fun (x : M) ↦ a ^ (n + 1) * x

Tactic:
simp [pow_succ, mul_left_iterate]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
h : ∀ (x : M), (fun (x : M) ↦ x * a)^[0] x = x * HPow.hPow (β := ℕ) a 0
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ x * a)^[0] fun (x : M) ↦ x * HPow.hPow (β := ℕ) a 0

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a x : M
⊢ (fun (x : M) ↦ x * a)^[0] x = x * HPow.hPow (β := ℕ) a 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
n : ℕ
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ x * a)^[n + 1] fun (x : M) ↦ x * a ^ (n + 1)

Tactic:
simp [pow_succ', mul_right_iterate]

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
a b : M
⊢ (fun (x : M) ↦ a * x)^[n] b = a ^ n * b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
a b : M
⊢ (fun (x : M) ↦ x * a)^[n] b = b * a ^ n

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
a : M
⊢ (fun (x : M) ↦ a * x)^[n] 1 = a ^ n

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
n : ℕ
a : M
⊢ (fun (x : M) ↦ x * a)^[n] 1 = a ^ n

Tactic:
simp [mul_right_iterate]

Premises used: mul_right_iterate
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
k : ℕ
h : ∀ (x : M), (fun (x : M) ↦ x ^ k)^[0] x = x ^ HPow.hPow (β := ℕ) k 0
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ x ^ k)^[0] fun (x : M) ↦ x ^ HPow.hPow (β := ℕ) k 0

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

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
k n : ℕ
h : ∀ (x : M), (fun (x : M) ↦ x ^ k)^[n + 1] x = x ^ k ^ (n + 1)
⊢ Eq.{u_4 + 1} (α := M → M) (fun (x : M) ↦ x ^ k)^[n + 1] fun (x : M) ↦ x ^ k ^ (n + 1)

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

Tactic:
simp [pow_iterate, Nat.pow_succ', pow_mul]

Premises used: Nat.pow_succ', pow_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x y z : M
hy : x * y = 1
hz : x * z = 1
⊢ y = z

Tactic:
left_inv_eq_right_inv (Trans.trans (mul_comm _ _) hy) hz

Premises used: Trans.trans, left_inv_eq_right_inv, mul_comm
-- Module: Mathlib.Algebra.Group.Basic
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
rw₃ rw₄ : Eq.{u_4 + 1} (α := M) 1 1
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0

Tactic:
rw [pow_zero, pow_zero, pow_zero, one_mul]

Premises used: pow_zero, one_mul
-- Module: Mathlib.Algebra.Group.Basic
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)
rw₄ rw₅ : a * a ^ n * (b * b ^ n) = a * a ^ n * (b * b ^ n)
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, pow_succ'
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsLeftCancelMul M
a b : M
rw rw₁ : a * b = a ↔ a * b = a
⊢ a * b = a ↔ a * b = a * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsLeftCancelMul M
a b : M
⊢ a = a * b ↔ b = 1

Tactic:
eq_comm.trans mul_eq_left

Premises used: eq_comm, mul_eq_left, Iff.trans
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsLeftCancelMul M
a b : M
⊢ a * b ≠ a ↔ b ≠ 1

Tactic:
mul_eq_left.not

Premises used: Iff.not, mul_eq_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsLeftCancelMul M
a b : M
⊢ a ≠ a * b ↔ b ≠ 1

Tactic:
left_eq_mul.not

Premises used: Iff.not, left_eq_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsRightCancelMul M
a b : M
rw rw₁ : a * b = b ↔ a * b = b
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsRightCancelMul M
a b : M
⊢ b = a * b ↔ a = 1

Tactic:
eq_comm.trans mul_eq_right

Premises used: mul_eq_right, eq_comm, Iff.trans
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsRightCancelMul M
a b : M
⊢ a * b ≠ b ↔ a ≠ 1

Tactic:
mul_eq_right.not

Premises used: mul_eq_right, Iff.not
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : IsRightCancelMul M
a b : M
⊢ b ≠ a * b ↔ a ≠ 1

Tactic:
right_eq_mul.not

Premises used: Iff.not, right_eq_mul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a = c ↔ b = d

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a ≠ c ↔ b ≠ d

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : InvolutiveInv G
⊢ Involutive.{u_3 + 1} (α := G) Inv.inv

Tactic:
inv_inv

Premises used: inv_inv, Function.Involutive
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : InvolutiveInv G
⊢ Bijective.{u_3 + 1, u_3 + 1} (α := G) Inv.inv

Tactic:
inv_involutive.bijective

Premises used: inv_involutive, Function.Involutive.bijective
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : InvolutiveInv G
⊢ Surjective.{u_3 + 1, u_3 + 1} (α := G) Inv.inv

Tactic:
inv_involutive.surjective

Premises used: Function.Involutive.surjective, inv_involutive
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : InvolutiveInv G
⊢ Injective.{u_3 + 1, u_3 + 1} (α := G) Inv.inv

Tactic:
inv_involutive.injective

Premises used: Function.Involutive.injective, inv_involutive
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : InvolutiveInv G
a b : G
⊢ a⁻¹ = b⁻¹ ↔ a = b

Tactic:
inv_injective.eq_iff

Premises used: Function.Injective.eq_iff, inv_injective
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : InvolutiveInv G
a b : G
⊢ a⁻¹ = b ↔ a = b⁻¹

Tactic:
inv_involutive.eq_iff

Premises used: inv_involutive, Function.Involutive.eq_iff
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : InvolutiveInv G
⊢ Eq.{u_3 + 1} (α := G → G) (Inv.inv ∘ Inv.inv) id

Tactic:
inv_involutive.comp_self

Premises used: inv_involutive, Function.Involutive.comp_self
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : InvolutiveInv G
⊢ LeftInverse (fun (a : G) ↦ a⁻¹) fun (a : G) ↦ a⁻¹

Tactic:
inv_inv

Premises used: Function.LeftInverse, inv_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : InvolutiveInv G
⊢ RightInverse (fun (a : G) ↦ a⁻¹) fun (a : G) ↦ a⁻¹

Tactic:
inv_inv

Premises used: Function.LeftInverse, inv_inv, Function.RightInverse
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : DivInvMonoid G
x y : G
rw : x * (1 * y⁻¹) = x / y
rw₁ : x * y⁻¹ = x / y
rw₂ rw₃ : x * y⁻¹ = x * y⁻¹
⊢ x * (1 / y) = x / y

Tactic:
rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]

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

Tactic:
(mul_div_assoc _ _ _).symm

Premises used: mul_div_assoc, Eq.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : DivInvMonoid G
a b c : G
⊢ a * (b / c) = a * b / c

Tactic:
simp only [mul_assoc, div_eq_mul_inv]

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

Tactic:
rw [div_eq_mul_inv, one_div]

Premises used: div_eq_mul_inv, one_div
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : DivInvOneMonoid G
a : G
⊢ a / 1 = a

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
G : Type u_3
inst : DivInvOneMonoid G
⊢ 1 / 1 = 1

Tactic:
div_one _

Premises used: div_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : a * b = 1
⊢ b = a⁻¹

Tactic:
(inv_eq_of_mul_eq_one_right h).symm

Premises used: inv_eq_of_mul_eq_one_right, Eq.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : b * a = 1
rw : a⁻¹ = 1 / a
rw₁ rw₂ : a⁻¹ = a⁻¹
⊢ b = 1 / a

Tactic:
rw [eq_inv_of_mul_eq_one_left h, one_div]

Premises used: eq_inv_of_mul_eq_one_left, one_div
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : a * b = 1
rw : a⁻¹ = 1 / a
rw₁ rw₂ : a⁻¹ = a⁻¹
⊢ b = 1 / a

Tactic:
rw [eq_inv_of_mul_eq_one_right h, one_div]

Premises used: one_div, eq_inv_of_mul_eq_one_right
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h rwa rwa₁ rwa₂ rwa₃ : a / b = 1
⊢ a * b⁻¹ = 1

Tactic:
rwa [← div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : a⁻¹ * b = 1
⊢ a = b

Tactic:
simpa using eq_inv_of_mul_eq_one_left h

Premises used: eq_inv_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
h : a * b⁻¹ = 1
⊢ a = b

Tactic:
simpa using eq_inv_of_mul_eq_one_left h

Premises used: eq_inv_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
⊢ a ≠ b → a / b ≠ 1

Tactic:
mt eq_of_div_eq_one

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

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

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

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

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

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

Tactic:
simp only [inv_div]

Premises used: inv_div
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
inst : DivisionMonoid α
a b c d : α
⊢ Eq.{u_1 + 1} (α := α) 1⁻¹ 1

Tactic:
simpa only [one_div, inv_inv] using (inv_div (1 : α) 1).symm

Premises used: inv_inv, one_div, inv_div, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
rw : 1 = (HPow.hPow (β := ℕ) a 0)⁻¹
rw₁ : Eq.{u_1 + 1} (α := α) 1 1⁻¹
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) 1 1
⊢ HPow.hPow (β := ℕ) a⁻¹ 0 = (HPow.hPow (β := ℕ) a 0)⁻¹

Tactic:
rw [pow_zero, pow_zero, inv_one]

Premises used: inv_one, pow_zero
-- Module: Mathlib.Algebra.Group.Basic
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)⁻¹
rw₃ rw₄ : a⁻¹ * (a ^ n)⁻¹ = a⁻¹ * (a ^ n)⁻¹
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹

Tactic:
rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]

Premises used: pow_succ, mul_inv_rev, pow_succ'
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
n : ℕ
rw : HPow.hPow (α := α) 1 n = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) 1 1
⊢ HPow.hPow (α := α) (β := ℤ) 1 (↑n : ℤ) = 1

Tactic:
rw [zpow_natCast, one_pow]

Premises used: zpow_natCast, one_pow
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
n : ℕ
rw : (HPow.hPow (α := α) 1 (n + 1))⁻¹ = 1
rw₁ : Eq.{u_1 + 1} (α := α) 1⁻¹ 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) 1 1
⊢ HPow.hPow (α := α) 1 (Int.negSucc n) = 1

Tactic:
rw [zpow_negSucc, one_pow, inv_one]

Premises used: one_pow, inv_one, zpow_negSucc
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
⊢ HPow.hPow (β := ℤ) a (-0) = (HPow.hPow (β := ℤ) a 0)⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : a ^ (-Int.negSucc n) = HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ)
⊢ a ^ (-Int.negSucc n) = (a ^ Int.negSucc n)⁻¹

Tactic:
rw [zpow_negSucc, inv_inv, ← zpow_natCast]

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

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a b : α
⊢ HPow.hPow (β := ℤ) (a * b) (-1) = HPow.hPow (β := ℤ) b (-1) * HPow.hPow (β := ℤ) a (-1)

Tactic:
simp only [zpow_neg, zpow_one, mul_inv_rev]

Premises used: zpow_one, zpow_neg, mul_inv_rev
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : a⁻¹ ^ n = (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹
rw₁ : a⁻¹ ^ n = (a ^ n)⁻¹
rw₂ rw₃ : (a ^ n)⁻¹ = (a ^ n)⁻¹
⊢ HPow.hPow (β := ℤ) a⁻¹ (↑n : ℤ) = (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹

Tactic:
rw [zpow_natCast, zpow_natCast, inv_pow]

Premises used: zpow_natCast, inv_pow
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
rw : (a⁻¹ ^ (n + 1))⁻¹ = (a ^ Int.negSucc n)⁻¹
rw₁ : (a⁻¹ ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹⁻¹
rw₂ rw₃ : (a ^ (n + 1))⁻¹⁻¹ = (a ^ (n + 1))⁻¹⁻¹
⊢ a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹

Tactic:
rw [zpow_negSucc, zpow_negSucc, inv_pow]

Premises used: zpow_negSucc, inv_pow
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℤ
rw : (a ^ n)⁻¹ = a ^ (-n)
rw₁ rw₂ : (a ^ n)⁻¹ = (a ^ n)⁻¹
⊢ a⁻¹ ^ n = a ^ (-n)

Tactic:
rw [inv_zpow, zpow_neg]

Premises used: inv_zpow, zpow_neg
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℕ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
simp only [one_div, inv_pow]

Premises used: inv_pow, one_div
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
n : ℤ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
simp only [one_div, inv_zpow]

Premises used: inv_zpow, one_div
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
inst : DivisionMonoid α
a : α
⊢ a⁻¹ = 1 ↔ a = 1

Tactic:
inv_injective.eq_iff' inv_one

Premises used: inv_one, Function.Injective.eq_iff', inv_injective