[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
⊢ ∀ (n : ℕ), n • 1 = ↑n
[PROOFSTEP]
let f : ℕ →+ A := { toFun := fun n ↦ n • (1 : A), map_zero' := by simp [zero_nsmul], map_add' := by simp [add_nsmul] }
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
⊢ (fun n => n • 1) 0 = 0
[PROOFSTEP]
simp [zero_nsmul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
⊢ ∀ (x y : ℕ),
    ZeroHom.toFun { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) } (x + y) =
      ZeroHom.toFun { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) } x +
        ZeroHom.toFun { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) } y
[PROOFSTEP]
simp [add_nsmul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
f : ℕ →+ A :=
  { toZeroHom := { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) },
    map_add' := (_ : ∀ (a a_1 : ℕ), (a + a_1) • 1 = a • 1 + a_1 • 1) }
⊢ ∀ (n : ℕ), n • 1 = ↑n
[PROOFSTEP]
refine' eq_natCast' f _
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
f : ℕ →+ A :=
  { toZeroHom := { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) },
    map_add' := (_ : ∀ (a a_1 : ℕ), (a + a_1) • 1 = a • 1 + a_1 • 1) }
⊢ ↑f 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
m : M
inst✝ : Invertible m
n : ℕ
⊢ ⅟m ^ n * m ^ n = 1
[PROOFSTEP]
rw [← (commute_invOf m).symm.mul_pow, invOf_mul_self, one_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
m : M
inst✝ : Invertible m
n : ℕ
⊢ m ^ n * ⅟m ^ n = 1
[PROOFSTEP]
rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : AddMonoid A
inst✝ : AddMonoid B
u : Mˣ
x : M
n : ℕ
hn : n ≠ 0
hu : x ^ n = ↑u
⊢ x * x ^ (n - 1) = ↑u
[PROOFSTEP]
rwa [← _root_.pow_succ, Nat.sub_add_cancel (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn)]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : AddMonoid A
inst✝ : AddMonoid B
x : M
n : ℕ
hx : x ^ n = 1
hn : n ≠ 0
⊢ ↑(ofPowEqOne x n hx hn ^ n) = ↑1
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : AddMonoid A
inst✝³ : AddMonoid B
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
k : M
x : N
p : ℕ
⊢ (k • x) ^ p = k ^ p • x ^ p
[PROOFSTEP]
induction' p with p IH
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : AddMonoid A
inst✝³ : AddMonoid B
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
k : M
x : N
⊢ (k • x) ^ Nat.zero = k ^ Nat.zero • x ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : AddMonoid A
inst✝³ : AddMonoid B
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
k : M
x : N
p : ℕ
IH : (k • x) ^ p = k ^ p • x ^ p
⊢ (k • x) ^ Nat.succ p = k ^ Nat.succ p • x ^ Nat.succ p
[PROOFSTEP]
rw [pow_succ', IH, smul_mul_smul, ← pow_succ', ← pow_succ']
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
n : ℕ
⊢ x • m ^ n = (x • m) ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
⊢ x • m ^ Nat.zero = (x • m) ^ Nat.zero
[PROOFSTEP]
rw [pow_zero, pow_zero]
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
⊢ x • 1 = 1
[PROOFSTEP]
exact smul_one x
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
n : ℕ
ih : x • m ^ n = (x • m) ^ n
⊢ x • m ^ Nat.succ n = (x • m) ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
n : ℕ
ih : x • m ^ n = (x • m) ^ n
⊢ x • (m * m ^ n) = x • m * (x • m) ^ n
[PROOFSTEP]
exact (smul_mul' x m (m ^ n)).trans (congr_arg _ ih)
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddGroupWithOne A
n : ℤ
⊢ n • 1 = ↑n
[PROOFSTEP]
cases n
[GOAL]
case ofNat
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddGroupWithOne A
a✝ : ℕ
⊢ ofNat a✝ • 1 = ↑(ofNat a✝)
[PROOFSTEP]
simp
[GOAL]
case negSucc
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddGroupWithOne A
a✝ : ℕ
⊢ -[a✝+1] • 1 = ↑-[a✝+1]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = (a ^ ↑m) ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, ← pow_mul, ← zpow_ofNat]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = a ^ ↑(m * n)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * -[n+1]) = (a ^ ↑m) ^ -[n+1]
[PROOFSTEP]
rw [zpow_ofNat, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg, inv_inj, ← zpow_ofNat]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (-[m+1] * ↑n) = (a ^ -[m+1]) ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, zpow_negSucc, ← inv_pow, ← pow_mul, negSucc_mul_ofNat, zpow_neg, inv_pow, inv_inj, ← zpow_ofNat]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (-[m+1] * -[n+1]) = (a ^ -[m+1]) ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ← zpow_ofNat]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑(Nat.succ m) * ↑(Nat.succ n)) = a ^ ↑((m + 1) * (n + 1))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
m n : ℤ
⊢ a ^ (m * n) = (a ^ n) ^ m
[PROOFSTEP]
rw [mul_comm, zpow_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ bit0 ↑n = a ^ ↑n * a ^ ↑n
[PROOFSTEP]
simp only [zpow_ofNat, ← Int.ofNat_bit0, pow_bit0]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ bit0 -[n+1] = a ^ -[n+1] * a ^ -[n+1]
[PROOFSTEP]
simp [← mul_inv_rev, ← pow_bit0]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ bit0 -[n+1] = (a ^ bit0 (n + 1))⁻¹
[PROOFSTEP]
rw [negSucc_eq, bit0_neg, zpow_neg]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ (a ^ bit0 (↑n + 1))⁻¹ = (a ^ bit0 (n + 1))⁻¹
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
x : α
n : ℤ
⊢ (-x) ^ bit0 n = x ^ bit0 n
[PROOFSTEP]
rw [zpow_bit0', zpow_bit0', neg_mul_neg]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a
[PROOFSTEP]
simp only [← Int.ofNat_succ, zpow_ofNat, pow_succ']
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
⊢ a ^ (-[0+1] + 1) = a ^ -[0+1] * a
[PROOFSTEP]
erw [zpow_zero, zpow_negSucc, pow_one, mul_left_inv]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-[n + 1+1] + 1) = a ^ -[n + 1+1] * a
[PROOFSTEP]
rw [zpow_negSucc, pow_succ, mul_inv_rev, inv_mul_cancel_right]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-[n + 1+1] + 1) = (a ^ (n + 1))⁻¹
[PROOFSTEP]
rw [Int.negSucc_eq, neg_add, add_assoc, neg_add_self, add_zero]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-↑(n + 1)) = (a ^ (n + 1))⁻¹
[PROOFSTEP]
exact zpow_negSucc _ _
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
[PROOFSTEP]
rw [← zpow_add_one, sub_add_cancel]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
induction' n using Int.induction_on with n ihn n ihn
[GOAL]
case hz
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0
case hp
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)
case hn
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)
[PROOFSTEP]
case hz => simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0
[PROOFSTEP]
case hz => simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0
[PROOFSTEP]
simp
[GOAL]
case hp
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)
[PROOFSTEP]
simp only [← add_assoc, zpow_add_one, ihn, mul_assoc]
[GOAL]
case hn
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)
[PROOFSTEP]
rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, add_sub_assoc]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
⊢ b * b ^ m = b ^ (m + 1)
[PROOFSTEP]
conv_lhs =>
  congr
  rw [← zpow_one b]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b * b ^ m
[PROOFSTEP]
  congr
  rw [← zpow_one b]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b * b ^ m
[PROOFSTEP]
  congr
  rw [← zpow_one b]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b * b ^ m
[PROOFSTEP]
congr
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b
case a
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b ^ m
[PROOFSTEP]
rw [← zpow_one b]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
⊢ b ^ 1 * b ^ m = b ^ (m + 1)
[PROOFSTEP]
rw [← zpow_add, add_comm]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
⊢ b ^ m * b = b ^ (m + 1)
[PROOFSTEP]
conv_lhs =>
  congr
  ·skip
  rw [← zpow_one b]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b ^ m * b
[PROOFSTEP]
  congr
  ·skip
  rw [← zpow_one b]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b ^ m * b
[PROOFSTEP]
  congr
  ·skip
  rw [← zpow_one b]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b ^ m * b
