[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) = fun x_1 => x * y * x_1
[PROOFSTEP]
ext z
[GOAL]
case h
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) z = x * y * z
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 => x_1 * x) ∘ fun x => x * y) = fun x_1 => x_1 * (y * x)
[PROOFSTEP]
ext z
[GOAL]
case h
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x_1 * x) ∘ fun x => x * y) z = z * (y * x)
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : 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
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : 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
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : 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
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : 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
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 ↔ b = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 → b = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
b : M
h : 1 * b = 1
⊢ b = 1
[PROOFSTEP]
simpa using h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommSemigroup G
a b c d : G
⊢ a * b * (c * d) = a * c * (b * d)
[PROOFSTEP]
simp only [mul_left_comm, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * b * c = b * c * a
[PROOFSTEP]
simp only [mul_left_comm, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * (b * c) = b * (c * a)
[PROOFSTEP]
simp only [mul_left_comm, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : AddCommSemigroup M
inst✝ : One M
a b : M
⊢ bit1 (a + b) = bit1 a + bit0 b
[PROOFSTEP]
rw [add_comm, bit1_add, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : AddMonoid M
a b c : M
inst✝ : One M
⊢ bit1 0 = 1
[PROOFSTEP]
rw [bit1, bit0_zero, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : LeftCancelMonoid M
a b : M
⊢ a * b = a ↔ a * b = a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : RightCancelMonoid M
a b : M
⊢ a * b = b ↔ a * b = 1 * b
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a b c x : G
⊢ x⁻¹ = 1 / x
[PROOFSTEP]
rw [div_eq_mul_inv, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a b c x y : G
⊢ x * (1 / y) = x / y
[PROOFSTEP]
rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a✝ b✝ c✝ a b c : G
⊢ a * b / c = a * (b / c)
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a✝ b✝ c✝ a b c : G
⊢ a * (b / c) = a * b / c
[PROOFSTEP]
simp only [mul_assoc, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a✝ b✝ c a b : G
⊢ a / b = a * (1 / b)
[PROOFSTEP]
rw [div_eq_mul_inv, one_div]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvOneMonoid G
a : G
⊢ a / 1 = a
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : a * b = 1
⊢ b⁻¹ = a
[PROOFSTEP]
rw [← inv_eq_of_mul_eq_one_right h, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : b * a = 1
⊢ b = 1 / a
[PROOFSTEP]
rw [eq_inv_of_mul_eq_one_left h, one_div]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : a * b = 1
⊢ b = 1 / a
[PROOFSTEP]
rw [eq_inv_of_mul_eq_one_right h, one_div]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : a / b = 1
⊢ a * b⁻¹ = 1
[PROOFSTEP]
rwa [← div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ 1 / a * (1 / b) = 1 / (b * a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ a⁻¹ / b = (b * a)⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ (a / b)⁻¹ = b / a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ 1 / (a / b) = b / a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ 1 / (1 / a) = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
src✝ : DivInvMonoid α := toDivInvMonoid
⊢ 1⁻¹ = 1
[PROOFSTEP]
simpa only [one_div, inv_inv] using (inv_div (1 : α) 1).symm
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : 1 / a = 1 / b
⊢ a = b
[PROOFSTEP]
rw [← one_div_one_div a, h, one_div_one_div]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ a / (b / c) = a * c / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ a / b⁻¹ = a * b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ a / (b * c) = a / c / b
[PROOFSTEP]
simp only [mul_assoc, mul_inv_rev, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ (a / b)⁻¹ = a⁻¹ / b⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b = b⁻¹ * a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a⁻¹ * b = b / a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ (a * b)⁻¹ = a⁻¹ / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a⁻¹ / b⁻¹ = b / a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ (a⁻¹ / b⁻¹)⁻¹ = a / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ 1 / a * (1 / b) = 1 / (a * b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / c = a / c / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / c = a / (b * c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * c = a / (b / c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a * (b / c) = b * (a / c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a * b / c = a / c * b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / (b * c) = a / b / c
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * c = a * c / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * c = a * (c / b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * c = c / b * a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / (b * c) = a / b * (1 / c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a * d / (b * c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a / c / (b / d)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * (c / d) = a * c / (b * d)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a * b / (c * d) = a / c * (b / d)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a / b = b⁻¹ ↔ a = 1
[PROOFSTEP]
rw [div_eq_mul_inv, mul_left_eq_self]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * c = b
⊢ a = b * c⁻¹
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b * a = c
⊢ a = b⁻¹ * c
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b = a * c
⊢ a⁻¹ * b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c * b
⊢ a * b⁻¹ = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * c⁻¹ = b
⊢ a = b * c
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b⁻¹ * a = c
⊢ a = b * c
[PROOFSTEP]
simp [h.symm, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b = a⁻¹ * c
⊢ a * b = c
[PROOFSTEP]
rw [h, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c * b⁻¹
⊢ a * b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = b⁻¹
⊢ a * b = 1
[PROOFSTEP]
rw [h, mul_left_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a * b = 1 ↔ a⁻¹ = b
[PROOFSTEP]
rw [mul_eq_one_iff_eq_inv, inv_eq_iff_eq_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = b * c⁻¹
⊢ a * c = b
[PROOFSTEP]
rw [h, inv_mul_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * c = b
⊢ a = b * c⁻¹
[PROOFSTEP]
rw [← h, mul_inv_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = b⁻¹ * c
⊢ b * a = c
[PROOFSTEP]
rw [h, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b * a = c
⊢ a = b⁻¹ * c
[PROOFSTEP]
rw [← h, inv_mul_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a⁻¹ * b = c
⊢ b = a * c
[PROOFSTEP]
rw [← h, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b = a * c
⊢ a⁻¹ * b = c
[PROOFSTEP]
rw [h, inv_mul_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * b⁻¹ = c
⊢ a = c * b
[PROOFSTEP]
rw [← h, inv_mul_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c * b
⊢ a * b⁻¹ = c
[PROOFSTEP]
rw [h, mul_inv_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a * b⁻¹ = 1 ↔ a = b
[PROOFSTEP]
rw [mul_eq_one_iff_eq_inv, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a⁻¹ * b = 1 ↔ a = b
[PROOFSTEP]
rw [mul_eq_one_iff_eq_inv, inv_inj]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ Injective fun a => a / b
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ Injective fun a => a * b⁻¹
[PROOFSTEP]
exact fun a a' h ↦ mul_left_injective b⁻¹ h
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ Injective fun a => b / a
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ Injective fun a => b * a⁻¹
[PROOFSTEP]
exact fun a a' h ↦ inv_injective (mul_right_injective b h)
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c d a b : G
⊢ a / b * b = a
[PROOFSTEP]
rw [div_eq_mul_inv, inv_mul_cancel_right a b]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b c d a : G
⊢ a / a = 1
[PROOFSTEP]
rw [div_eq_mul_inv, mul_right_inv a]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c d a b : G
⊢ a * b / b = a
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_cancel_right a b]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c d a b : G
⊢ a / (b * a) = b⁻¹
[PROOFSTEP]
rw [← inv_div, mul_div_cancel'']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a * c / (b * c) = a / b
[PROOFSTEP]
rw [div_mul_eq_div_div_swap]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a * c / c / b = a / b
[PROOFSTEP]
simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel'']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * c = b
⊢ a = b / c
[PROOFSTEP]
simp [← h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c * b
⊢ a / b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a / c = b
⊢ a = b * c
[PROOFSTEP]
simp [← h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c / b
⊢ a * b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ b / a = c / a ↔ b = c
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ b * a⁻¹ = c * a⁻¹ ↔ b = c
[PROOFSTEP]
exact mul_left_inj _
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a / b * (b / c) = a / c
[PROOFSTEP]
rw [← mul_div_assoc, div_mul_cancel']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a / c / (b / c) = a / b
[PROOFSTEP]
rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = b
⊢ a / b = 1
[PROOFSTEP]
rw [h, div_self']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a / b = a ↔ b = 1
[PROOFSTEP]
rw [div_eq_mul_inv, mul_right_eq_self, inv_eq_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a = b / c ↔ a * c = b
[PROOFSTEP]
rw [div_eq_mul_inv, eq_mul_inv_iff_mul_eq]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a / b = c ↔ a = c * b
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
H : a / b = c / d
⊢ a = b ↔ c = d
[PROOFSTEP]
rw [← div_eq_one, H, div_eq_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
n : ℤ
hn : n ≠ 0
x : G
h : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ Int.ofNat n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
simp only [Int.ofNat_eq_coe] at h 
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ ↑n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
rw [zpow_ofNat] at h 
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
refine' ⟨n, Nat.pos_of_ne_zero fun n0 ↦ hn ?_, h⟩
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
n0 : n = 0
⊢ Int.ofNat n = 0
[PROOFSTEP]
rw [n0]
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
n0 : n = 0
⊢ Int.ofNat 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.negSucc n ≠ 0
h : x ^ Int.negSucc n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
rw [zpow_negSucc, inv_eq_one] at h 
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.negSucc n ≠ 0
h : x ^ (n + 1) = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
refine' ⟨n + 1, n.succ_pos, h⟩
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
h : a = b * c
⊢ a / b = c
[PROOFSTEP]
rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ c * a / (c * b) = a / b
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_rev, mul_comm b⁻¹ c⁻¹, mul_comm c a, mul_assoc, ← mul_assoc c, mul_right_inv, one_mul,
  div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
h : c * a = b
⊢ a = b / c
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
h : a / b = c
⊢ a = b * c
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
h : b = c / a
⊢ a * b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
h : b = c / a
⊢ a * (c * a⁻¹) = c
[PROOFSTEP]
rw [mul_comm c, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a / (a / b) = b
[PROOFSTEP]
simpa using mul_inv_cancel_left a b
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a / b = c / b * (a / c)
[PROOFSTEP]
simp [mul_left_comm c]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a / b / a = b⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a = b / c ↔ c * a = b
[PROOFSTEP]
rw [eq_div_iff_mul_eq', mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c ↔ a = b * c
[PROOFSTEP]
rw [div_eq_iff_eq_mul, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a * b / a = b
[PROOFSTEP]
rw [div_eq_inv_mul, inv_mul_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a * (b / a) = b
[PROOFSTEP]
rw [← mul_div_assoc, mul_div_cancel''']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a / (a * b) = b⁻¹
[PROOFSTEP]
rw [← inv_div, mul_div_cancel''']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a * (b * a⁻¹) = b
[PROOFSTEP]
rw [← div_eq_mul_inv, mul_div_cancel'_right a b]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a * c * (b / c) = a * b
[PROOFSTEP]
rw [mul_assoc, mul_div_cancel'_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a / c * (b * c) = a * b
[PROOFSTEP]
rw [mul_left_comm, div_mul_cancel', mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a / b * (c / a) = c / b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ c / a * (a / b) = c / b
[PROOFSTEP]
apply div_mul_div_cancel'
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a * b / (a / c) = b * c
[PROOFSTEP]
rw [← div_mul, mul_div_cancel''']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ c / a / (c / b) = b / a
[PROOFSTEP]
rw [← inv_div b c, div_inv_eq_mul, mul_comm, div_mul_div_cancel']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b
[PROOFSTEP]
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ c * b = d * a ↔ a * d = c * b
[PROOFSTEP]
simp only [mul_comm, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a / c = b / d
[PROOFSTEP]
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, div_eq_iff_eq_mul', mul_div_assoc]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
⊢ f a c = f a b * f b c
[PROOFSTEP]
have hmul' : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c :=
  by
  intros b c rbc pab pbc pac
  obtain rab | rba := total_of r a b
  · exact hmul rab rbc pab pbc pac
  rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
  obtain rac | rca := total_of r a c
  · rw [hmul rba rac (hsymm pab) pac pbc]
  · rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
⊢ ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
[PROOFSTEP]
intros b c rbc pab pbc pac
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
⊢ f a c = f a b * f b c
[PROOFSTEP]
obtain rab | rba := total_of r a b
[GOAL]
case inl
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rab : r a b
⊢ f a c = f a b * f b c
[PROOFSTEP]
exact hmul rab rbc pab pbc pac
[GOAL]
case inr
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a c = f a b * f b c
[PROOFSTEP]
rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
[GOAL]
case inr
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a b * (f b a * f a c) = f a b * f b c
[PROOFSTEP]
obtain rac | rca := total_of r a c
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rac : r a c
⊢ f a b * (f b a * f a c) = f a b * f b c
[PROOFSTEP]
rw [hmul rba rac (hsymm pab) pac pbc]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rca : r c a
⊢ f a b * (f b a * f a c) = f a b * f b c
[PROOFSTEP]
rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
⊢ f a c = f a b * f b c
[PROOFSTEP]
obtain rbc | rcb := total_of r b c
[GOAL]
case inl
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rbc : r b c
⊢ f a c = f a b * f b c
[PROOFSTEP]
exact hmul' rbc pab pbc pac
[GOAL]
case inr
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rcb : r c b
⊢ f a c = f a b * f b c
[PROOFSTEP]
rw [hmul' rcb pac (hsymm pbc) pab, mul_assoc, hf_swap (hsymm pbc), mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ f a c = f a b * f b c
[PROOFSTEP]
apply multiplicative_of_symmetric_of_isTotal (fun a b => p a ∧ p b) r f fun _ _ => And.symm
[GOAL]
case hf_swap
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ ∀ {a b : α}, p a ∧ p b → f a b * f b a = 1
[PROOFSTEP]
simp_rw [and_imp]
[GOAL]
case hf_swap
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ ∀ {a b : α}, p a → p b → f a b * f b a = 1
[PROOFSTEP]
exact @hswap
[GOAL]
case hmul
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ ∀ {a b c : α}, r a b → r b c → p a ∧ p b → p b ∧ p c → p a ∧ p c → f a c = f a b * f b c
[PROOFSTEP]
exact fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2
[GOAL]
case pab
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p a ∧ p b
case pbc
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p b ∧ p c
case pac
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p a ∧ p c
[PROOFSTEP]
exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]
