[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]