[PROOFSTEP]
congr
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b ^ m
case a
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b
[PROOFSTEP]
·skip
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b ^ m
[PROOFSTEP]
skip
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b ^ m
[PROOFSTEP]
skip
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b ^ m
[PROOFSTEP]
skip
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
| b
[PROOFSTEP]
rw [← zpow_one b]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
⊢ b ^ m * b ^ 1 = b ^ (m + 1)
[PROOFSTEP]
rw [← zpow_add, add_comm]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
rw [sub_eq_add_neg, zpow_add, zpow_neg]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
i : ℤ
⊢ a ^ (1 + i) = a * a ^ i
[PROOFSTEP]
rw [zpow_add, zpow_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ bit1 n = a ^ n * a ^ n * a
[PROOFSTEP]
rw [bit1, zpow_add, zpow_bit0, zpow_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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)
[PROOFSTEP]
induction' n using Int.induction_on with n ih n ih
[GOAL]
case hz
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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)
⊢ P (g ^ 0)
[PROOFSTEP]
rwa [zpow_zero]
[GOAL]
case hp
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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 (g ^ ↑n)
⊢ P (g ^ (↑n + 1))
[PROOFSTEP]
rw [add_comm, zpow_add, zpow_one]
[GOAL]
case hp
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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 (g ^ ↑n)
⊢ P (g * g ^ ↑n)
[PROOFSTEP]
exact h_mul _ ih
[GOAL]
case hn
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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 (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))
[PROOFSTEP]
rw [sub_eq_add_neg, add_comm, zpow_add, zpow_neg_one]
[GOAL]
case hn
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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 (g ^ (-↑n))
⊢ P (g⁻¹ * g ^ (-↑n))
[PROOFSTEP]
exact h_inv _ ih
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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)
[PROOFSTEP]
induction' n using Int.induction_on with n ih n ih
[GOAL]
case hz
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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⁻¹)
⊢ P (g ^ 0)
[PROOFSTEP]
rwa [zpow_zero]
[GOAL]
case hp
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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 (g ^ ↑n)
⊢ P (g ^ (↑n + 1))
[PROOFSTEP]
rw [zpow_add_one]
[GOAL]
case hp
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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 (g ^ ↑n)
⊢ P (g ^ ↑n * g)
[PROOFSTEP]
exact h_mul _ ih
[GOAL]
case hn
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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 (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))
[PROOFSTEP]
rw [zpow_sub_one]
[GOAL]
case hn
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
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 (g ^ (-↑n))
⊢ P (g ^ (-↑n) * g⁻¹)
[PROOFSTEP]
exact h_inv _ ih
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m n : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
⊢ 1 < a ^ k
[PROOFSTEP]
obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le hk.le
[GOAL]
case intro
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m n✝ : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
n : ℕ
hn : k = ↑n
⊢ 1 < a ^ k
[PROOFSTEP]
rw [hn, zpow_ofNat]
[GOAL]
case intro
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m n✝ : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
n : ℕ
hn : k = ↑n
⊢ 1 < a ^ n
[PROOFSTEP]
refine' one_lt_pow' ha (coe_nat_pos.mp _).ne'
[GOAL]
case intro
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m n✝ : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
n : ℕ
hn : k = ↑n
⊢ 0 < ↑n
[PROOFSTEP]
rwa [← hn]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m✝ n✝ : ℤ
a b : α
ha : 1 < a
m n : ℤ
h : m < n
⊢ a ^ m * a ^ (n - m) = a ^ n
[PROOFSTEP]
rw [← zpow_add]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m✝ n✝ : ℤ
a b : α
ha : 1 < a
m n : ℤ
h : m < n
⊢ a ^ (m + (n - m)) = a ^ n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m✝ n✝ : ℤ
a b : α
ha : 1 ≤ a
m n : ℤ
h : m ≤ n
⊢ a ^ m * a ^ (n - m) = a ^ n
[PROOFSTEP]
rw [← zpow_add]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m✝ n✝ : ℤ
a b : α
ha : 1 ≤ a
m n : ℤ
h : m ≤ n
⊢ a ^ (m + (n - m)) = a ^ n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m n : ℤ
a✝ b✝ : α
hn : 0 < n
a b : α
hab : a < b
⊢ (fun x => x ^ n) a < (fun x => x ^ n) b
[PROOFSTEP]
rw [← one_lt_div', ← div_zpow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m n : ℤ
a✝ b✝ : α
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n
[PROOFSTEP]
exact one_lt_zpow' (one_lt_div'.2 hab) hn
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m n : ℤ
a✝ b✝ : α
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ (fun x => x ^ n) a ≤ (fun x => x ^ n) b
[PROOFSTEP]
rw [← one_le_div', ← div_zpow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedCommGroup α
m n : ℤ
a✝ b✝ : α
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n
[PROOFSTEP]
exact one_le_zpow (one_le_div'.2 hab) hn
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a b : α
hn : n ≠ 0
⊢ Function.Injective fun x => x ^ n
[PROOFSTEP]
rcases hn.symm.lt_or_lt with (h | h)
[GOAL]
case inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a b : α
hn : n ≠ 0
h : 0 < n
⊢ Function.Injective fun x => x ^ n
[PROOFSTEP]
exact (zpow_strictMono_left α h).injective
[GOAL]
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a b : α
hn : n ≠ 0
h : n < 0
⊢ Function.Injective fun x => x ^ n
[PROOFSTEP]
refine' fun a b (hab : a ^ n = b ^ n) => (zpow_strictMono_left α (neg_pos.mpr h)).injective _
[GOAL]
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a✝ b✝ : α
hn : n ≠ 0
h : n < 0
a b : α
hab : a ^ n = b ^ n
⊢ a ^ (-n) = b ^ (-n)
[PROOFSTEP]
rw [zpow_neg, zpow_neg, hab]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℕ
a : α
⊢ |n • a| = n • |a|
[PROOFSTEP]
cases' le_total a 0 with hneg hpos
[GOAL]
case inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℕ
a : α
hneg : a ≤ 0
⊢ |n • a| = n • |a|
[PROOFSTEP]
rw [abs_of_nonpos hneg, ← abs_neg, ← neg_nsmul, abs_of_nonneg]
[GOAL]
case inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℕ
a : α
hneg : a ≤ 0
⊢ 0 ≤ n • -a
[PROOFSTEP]
exact nsmul_nonneg (neg_nonneg.mpr hneg) n
[GOAL]
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℕ
a : α
hpos : 0 ≤ a
⊢ |n • a| = n • |a|
[PROOFSTEP]
rw [abs_of_nonneg hpos, abs_of_nonneg]
[GOAL]
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℕ
a : α
hpos : 0 ≤ a
⊢ 0 ≤ n • a
[PROOFSTEP]
exact nsmul_nonneg hpos n
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℤ
a : α
⊢ |n • a| = |n| • |a|
[PROOFSTEP]
obtain n0 | n0 := le_total 0 n
[GOAL]
case inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℤ
a : α
n0 : 0 ≤ n
⊢ |n • a| = |n| • |a|
[PROOFSTEP]
obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0
[GOAL]
case inl.intro
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b a : α
n : ℕ
n0 : 0 ≤ ↑n
⊢ |↑n • a| = |↑n| • |a|
[PROOFSTEP]
simp only [abs_nsmul, coe_nat_zsmul, Nat.abs_cast]
[GOAL]
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℤ
a : α
n0 : n ≤ 0
⊢ |n • a| = |n| • |a|
[PROOFSTEP]
obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)
[GOAL]
case inr.intro
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ |n • a| = |n| • |a|
[PROOFSTEP]
rw [← abs_neg, ← neg_zsmul, ← abs_neg n, h, coe_nat_zsmul, Nat.abs_cast, coe_nat_zsmul]
[GOAL]
case inr.intro
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b : α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ |m • a| = m • |a|
[PROOFSTEP]
exact abs_nsmul m _
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
obtain a0 | a0 := le_or_lt 0 a
[GOAL]
case inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : 0 ≤ a
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
obtain b0 | b0 := le_or_lt 0 b
[GOAL]
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
obtain b0 | b0 := le_or_lt 0 b
[GOAL]
case inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : 0 ≤ a
b0 : 0 ≤ b
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
simp [a0, b0, abs_of_nonneg, add_nonneg a0 b0]
[GOAL]
case inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : 0 ≤ a
b0 : b < 0
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
exact (lt_irrefl (0 : α) <| a0.trans_lt <| hle.trans_lt b0).elim
[GOAL]
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
case inr.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : b < 0
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
any_goals simp [a0.le, b0.le, abs_of_nonpos, add_nonpos, add_comm]
[GOAL]
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
simp [a0.le, b0.le, abs_of_nonpos, add_nonpos, add_comm]
[GOAL]
case inr.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : b < 0
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
simp [a0.le, b0.le, abs_of_nonpos, add_nonpos, add_comm]
[GOAL]
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
have : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) := by
  simp [a0, a0.le, a0.not_le, b0, abs_of_neg, abs_of_nonneg]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
