[GOAL]
n : ℕ
x : ℤ
⊢ (↑n + 1) * x = x + ↑n * x
[PROOFSTEP]
rw [Int.add_mul, Int.add_comm, Int.one_mul]
[GOAL]
x✝¹ : ℕ
x✝ : ℤ
⊢ (fun n x => x ^ n) (x✝¹ + 1) x✝ = x✝ * (fun n x => x ^ n) x✝¹ x✝
[PROOFSTEP]
rw [Int.mul_comm]
[GOAL]
x✝¹ : ℕ
x✝ : ℤ
⊢ (fun n x => x ^ n) (x✝¹ + 1) x✝ = (fun n x => x ^ n) x✝¹ x✝ * x✝
[PROOFSTEP]
rfl
[GOAL]
m : ℕ
n : ℤ
⊢ (fun x x_1 => x * x_1) (ofNat (succ m)) n = n + (fun x x_1 => x * x_1) (ofNat m) n
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_succ, Int.add_mul, Int.add_comm, Int.one_mul]
[GOAL]
m : ℕ
n : ℤ
⊢ (fun x x_1 => x * x_1) -[m+1] n = -(fun x x_1 => x * x_1) (↑(succ m)) n
[PROOFSTEP]
simp only [negSucc_coe, ofNat_succ, Int.neg_mul]
[GOAL]
⊢ AddCommMonoid ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddMonoid ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Monoid ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommMonoid ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommSemigroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Semigroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddCommGroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddGroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddCommSemigroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddSemigroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommSemiring ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Semiring ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Ring ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Distrib ℤ
[PROOFSTEP]
infer_instance
[GOAL]
a : ℤ
⊢ succ (-succ a) = -a
[PROOFSTEP]
rw [neg_succ, succ_pred]
[GOAL]
a : ℤ
⊢ -pred a = succ (-a)
[PROOFSTEP]
rw [neg_eq_iff_eq_neg.mp (neg_succ (-a)), neg_neg]
[GOAL]
a : ℤ
⊢ pred (-pred a) = -a
[PROOFSTEP]
rw [neg_pred, pred_succ]
[GOAL]
n : ℕ
h : 0 < n
⊢ ↑(n - 1) = ↑n - 1
[PROOFSTEP]
cases n
[GOAL]
case zero
h : 0 < zero
⊢ ↑(zero - 1) = ↑zero - 1
case succ n✝ : ℕ h : 0 < Nat.succ n✝ ⊢ ↑(Nat.succ n✝ - 1) = ↑(Nat.succ n✝) - 1
[PROOFSTEP]
cases h
[GOAL]
case succ
n✝ : ℕ
h : 0 < Nat.succ n✝
⊢ ↑(Nat.succ n✝ - 1) = ↑(Nat.succ n✝) - 1
[PROOFSTEP]
simp
[GOAL]
p : ℤ → Prop
i : ℤ
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p i
[PROOFSTEP]
induction i with
| ofNat i =>
  induction i with
  | zero => exact hz
  | succ i ih => exact hp _ ih
| negSucc i =>
  suffices ∀ n : ℕ, p (-n) from this (i + 1)
  intro n;
  induction n with
  | zero => simp [hz, Nat.cast_zero]
  | succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
p : ℤ → Prop
i : ℤ
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p i
[PROOFSTEP]
induction i with
| ofNat i =>
  induction i with
  | zero => exact hz
  | succ i ih => exact hp _ ih
| negSucc i =>
  suffices ∀ n : ℕ, p (-n) from this (i + 1)
  intro n;
  induction n with
  | zero => simp [hz, Nat.cast_zero]
  | succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case ofNat
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (ofNat i)
[PROOFSTEP]

| ofNat i =>
  induction i with
  | zero => exact hz
  | succ i ih => exact hp _ ih
[GOAL]
case ofNat
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (ofNat i)
[PROOFSTEP]
induction i with
| zero => exact hz
| succ i ih => exact hp _ ih
[GOAL]
case ofNat
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (ofNat i)
[PROOFSTEP]
induction i with
| zero => exact hz
| succ i ih => exact hp _ ih
[GOAL]
case ofNat.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p (ofNat zero)
[PROOFSTEP]

| zero => exact hz
[GOAL]
case ofNat.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p (ofNat zero)
[PROOFSTEP]
exact hz
[GOAL]
case ofNat.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
ih : p (ofNat i)
⊢ p (ofNat (Nat.succ i))
[PROOFSTEP]

| succ i ih => exact hp _ ih
[GOAL]
case ofNat.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
ih : p (ofNat i)
⊢ p (ofNat (Nat.succ i))
[PROOFSTEP]
exact hp _ ih
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p -[i+1]
[PROOFSTEP]

| negSucc i =>
  suffices ∀ n : ℕ, p (-n) from this (i + 1)
  intro n;
  induction n with
  | zero => simp [hz, Nat.cast_zero]
  | succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p -[i+1]
[PROOFSTEP]
suffices ∀ n : ℕ, p (-n) from this (i + 1)
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ ∀ (n : ℕ), p (-↑n)
[PROOFSTEP]
intro n
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
⊢ p (-↑n)
[PROOFSTEP]
induction n with
| zero => simp [hz, Nat.cast_zero]
| succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
⊢ p (-↑n)
[PROOFSTEP]
induction n with
| zero => simp [hz, Nat.cast_zero]
| succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case negSucc.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (-↑zero)
[PROOFSTEP]

| zero => simp [hz, Nat.cast_zero]
[GOAL]
case negSucc.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (-↑zero)
[PROOFSTEP]
simp [hz, Nat.cast_zero]
[GOAL]
case negSucc.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
ih : p (-↑n)
⊢ p (-↑(Nat.succ n))
[PROOFSTEP]

| succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case negSucc.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
ih : p (-↑n)
⊢ p (-↑(Nat.succ n))
[PROOFSTEP]
convert hn _ ih using 1
[GOAL]
case h.e'_1
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
ih : p (-↑n)
⊢ -↑(Nat.succ n) = -↑n - 1
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -((- -[m+1] - 1) / ↑(Nat.succ n) + 1)
[PROOFSTEP]
rw [show (- -[m+1] : ℤ) = (m + 1 : ℤ) by rfl]
[GOAL]
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ - -[m+1] = ↑m + 1
[PROOFSTEP]
rfl
[GOAL]
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -((↑m + 1 - 1) / ↑(Nat.succ n) + 1)
[PROOFSTEP]
rw [add_sub_cancel]
[GOAL]
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -(↑m / ↑(Nat.succ n) + 1)
[PROOFSTEP]
rfl