⊢ (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
[PROOFSTEP]
simp [a0, a0.le, a0.not_le, b0, abs_of_neg, abs_of_nonneg]
[GOAL]
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
refine' this.mp ⟨fun h => _, fun h => by simp only [le_antisymm h b0, abs_of_neg a0, add_zero]⟩
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : b ≤ 0
⊢ |a + b| = -a + b
[PROOFSTEP]
simp only [le_antisymm h b0, abs_of_neg a0, add_zero]
[GOAL]
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : |a + b| = -a + b
⊢ b ≤ 0
[PROOFSTEP]
obtain ab | ab := le_or_lt (a + b) 0
[GOAL]
case inr.inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : |a + b| = -a + b
ab : a + b ≤ 0
⊢ b ≤ 0
[PROOFSTEP]
refine' le_of_eq (eq_zero_of_neg_eq _)
[GOAL]
case inr.inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : |a + b| = -a + b
ab : a + b ≤ 0
⊢ -b = b
[PROOFSTEP]
rwa [abs_of_nonpos ab, neg_add_rev, add_comm, add_right_inj] at h
[GOAL]
case inr.inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : |a + b| = -a + b
ab : 0 < a + b
⊢ b ≤ 0
[PROOFSTEP]
refine' (lt_irrefl (0 : α) _).elim
[GOAL]
case inr.inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : |a + b| = -a + b
ab : 0 < a + b
⊢ 0 < 0
[PROOFSTEP]
rw [abs_of_pos ab, add_left_inj] at h
[GOAL]
case inr.inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : a = -a
ab : 0 < a + b
⊢ 0 < 0
[PROOFSTEP]
rwa [eq_zero_of_neg_eq h.symm] at a0
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ a b : α
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
obtain ab | ab := le_total a b
[GOAL]
case inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ a b : α
ab : a ≤ b
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
exact abs_add_eq_add_abs_le ab
[GOAL]
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ a b : α
ab : b ≤ a
⊢ |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
rw [add_comm a, add_comm (abs _), abs_add_eq_add_abs_le ab, and_comm, @and_comm (b ≤ 0)]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocSemiring R
a : R
n : ℕ
⊢ n • a = a * ↑n
[PROOFSTEP]
induction' n with n ih <;> [rw [zero_nsmul, Nat.cast_zero, mul_zero];
  rw [succ_nsmul', ih, Nat.cast_succ, mul_add, mul_one]]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocSemiring R
a : R
n : ℕ
⊢ n • a = a * ↑n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocSemiring R
a : R
⊢ Nat.zero • a = a * ↑Nat.zero
[PROOFSTEP]
rw [zero_nsmul, Nat.cast_zero, mul_zero]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocSemiring R
a : R
n : ℕ
ih : n • a = a * ↑n
⊢ Nat.succ n • a = a * ↑(Nat.succ n)
[PROOFSTEP]
rw [succ_nsmul', ih, Nat.cast_succ, mul_add, mul_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocSemiring R
n : ℕ
a : R
⊢ n • a = ↑n * a
[PROOFSTEP]
rw [nsmul_eq_mul', (n.cast_commute a).eq]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocSemiring R
n : ℕ
x y : R
⊢ n • x • y = x • n • y
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ Nat.zero • x • y = x • Nat.zero • y
[PROOFSTEP]
simp [zero_nsmul]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : n • x • y = x • n • y
⊢ Nat.succ n • x • y = x • Nat.succ n • y
[PROOFSTEP]
simp_rw [succ_nsmul, smul_eq_mul, mul_add, ← smul_eq_mul, ih]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocSemiring R
n : ℕ
x y : R
⊢ (n • x) • y = n • x • y
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ (Nat.zero • x) • y = Nat.zero • x • y
[PROOFSTEP]
simp [zero_nsmul]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
⊢ (Nat.succ n • x) • y = Nat.succ n • x • y
[PROOFSTEP]
simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Semiring R
n m : ℕ
⊢ ↑(n ^ m) = ↑n ^ m
[PROOFSTEP]
induction' m with m ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Semiring R
n : ℕ
⊢ ↑(n ^ zero) = ↑n ^ zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Semiring R
n m : ℕ
ih : ↑(n ^ m) = ↑n ^ m
⊢ ↑(n ^ succ m) = ↑n ^ succ m
[PROOFSTEP]
rw [_root_.pow_succ', _root_.pow_succ', Nat.cast_mul, ih]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
n m : ℕ
⊢ ↑(n ^ m) = ↑n ^ m
[PROOFSTEP]
induction' m with m _
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
n : ℕ
⊢ ↑(n ^ Nat.zero) = ↑n ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
n m : ℕ
n_ih✝ : ↑(n ^ m) = ↑n ^ m
⊢ ↑(n ^ Nat.succ m) = ↑n ^ Nat.succ m
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
n : ℤ
k : ℕ
⊢ natAbs (n ^ k) = natAbs n ^ k
[PROOFSTEP]
induction' k with k ih <;> [rfl; rw [pow_succ', Int.natAbs_mul, pow_succ', ih]]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
n : ℤ
k : ℕ
⊢ natAbs (n ^ k) = natAbs n ^ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
n : ℤ
⊢ natAbs (n ^ Nat.zero) = natAbs n ^ Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
n : ℤ
k : ℕ
ih : natAbs (n ^ k) = natAbs n ^ k
⊢ natAbs (n ^ Nat.succ k) = natAbs n ^ Nat.succ k
[PROOFSTEP]
rw [pow_succ', Int.natAbs_mul, pow_succ', ih]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocRing R
n r : R
⊢ bit0 n * r = 2 • (n * r)
[PROOFSTEP]
dsimp [bit0]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocRing R
n r : R
⊢ (n + n) * r = 2 • (n * r)
[PROOFSTEP]
rw [add_mul, ← one_add_one_eq_two, add_zsmul, one_zsmul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocRing R
n r : R
⊢ r * bit0 n = 2 • (r * n)
[PROOFSTEP]
dsimp [bit0]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocRing R
n r : R
⊢ r * (n + n) = 2 • (r * n)
[PROOFSTEP]
rw [mul_add, ← one_add_one_eq_two, add_zsmul, one_zsmul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocRing R
n r : R
⊢ bit1 n * r = 2 • (n * r) + r
[PROOFSTEP]
dsimp [bit1]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocRing R
n r : R
⊢ (bit0 n + 1) * r = 2 • (n * r) + r
[PROOFSTEP]
rw [add_mul, bit0_mul, one_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocRing R
n r : R
⊢ r * bit1 n = 2 • (r * n) + r
[PROOFSTEP]
dsimp [bit1]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocRing R
n r : R
⊢ r * (bit0 n + 1) = 2 • (r * n) + r
[PROOFSTEP]
rw [mul_add, mul_bit0, mul_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddCommGroupWithOne α
m : ℤ
⊢ ∀ (n : ℤ), ↑(0 * n) = 0 • ↑n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddCommGroupWithOne α
m k : ℤ
x✝ : 0 ≤ k
ih : ∀ (n : ℤ), ↑(k * n) = k • ↑n
n : ℤ
⊢ ↑((k + 1) * n) = (k + 1) • ↑n
[PROOFSTEP]
simp [add_mul, add_zsmul, ih]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddCommGroupWithOne α
m k : ℤ
x✝ : k ≤ 0
ih : ∀ (n : ℤ), ↑(k * n) = k • ↑n
n : ℤ
⊢ ↑((k - 1) * n) = (k - 1) • ↑n
[PROOFSTEP]
simp [sub_mul, sub_zsmul, ih, ← sub_eq_add_neg]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
a : R
n : ℕ
⊢ ↑n • a = ↑↑n * a
[PROOFSTEP]
rw [coe_nat_zsmul, nsmul_eq_mul, Int.cast_ofNat]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
a : R
n : ℕ
⊢ -[n+1] • a = ↑-[n+1] * a
[PROOFSTEP]
simp [Nat.cast_succ, neg_add_rev, Int.cast_negSucc, add_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
a : R
n : ℤ
⊢ n • a = a * ↑n
[PROOFSTEP]
rw [zsmul_eq_mul, (n.cast_commute a).eq]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ ↑n • x • y = x • ↑n • y
[PROOFSTEP]
simp_rw [coe_nat_zsmul, smul_comm]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ -[n+1] • x • y = x • -[n+1] • y
[PROOFSTEP]
simp_rw [negSucc_zsmul, smul_eq_mul, mul_neg, mul_smul_comm]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ (↑n • x) • y = ↑n • x • y
[PROOFSTEP]
simp_rw [coe_nat_zsmul, smul_assoc]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ (-[n+1] • x) • y = -[n+1] • x • y
[PROOFSTEP]
simp_rw [negSucc_zsmul, smul_eq_mul, neg_mul, smul_mul_assoc]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
a b : ℤ
⊢ a • b = a * b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
n : ℤ
⊢ n • 1 = n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
n : ℤ
m : ℕ
⊢ ↑(n ^ m) = ↑n ^ m
[PROOFSTEP]
induction' m with m ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
n : ℤ
⊢ ↑(n ^ Nat.zero) = ↑n ^ Nat.zero
[PROOFSTEP]
rw [pow_zero, pow_zero, Int.cast_one]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
n : ℤ
m : ℕ
ih : ↑(n ^ m) = ↑n ^ m
⊢ ↑(n ^ Nat.succ m) = ↑n ^ Nat.succ m
[PROOFSTEP]
rw [pow_succ, pow_succ, Int.cast_mul, ih]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ n = (-1) ^ (n % 2)
[PROOFSTEP]
rw [← Nat.mod_add_div n 2, pow_add, pow_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * ((-1) ^ 2) ^ (n / 2) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)
[PROOFSTEP]
simp [sq]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
⊢ 1 + ↑0 * a ≤ (1 + a) ^ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
⊢ 1 + ↑1 * a ≤ (1 + a) ^ 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
n : ℕ
this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a
⊢ 1 + ↑(n + 2) * a + (↑n * (a * a * (2 + a)) + a * a) = (1 + a) * (1 + a) * (1 + ↑n * a)
[PROOFSTEP]
{ simp only [Nat.cast_add, add_mul, mul_add, one_mul, mul_one, ← one_add_one_eq_two, Nat.cast_one, add_assoc,
    add_right_inj]
  simp only [← add_assoc, add_comm _ (↑n * a)]
  simp only [add_assoc, (n.cast_commute (_ : R)).left_comm]
  simp only [add_comm, add_left_comm]
}
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
n : ℕ
this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a
⊢ 1 + ↑(n + 2) * a + (↑n * (a * a * (2 + a)) + a * a) = (1 + a) * (1 + a) * (1 + ↑n * a)
[PROOFSTEP]
simp only [Nat.cast_add, add_mul, mul_add, one_mul, mul_one, ← one_add_one_eq_two, Nat.cast_one, add_assoc,
  add_right_inj]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
n : ℕ
this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a
⊢ 1 + (↑n * a + (a + (a + (↑n * (a * a) + (↑n * (a * a) + (↑n * (a * a * a) + a * a)))))) =
    1 + (a + (a + (a * a + (↑n * a + (a * (↑n * a) + (a * (↑n * a) + a * a * (↑n * a)))))))
[PROOFSTEP]
simp only [← add_assoc, add_comm _ (↑n * a)]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
n : ℕ
this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a
⊢ ↑n * a + 1 + a + a + ↑n * (a * a) + ↑n * (a * a) + ↑n * (a * a * a) + a * a =
    ↑n * a + 1 + a + a + a * a + a * (↑n * a) + a * (↑n * a) + a * a * (↑n * a)
[PROOFSTEP]
simp only [add_assoc, (n.cast_commute (_ : R)).left_comm]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
n : ℕ
this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a
⊢ ↑n * a + (1 + (a + (a + (a * (↑n * a) + (a * (↑n * a) + (a * a * (↑n * a) + a * a)))))) =
    ↑n * a + (1 + (a + (a + (a * a + (a * (↑n * a) + (a * (↑n * a) + a * a * (↑n * a)))))))
[PROOFSTEP]
simp only [add_comm, add_left_comm]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
n : ℕ
this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a
⊢ (1 + a) * (1 + a) * (1 + a) ^ n = (1 + a) ^ (n + 2)
[PROOFSTEP]
simp only [pow_succ, mul_assoc]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i : ℕ
⊢ a ^ (i + 0) ≤ a ^ i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i k : ℕ
⊢ a ^ (i + (k + 1)) ≤ a ^ i
[PROOFSTEP]
rw [← add_assoc, ← one_mul (a ^ i), pow_succ]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i k : ℕ
⊢ a * a ^ (i + k) ≤ 1 * a ^ i
[PROOFSTEP]
exact mul_le_mul ha (pow_le_pow_of_le_one_aux h ha _ _) (pow_nonneg h _) zero_le_one
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i j : ℕ
hij : i ≤ j
⊢ a ^ j ≤ a ^ i
[PROOFSTEP]
let ⟨k, hk⟩ := Nat.exists_eq_add_of_le hij
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i j : ℕ
hij : i ≤ j
k : ℕ
hk : j = i + k
⊢ a ^ j ≤ a ^ i
[PROOFSTEP]
rw [hk]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : OrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i j : ℕ
hij : i ≤ j
k : ℕ
hk : j = i + k
⊢ a ^ (i + k) ≤ a ^ i
[PROOFSTEP]
exact pow_le_pow_of_le_one_aux h ha _ _
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
⊢ C = 0 ∨ 0 < C ∧ 0 ≤ r
[PROOFSTEP]
have : 0 ≤ C := by simpa only [pow_zero, mul_one] using h 0
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
⊢ 0 ≤ C
[PROOFSTEP]
simpa only [pow_zero, mul_one] using h 0
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
this : 0 ≤ C
⊢ C = 0 ∨ 0 < C ∧ 0 ≤ r
[PROOFSTEP]
refine' this.eq_or_lt.elim (fun h => Or.inl h.symm) fun hC => Or.inr ⟨hC, _⟩
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
this : 0 ≤ C
hC : 0 < C
⊢ 0 ≤ r
[PROOFSTEP]
refine' nonneg_of_mul_nonneg_right _ hC
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
this : 0 ≤ C
hC : 0 < C
⊢ 0 ≤ C * r
[PROOFSTEP]
simpa only [pow_one] using h 1
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ a ^ bit1 n ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simp only [le_iff_lt_or_eq, pow_bit1_neg_iff]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ a < 0 ∨ a ^ bit1 n = 0 ↔ a < 0 ∨ a = 0
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ a < 0 ∨ a ^ bit1 n = 0 → a < 0 ∨ a = 0
[PROOFSTEP]
rintro (hpos | hz)
[GOAL]
case refine'_1.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hpos : a < 0
⊢ a < 0 ∨ a = 0
[PROOFSTEP]
left
[GOAL]
case refine'_1.inl.h
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hpos : a < 0
⊢ a < 0
[PROOFSTEP]
exact hpos
[GOAL]
case refine'_1.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hz : a ^ bit1 n = 0
⊢ a < 0 ∨ a = 0
[PROOFSTEP]
right
[GOAL]
case refine'_1.inr.h
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hz : a ^ bit1 n = 0
⊢ a = 0
[PROOFSTEP]
exact (pow_eq_zero_iff'.1 hz).1
[GOAL]
case refine'_2
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ a < 0 ∨ a = 0 → a < 0 ∨ a ^ bit1 n = 0
[PROOFSTEP]
rintro (hneg | hz)
[GOAL]
case refine'_2.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hneg : a < 0
⊢ a < 0 ∨ a ^ bit1 n = 0
[PROOFSTEP]
left
[GOAL]
case refine'_2.inl.h
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hneg : a < 0
⊢ a < 0
[PROOFSTEP]
exact hneg
[GOAL]
case refine'_2.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hz : a = 0
⊢ a < 0 ∨ a ^ bit1 n = 0
[PROOFSTEP]
right
[GOAL]
case refine'_2.inr.h
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hz : a = 0
⊢ a ^ bit1 n = 0
[PROOFSTEP]
simp [hz, bit1]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n✝ n : ℕ
⊢ StrictMono fun a => a ^ bit1 n
[PROOFSTEP]
intro a b hab
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
[PROOFSTEP]
cases' le_total a 0 with ha ha
[GOAL]
case inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
[PROOFSTEP]
cases' le_or_lt b 0 with hb hb
[GOAL]
case inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
[PROOFSTEP]
rw [← neg_lt_neg_iff, ← neg_pow_bit1, ← neg_pow_bit1]
[GOAL]
case inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (-b) ^ bit1 n < (-a) ^ bit1 n
[PROOFSTEP]
exact pow_lt_pow_of_lt_left (neg_lt_neg hab) (neg_nonneg.2 hb) (bit1_pos (zero_le n))
[GOAL]
case inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : a ≤ 0
hb : 0 < b
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
[PROOFSTEP]
exact (pow_bit1_nonpos_iff.2 ha).trans_lt (pow_bit1_pos_iff.2 hb)
[GOAL]
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a✝ : R
n✝ n : ℕ
a b : R
hab : a < b
ha : 0 ≤ a
⊢ (fun a => a ^ bit1 n) a < (fun a => a ^ bit1 n) b
[PROOFSTEP]
exact pow_lt_pow_of_lt_left hab ha (bit1_pos (zero_le n))
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n✝ : ℕ
H : -1 ≤ a
n : ℕ
⊢ 1 + ↑n * (a - 1) ≤ a ^ n
[PROOFSTEP]
have : -2 ≤ a - 1 := by rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n✝ : ℕ
H : -1 ≤ a
n : ℕ
⊢ -2 ≤ a - 1
[PROOFSTEP]
rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H✝ : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedRing R
a : R
n✝ : ℕ
H : -1 ≤ a
n : ℕ
this : -2 ≤ a - 1
⊢ 1 + ↑n * (a - 1) ≤ a ^ n
[PROOFSTEP]
simpa only [add_sub_cancel'_right] using one_add_mul_le_pow this n
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
x : ℤ
⊢ ↑(natAbs x) ^ 2 = x ^ 2
[PROOFSTEP]
rw [sq, Int.natAbs_mul_self', sq]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
a : ℤ
⊢ ↑(natAbs a) ≤ a ^ 2
[PROOFSTEP]
rw [← Int.natAbs_sq a, sq]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
a : ℤ
⊢ ↑(natAbs a) ≤ ↑(natAbs a) * ↑(natAbs a)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
a : ℤ
⊢ natAbs a ≤ natAbs a * natAbs a
[PROOFSTEP]
apply Nat.le_mul_self
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
x : ℤ
h : 1 < natAbs x
⊢ Function.Injective ((fun x x_1 => x ^ x_1) x)
[PROOFSTEP]
suffices Function.Injective (natAbs ∘ ((· ^ ·) x : ℕ → ℤ)) by exact Function.Injective.of_comp this
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
x : ℤ
h : 1 < natAbs x
this : Function.Injective (natAbs ∘ (fun x x_1 => x ^ x_1) x)
⊢ Function.Injective ((fun x x_1 => x ^ x_1) x)
[PROOFSTEP]
exact Function.Injective.of_comp this
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
x : ℤ
h : 1 < natAbs x
⊢ Function.Injective (natAbs ∘ (fun x x_1 => x ^ x_1) x)
[PROOFSTEP]
convert Nat.pow_right_injective h using 2
[GOAL]
case h.e'_3.h
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
x : ℤ
h : 1 < natAbs x
x✝ : ℕ
⊢ (natAbs ∘ (fun x x_1 => x ^ x_1) x) x✝ = natAbs x ^ x✝
[PROOFSTEP]
rw [Function.comp_apply, natAbs_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ ↑f n = ↑f (↑Multiplicative.ofAdd 1) ^ ↑Multiplicative.toAdd n
[PROOFSTEP]
rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Monoid M
f g : Multiplicative ℕ →* M
h : ↑f (↑Multiplicative.ofAdd 1) = ↑g (↑Multiplicative.ofAdd 1)
n : Multiplicative ℕ
⊢ ↑f n = ↑g n
[PROOFSTEP]
rw [f.apply_mnat, g.apply_mnat, h]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group M
f : Multiplicative ℤ →* M
n : Multiplicative ℤ
⊢ ↑f n = ↑f (↑Multiplicative.ofAdd 1) ^ ↑Multiplicative.toAdd n
[PROOFSTEP]
rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoid M
f : ℕ →+ M
n : ℕ
⊢ ↑f n = n • ↑f 1
[PROOFSTEP]
rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddGroup M
f : ℤ →+ M
n : ℤ
⊢ ↑f n = n • ↑f 1
[PROOFSTEP]
rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : CommMonoid M
src✝ : M ≃ (Multiplicative ℕ →* M) := powersHom M
a b : M
n : Multiplicative ℕ
⊢ ↑(Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          (a * b))
      n =
    ↑(Equiv.toFun
            { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            a *
          Equiv.toFun
            { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            b)
      n
[PROOFSTEP]
simp [mul_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : CommGroup G
src✝ : G ≃ (Multiplicative ℤ →* G) := zpowersHom G
a b : G
n : Multiplicative ℤ
⊢ ↑(Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          (a * b))
      n =
    ↑(Equiv.toFun
            { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            a *
          Equiv.toFun
            { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            b)
      n
[PROOFSTEP]
simp [mul_zpow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddCommMonoid A
src✝ : A ≃ (ℕ →+ A) := multiplesHom A
a b : A
n : ℕ
⊢ ↑(Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          (a + b))
      n =
    ↑(Equiv.toFun
            { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            a +
          Equiv.toFun
            { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            b)
      n
[PROOFSTEP]
simp [nsmul_add]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddCommGroup A
src✝ : A ≃ (ℤ →+ A) := zmultiplesHom A
a b : A
n : ℤ
⊢ ↑(Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          (a + b))
      n =
    ↑(Equiv.toFun
            { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            a +
          Equiv.toFun
            { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            b)
      n
[PROOFSTEP]
simp [zsmul_add]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M
inst✝¹ : Group G
inst✝ : Ring R
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ ↑n) ↑(y ^ ↑n)
[PROOFSTEP]
simp only [zpow_ofNat, Units.val_pow_eq_pow_val, h, pow_right]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M
inst✝¹ : Group G
inst✝ : Ring R
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ -[n+1]) ↑(y ^ -[n+1])
[PROOFSTEP]
simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]


[GOAL]
α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ a = b
[PROOFSTEP]
rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc
[GOAL]
α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a = b
⊢ a = b
[PROOFSTEP]
exact hc
[GOAL]
α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a = b
⊢ IsConj a b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (↑(↑(Units.map f) c)) (↑f a) (↑f b)
[PROOFSTEP]
rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]
[GOAL]
α : Type u
β : Type v
inst✝ : CancelMonoid α
a : α
h : a = 1
⊢ IsConj 1 a
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
inst✝ : Group α
i : ℕ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
[PROOFSTEP]
induction' i with i hi
[GOAL]
case zero
α : Type u
β : Type v
inst✝ : Group α
a b : α
⊢ (a * b * a⁻¹) ^ Nat.zero = a * b ^ Nat.zero * a⁻¹
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
β : Type v
inst✝ : Group α
a b : α
i : ℕ
hi : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
⊢ (a * b * a⁻¹) ^ Nat.succ i = a * b ^ Nat.succ i * a⁻¹
[PROOFSTEP]
simp [pow_succ, hi]
[GOAL]
α : Type u
β : Type v
inst✝ : Group α
i : ℤ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
[PROOFSTEP]
induction' i
[GOAL]
case ofNat
α : Type u
β : Type v
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹
[PROOFSTEP]
change (a * b * a⁻¹) ^ (_ : ℤ) = a * b ^ (_ : ℤ) * a⁻¹
[GOAL]
case ofNat
α : Type u
β : Type v
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹
[PROOFSTEP]
simp [zpow_ofNat]
[GOAL]
case negSucc
α : Type u
β : Type v
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹
[PROOFSTEP]
simp [zpow_negSucc, conj_pow]
[GOAL]
case negSucc
α : Type u
β : Type v
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ a * ((b ^ (a✝ + 1))⁻¹ * a⁻¹) = a * (b ^ (a✝ + 1))⁻¹ * a⁻¹
[PROOFSTEP]
rw [mul_assoc]
  -- Porting note: Added `change`, `zpow_ofNat`, and `rw`.
[GOAL]
α : Type u
β : Type v
inst✝ : GroupWithZero α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ ↑c ≠ 0 ∧ ↑c * a * (↑c)⁻¹ = b
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val, Units.mul_inv_eq_iff_eq_mul]
[GOAL]
α : Type u
β : Type v
inst✝ : GroupWithZero α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ ↑c ≠ 0 ∧ ↑c * a = b * ↑c
[PROOFSTEP]
exact ⟨c.ne_zero, hc⟩
[GOAL]
α : Type u
β : Type v
inst✝ : GroupWithZero α
a b : α
x✝ : ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b
c : α
c0 : c ≠ 0
hc : c * a * c⁻¹ = b
⊢ SemiconjBy (↑(Units.mk0 c c0)) a b
[PROOFSTEP]
rw [SemiconjBy, ← Units.mul_inv_eq_iff_eq_mul, Units.val_inv_eq_inv_val, Units.val_mk0]
[GOAL]
α : Type u
β : Type v
inst✝ : GroupWithZero α
a b : α
x✝ : ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b
c : α
c0 : c ≠ 0
hc : c * a * c⁻¹ = b
⊢ c * a * c⁻¹ = b
[PROOFSTEP]
exact hc
[GOAL]
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
⊢ Function.Surjective (map f)
[PROOFSTEP]
intro b
[GOAL]
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
b : ConjClasses β
⊢ ∃ a, map f a = b
[PROOFSTEP]
obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
b : β
⊢ ∃ a, map f a = ConjClasses.mk b
[PROOFSTEP]
obtain ⟨a, rfl⟩ := hf b
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
a : α
⊢ ∃ a_1, map f a_1 = ConjClasses.mk (↑f a)
[PROOFSTEP]
exact ⟨ConjClasses.mk a, rfl⟩
[GOAL]
α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ Function.RightInverse (Quotient.lift id (_ : ∀ (a b : α), IsConj a b → a = b)) ConjClasses.mk
[PROOFSTEP]
rw [Function.RightInverse, Function.LeftInverse, forall_isConj]
[GOAL]
α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ ∀ (a : α),
    ConjClasses.mk (Quotient.lift id (_ : ∀ (a b : α), IsConj a b → a = b) (ConjClasses.mk a)) = ConjClasses.mk a
[PROOFSTEP]
intro x
[GOAL]
α : Type u
β : Type v
inst✝ : CommMonoid α
x : α
⊢ ConjClasses.mk (Quotient.lift id (_ : ∀ (a b : α), IsConj a b → a = b) (ConjClasses.mk x)) = ConjClasses.mk x
[PROOFSTEP]
rw [← quotient_mk_eq_mk, ← quotient_mk_eq_mk, Quotient.lift_mk, id.def]
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
⊢ IsConj a b
[PROOFSTEP]
have ha := @mem_conjugatesOf_self _ _ b
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf b
⊢ IsConj a b
[PROOFSTEP]
rwa [← h] at ha
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a : α
b : ConjClasses α
⊢ a ∈ carrier b ↔ ConjClasses.mk a = b
[PROOFSTEP]
revert b
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ carrier b ↔ ConjClasses.mk a = b
[PROOFSTEP]
rw [forall_isConj]
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a : α
⊢ ∀ (a_1 : α), a ∈ carrier (ConjClasses.mk a_1) ↔ ConjClasses.mk a = ConjClasses.mk a_1
[PROOFSTEP]
intro b
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
⊢ a ∈ carrier (ConjClasses.mk b) ↔ ConjClasses.mk a = ConjClasses.mk b
[PROOFSTEP]
rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
⊢ a ∈ conjugatesOf b ↔ IsConj b a
[PROOFSTEP]
rfl


[GOAL]
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : ↑{ val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = ↑{ val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }
[PROOFSTEP]
simp only at e
[GOAL]
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : v = v'
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }
[PROOFSTEP]
subst v'
[GOAL]
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v, inv := i₂, val_inv := vi₂, inv_val := iv₂ }
[PROOFSTEP]
congr
[GOAL]
case e_inv
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ i₁ = i₂
[PROOFSTEP]
simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁
[GOAL]
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * ↑u₂ * (u₂.inv * u₁.inv) = 1
[PROOFSTEP]
rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * u₁.inv * (↑u₁ * ↑u₂) = 1
[PROOFSTEP]
rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u a : αˣ
⊢ ↑a = 1 ↔ a = 1
[PROOFSTEP]
rw [← Units.val_one, eq_iff]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : ↑u = a
⊢ ↑u⁻¹ * a = 1
[PROOFSTEP]
rw [← h, u.inv_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : ↑u = a
⊢ a * ↑u⁻¹ = 1
[PROOFSTEP]
rw [← h, u.mul_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u a : αˣ
b : α
⊢ ↑a * (↑a⁻¹ * b) = b
[PROOFSTEP]
rw [← mul_assoc, mul_inv, one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u a : αˣ
b : α
⊢ ↑a⁻¹ * (↑a * b) = b
[PROOFSTEP]
rw [← mul_assoc, inv_mul, one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u : αˣ
a : α
b : αˣ
⊢ a * ↑b * ↑b⁻¹ = a
[PROOFSTEP]
rw [mul_assoc, mul_inv, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u : αˣ
a : α
b : αˣ
⊢ a * ↑b⁻¹ * ↑b = a
[PROOFSTEP]
rw [mul_assoc, inv_mul, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c✝ u a : αˣ
b c : α
h : ↑a * b = ↑a * c
⊢ b = c
[PROOFSTEP]
simpa only [inv_mul_cancel_left] using congr_arg (fun x : α => ↑(a⁻¹ : αˣ) * x) h
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c✝ u a : αˣ
b c : α
h : b * ↑a = c * ↑a
⊢ b = c
[PROOFSTEP]
simpa only [mul_inv_cancel_right] using congr_arg (fun x : α => x * ↑(a⁻¹ : αˣ)) h
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u : αˣ
a b : α
h : a = b * ↑c⁻¹
⊢ a * ↑c = b
[PROOFSTEP]
rw [h, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u : αˣ
a b : α
h : a * ↑c = b
⊢ a = b * ↑c⁻¹
[PROOFSTEP]
rw [← h, mul_inv_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : a = ↑b⁻¹ * c
⊢ ↑b * a = c
[PROOFSTEP]
rw [h, mul_inv_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : ↑b * a = c
⊢ a = ↑b⁻¹ * c
[PROOFSTEP]
rw [← h, inv_mul_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a b✝ c✝ u : αˣ
b c : α
h : ↑a⁻¹ * b = c
⊢ b = ↑a * c
[PROOFSTEP]
rw [← h, mul_inv_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a b✝ c✝ u : αˣ
b c : α
h : b = ↑a * c
⊢ ↑a⁻¹ * b = c
[PROOFSTEP]
rw [h, inv_mul_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : a * ↑b⁻¹ = c
⊢ a = c * ↑b
[PROOFSTEP]
rw [← h, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : a = c * ↑b
⊢ a * ↑b⁻¹ = c
[PROOFSTEP]
rw [h, mul_inv_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : a * ↑u = 1
⊢ ↑u⁻¹ = 1 * ↑u⁻¹
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : a * ↑u = 1
⊢ 1 * ↑u⁻¹ = a
[PROOFSTEP]
rw [← h, mul_inv_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ = ↑u⁻¹ * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ * 1 = a
[PROOFSTEP]
rw [← h, inv_mul_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
⊢ a * ↑u = 1 ↔ a = ↑u⁻¹
[PROOFSTEP]
rw [← mul_inv_eq_one, inv_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
⊢ ↑u * a = 1 ↔ ↑u⁻¹ = a
[PROOFSTEP]
rw [← inv_mul_eq_one, inv_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c u u₁ u₂ : αˣ
h : ↑u₁ = ↑u₂
⊢ ↑u₁ * ↑u₂⁻¹ = 1
[PROOFSTEP]
rw [h, u₂.mul_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c a : α
u : αˣ
⊢ a * (↑u⁻¹ * ↑u) = a
[PROOFSTEP]
rw [Units.inv_mul, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c a : α
u : αˣ
⊢ a * (↑u * ↑u⁻¹) = a
[PROOFSTEP]
rw [Units.mul_inv, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c x : α
u₁ u₂ : αˣ
⊢ x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)
[PROOFSTEP]
simp only [divp, mul_inv_rev, Units.val_mul, mul_assoc]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c x : α
u : αˣ
y : α
⊢ x /ₚ u * ↑u = y * ↑u ↔ y * ↑u = x
[PROOFSTEP]
rw [divp_mul_cancel]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c x : α
u : αˣ
y : α
⊢ x = y * ↑u ↔ y * ↑u = x
[PROOFSTEP]
exact ⟨Eq.symm, Eq.symm⟩
[GOAL]
α : Type u
inst✝ : Monoid α
a b c x : α
u : αˣ
y : α
⊢ x = y /ₚ u ↔ x * ↑u = y
[PROOFSTEP]
rw [eq_comm, divp_eq_iff_mul_eq]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c a : α
u : αˣ
⊢ a /ₚ u * ↑u = 1 * ↑u ↔ a = ↑u
[PROOFSTEP]
rw [divp_mul_cancel, one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c : α
u : αˣ
⊢ ↑u⁻¹ = 1 /ₚ u
[PROOFSTEP]
rw [one_divp]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c : α
u : αˣ
⊢ ↑(1 / u) = 1 /ₚ u
[PROOFSTEP]
rw [one_div, one_divp]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c : α
u₁ u₂ : αˣ
⊢ ↑(u₁ / u₂) = ↑u₁ /ₚ u₂
[PROOFSTEP]
rw [divp, division_def, Units.val_mul]
[GOAL]
α : Type u
inst✝ : CommMonoid α
x y : α
u : αˣ
⊢ x /ₚ u * y = x * y /ₚ u
[PROOFSTEP]
rw [divp, divp, mul_right_comm]
[GOAL]
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux
[PROOFSTEP]
rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]
[GOAL]
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
[PROOFSTEP]
rw [divp_mul_eq_mul_divp, divp_assoc', divp_divp_eq_divp_mul]
[GOAL]
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1
[PROOFSTEP]
exact mul_one _
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, a * b = 1
[PROOFSTEP]
rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩
[GOAL]
case intro.mk
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a b : M
hab : a * b = 1
inv_val✝ : b * a = 1
⊢ ∃ b_1, ↑{ val := a, inv := b, val_inv := hab, inv_val := inv_val✝ } * b_1 = 1
[PROOFSTEP]
exact ⟨b, hab⟩
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, b * a = 1
[PROOFSTEP]
rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩
[GOAL]
case intro.mk
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a b : M
val_inv✝ : a * b = 1
hba : b * a = 1
⊢ ∃ b_1, b_1 * ↑{ val := a, inv := b, val_inv := val_inv✝, inv_val := hba } = 1
[PROOFSTEP]
exact ⟨b, hba⟩
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : CommMonoid M
a : M
⊢ IsUnit a ↔ ∃ b, b * a = 1
[PROOFSTEP]
simp [isUnit_iff_exists_inv, mul_comm]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
x y : M
⊢ IsUnit x → IsUnit y → IsUnit (x * y)
[PROOFSTEP]
rintro ⟨x, rfl⟩ ⟨y, rfl⟩
[GOAL]
case intro.intro
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
x y : Mˣ
⊢ IsUnit (↑x * ↑y)
[PROOFSTEP]
exact ⟨x * y, Units.val_mul _ _⟩
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit a
[PROOFSTEP]
have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit (a * ↑u * ↑u⁻¹)
[PROOFSTEP]
exists v * u⁻¹
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ ↑(v * u⁻¹) = a * ↑u * ↑u⁻¹
[PROOFSTEP]
rw [← hv, Units.val_mul]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
this : IsUnit (a * ↑u * ↑u⁻¹)
⊢ IsUnit a
[PROOFSTEP]
rwa [mul_assoc, Units.mul_inv, mul_one] at this
[GOAL]
α : Type u
M✝ : Type u_1
N : Type u_2
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ IsUnit a
[PROOFSTEP]
have : IsUnit (↑u⁻¹ * (↑u * a)) := by exists u⁻¹ * v; rw [← hv, Units.val_mul]
[GOAL]
α : Type u
M✝ : Type u_1
N : Type u_2
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ IsUnit (↑u⁻¹ * (↑u * a))
[PROOFSTEP]
exists u⁻¹ * v
[GOAL]
α : Type u
M✝ : Type u_1
N : Type u_2
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ ↑(u⁻¹ * v) = ↑u⁻¹ * (↑u * a)
[PROOFSTEP]
rw [← hv, Units.val_mul]
[GOAL]
α : Type u
M✝ : Type u_1
N : Type u_2
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
this : IsUnit (↑u⁻¹ * (↑u * a))
⊢ IsUnit a
[PROOFSTEP]
rwa [← mul_assoc, Units.inv_mul, one_mul] at this
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : CommMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
⊢ x * (y * z) = 1
[PROOFSTEP]
rwa [← mul_assoc]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : CommMonoid M
x y : M
hu : IsUnit (x * y)
⊢ IsUnit (y * x)
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a b c : M
h : IsUnit a
⊢ a * ↑(IsUnit.unit h)⁻¹ = 1
[PROOFSTEP]
rw [← h.unit.mul_inv]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a b c : M
h : IsUnit a
⊢ a * ↑(IsUnit.unit h)⁻¹ = ↑(IsUnit.unit h) * ↑(IsUnit.unit h)⁻¹
[PROOFSTEP]
congr
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : DivisionMonoid M
a : M
⊢ IsUnit a → a⁻¹ * a = 1
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case intro
α : Type u
M : Type u_1
N : Type u_2
inst✝ : DivisionMonoid M
u : Mˣ
⊢ (↑u)⁻¹ * ↑u = 1
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val, Units.inv_mul]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : DivisionMonoid M
a : M
⊢ IsUnit a → a * a⁻¹ = 1
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case intro
α : Type u
M : Type u_1
N : Type u_2
inst✝ : DivisionMonoid M
u : Mˣ
⊢ ↑u * (↑u)⁻¹ = 1
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val, Units.mul_inv]
[GOAL]
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a⁻¹ * a = 1
[PROOFSTEP]
change ↑(h a).unit⁻¹ * a = 1
[GOAL]
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑(IsUnit.unit (_ : IsUnit a))⁻¹ * a = 1
[PROOFSTEP]
rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]
[GOAL]
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a⁻¹ * a = 1
[PROOFSTEP]
change ↑(h a).unit⁻¹ * a = 1
[GOAL]
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑(IsUnit.unit (_ : IsUnit a))⁻¹ * a = 1
[PROOFSTEP]
rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]


[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
x y : Decomposition ℳ
⊢ x = y
[PROOFSTEP]
cases' x with x xl xr
[GOAL]
case mk
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
y : Decomposition ℳ
x : M → ⨁ (i : ι), { x // x ∈ ℳ i }
xl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
xr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
⊢ { decompose' := x, left_inv := xl, right_inv := xr } = y
[PROOFSTEP]
cases' y with y yl yr
[GOAL]
case mk.mk
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
x : M → ⨁ (i : ι), { x // x ∈ ℳ i }
xl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
xr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
y : M → ⨁ (i : ι), { x // x ∈ ℳ i }
yl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) y
yr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) y
⊢ { decompose' := x, left_inv := xl, right_inv := xr } = { decompose' := y, left_inv := yl, right_inv := yr }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_decompose'
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
x : M → ⨁ (i : ι), { x // x ∈ ℳ i }
xl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
xr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
y : M → ⨁ (i : ι), { x // x ∈ ℳ i }
yl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) y
yr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) y
⊢ x = y
[PROOFSTEP]
exact Function.LeftInverse.eq_rightInverse xr yl
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
p : M → Prop
h_zero : p 0
h_homogeneous : ∀ {i : ι} (m : { x // x ∈ ℳ i }), p ↑m
h_add : ∀ (m m' : M), p m → p m' → p (m + m')
⊢ ∀ (m : M), p m
[PROOFSTEP]
let ℳ' : ι → AddSubmonoid M := fun i ↦
  (⟨⟨ℳ i, fun x y ↦ AddMemClass.add_mem x y⟩, (ZeroMemClass.zero_mem _)⟩ : AddSubmonoid M)
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
p : M → Prop
h_zero : p 0
h_homogeneous : ∀ {i : ι} (m : { x // x ∈ ℳ i }), p ↑m
h_add : ∀ (m m' : M), p m → p m' → p (m + m')
ℳ' : ι → AddSubmonoid M :=
  fun i =>
    { toAddSubsemigroup := { carrier := ↑(ℳ i), add_mem' := (_ : ∀ {a b : M}, a ∈ ↑(ℳ i) → b ∈ ↑(ℳ i) → a + b ∈ ℳ i) },
      zero_mem' := (_ : 0 ∈ ℳ i) }
⊢ ∀ (m : M), p m
[PROOFSTEP]
haveI t : DirectSum.Decomposition ℳ' :=
  { decompose' := DirectSum.decompose ℳ
    left_inv := fun _ ↦ (decompose ℳ).left_inv _
    right_inv := fun _ ↦ (decompose ℳ).right_inv _ }
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
p : M → Prop
h_zero : p 0
h_homogeneous : ∀ {i : ι} (m : { x // x ∈ ℳ i }), p ↑m
h_add : ∀ (m m' : M), p m → p m' → p (m + m')
ℳ' : ι → AddSubmonoid M :=
  fun i =>
    { toAddSubsemigroup := { carrier := ↑(ℳ i), add_mem' := (_ : ∀ {a b : M}, a ∈ ↑(ℳ i) → b ∈ ↑(ℳ i) → a + b ∈ ℳ i) },
      zero_mem' := (_ : 0 ∈ ℳ i) }
t : Decomposition ℳ'
⊢ ∀ (m : M), p m
[PROOFSTEP]
have mem : ∀ m, m ∈ iSup ℳ' := fun _m ↦
  (DirectSum.IsInternal.addSubmonoid_iSup_eq_top ℳ' (Decomposition.isInternal ℳ')).symm ▸ trivial
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
p : M → Prop
h_zero : p 0
h_homogeneous : ∀ {i : ι} (m : { x // x ∈ ℳ i }), p ↑m
h_add : ∀ (m m' : M), p m → p m' → p (m + m')
ℳ' : ι → AddSubmonoid M :=
  fun i =>
    { toAddSubsemigroup := { carrier := ↑(ℳ i), add_mem' := (_ : ∀ {a b : M}, a ∈ ↑(ℳ i) → b ∈ ↑(ℳ i) → a + b ∈ ℳ i) },
      zero_mem' := (_ : 0 ∈ ℳ i) }
t : Decomposition ℳ'
mem : ∀ (m : M), m ∈ iSup ℳ'
⊢ ∀ (m : M), p m
[PROOFSTEP]
exact fun m ↦ @AddSubmonoid.iSup_induction _ _ _ ℳ' _ _ (mem m) (fun i m h ↦ h_homogeneous ⟨m, h⟩) h_zero h_add
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
i : ι
x : { x // x ∈ ℳ i }
⊢ ↑(decompose ℳ) ↑x = ↑(of (fun i => { x // x ∈ ℳ i }) i) x
[PROOFSTEP]
rw [← decompose_symm_of _, Equiv.apply_symm_apply]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i : ι
hx : x ∈ ℳ i
⊢ ↑(↑(↑(decompose ℳ) x) i) = x
[PROOFSTEP]
rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hx : x ∈ ℳ i
hij : i ≠ j
⊢ ↑(↑(↑(decompose ℳ) x) j) = 0
[PROOFSTEP]
rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ _ hij, ZeroMemClass.coe_zero]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in DFinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) = r
[PROOFSTEP]
conv_rhs => rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (fun i ↦ ℳ i) (decompose ℳ r)]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
| r
[PROOFSTEP]
rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (fun i ↦ ℳ i) (decompose ℳ r)]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
| r
[PROOFSTEP]
rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (fun i ↦ ℳ i) (decompose ℳ r)]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
| r
[PROOFSTEP]
rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (fun i ↦ ℳ i) (decompose ℳ r)]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in DFinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) =
    ↑(decompose ℳ).symm
      (∑ i in DFinsupp.support (↑(decompose ℳ) r), ↑(of (fun i => { x // x ∈ ℳ i }) i) (↑(↑(decompose ℳ) r) i))
[PROOFSTEP]
rw [decompose_symm_sum]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in DFinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) =
    ∑ i in DFinsupp.support (↑(decompose ℳ) r),
      ↑(decompose ℳ).symm (↑(of (fun i => { x // x ∈ ℳ i }) i) (↑(↑(decompose ℳ) r) i))
[PROOFSTEP]
simp_rw [decompose_symm_of]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : SetLike σ M
inst✝ : AddSubgroupClass σ M
ℳ : ι → σ
⊢ AddCommGroup (⨁ (i : ι), { x // x ∈ ℳ i })
[PROOFSTEP]
infer_instance


[GOAL]
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x') (y * y')
[PROOFSTEP]
unfold SemiconjBy
[GOAL]
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * (x * x') = y * y' * a
[PROOFSTEP]
rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]
[GOAL]
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ SemiconjBy (a * b) x z
[PROOFSTEP]
unfold SemiconjBy
[GOAL]
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ a * b * x = z * (a * b)
[PROOFSTEP]
rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]
[GOAL]
M : Type u_1
inst✝ : MulOneClass M
a : M
⊢ SemiconjBy a 1 1
[PROOFSTEP]
rw [SemiconjBy, mul_one, one_mul]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ a * ↑x⁻¹ = ↑y⁻¹ * (↑y * a) * ↑x⁻¹
[PROOFSTEP]
rw [Units.inv_mul_cancel_left]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ ↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a
[PROOFSTEP]
rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * y = ↑a⁻¹ * (y * ↑a * ↑a⁻¹)
[PROOFSTEP]
rw [Units.mul_inv_cancel_right]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹
[PROOFSTEP]
rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ n) (y ^ n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero)
[PROOFSTEP]
rw [pow_zero, pow_zero]
[GOAL]
case zero
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1
[PROOFSTEP]
exact SemiconjBy.one_right _
[GOAL]
case succ
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
case succ
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x * x ^ n) (y * y ^ n)
[PROOFSTEP]
exact h.mul_right ih
[GOAL]
G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ (a⁻¹ * x⁻¹)⁻¹ = (y⁻¹ * a⁻¹)⁻¹ ↔ SemiconjBy a y x
[PROOFSTEP]
rw [mul_inv_rev, mul_inv_rev, inv_inv, inv_inv, inv_inv, eq_comm, SemiconjBy]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ x✝ y a x : G
⊢ SemiconjBy a x (a * x * a⁻¹)
[PROOFSTEP]
unfold SemiconjBy
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ x✝ y a x : G
⊢ a * x = a * x * a⁻¹ * a
[PROOFSTEP]
rw [mul_assoc, inv_mul_self, mul_one]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ SemiconjBy a x y
[PROOFSTEP]
rw [h, SemiconjBy, mul_comm]
[GOAL]
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)
[PROOFSTEP]
unfold SemiconjBy
[GOAL]
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ ↑u * x = ↑u * x * ↑u⁻¹ * ↑u
[PROOFSTEP]
rw [Units.inv_mul_cancel_right]


[GOAL]
α : Type u_1
inst✝ : Group α
x✝ : (WithZero α)ˣ
⊢ ↑((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) ((fun a => unzero (_ : ↑a ≠ 0)) x✝)) = ↑x✝
[PROOFSTEP]
simp only [coe_unzero, Units.mk0_val]
[GOAL]
α : Type u_1
inst✝ : Group α
x✝¹ x✝ : (WithZero α)ˣ
⊢ ↑(Equiv.toFun
        { toFun := fun a => unzero (_ : ↑a ≠ 0), invFun := fun a => Units.mk0 ↑a (_ : ↑a ≠ 0),
          left_inv :=
            (_ : ∀ (x : (WithZero α)ˣ), (fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) ((fun a => unzero (_ : ↑a ≠ 0)) x) = x),
          right_inv :=
            (_ :
              ∀ (x : α),
                (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x) =
                  (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x)) }
        (x✝¹ * x✝)) =
    ↑(Equiv.toFun
          { toFun := fun a => unzero (_ : ↑a ≠ 0), invFun := fun a => Units.mk0 ↑a (_ : ↑a ≠ 0),
            left_inv :=
              (_ : ∀ (x : (WithZero α)ˣ), (fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) ((fun a => unzero (_ : ↑a ≠ 0)) x) = x),
            right_inv :=
              (_ :
                ∀ (x : α),
                  (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x) =
                    (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x)) }
          x✝¹ *
        Equiv.toFun
          { toFun := fun a => unzero (_ : ↑a ≠ 0), invFun := fun a => Units.mk0 ↑a (_ : ↑a ≠ 0),
            left_inv :=
              (_ : ∀ (x : (WithZero α)ˣ), (fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) ((fun a => unzero (_ : ↑a ≠ 0)) x) = x),
            right_inv :=
              (_ :
                ∀ (x : α),
                  (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x) =
                    (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x)) }
          x✝)
[PROOFSTEP]
simp only [Units.val_mul, coe_unzero, coe_mul]