[GOAL]
α : Type u
n m i : ℕ
H : i < length (range' n m)
⊢ nthLe (range' n m) i H = n + i
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
⊢ Pairwise (fun x x_1 => x < x_1) (range n)
[PROOFSTEP]
simp only [range_eq_range', pairwise_lt_range']
[GOAL]
α : Type u
n : ℕ
⊢ Nodup (range n)
[PROOFSTEP]
simp only [range_eq_range', nodup_range']
[GOAL]
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range (succ n)) ↔ ∀ (m : ℕ), m < n → r m (succ m)
[PROOFSTEP]
rw [range_succ]
[GOAL]
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u
r : ℕ → ℕ → Prop
⊢ Chain' r (range zero ++ [zero]) ↔ ∀ (m : ℕ), m < zero → r m (succ m)
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range (succ n) ++ [succ n]) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
[PROOFSTEP]
rw [range_succ]
[GOAL]
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range n ++ [n] ++ [succ n]) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
[PROOFSTEP]
simp only [append_assoc, singleton_append, chain'_append_cons_cons, chain'_singleton, and_true_iff]
[GOAL]
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range n ++ [n]) ∧ r n (succ n) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
[PROOFSTEP]
rw [hn, forall_lt_succ]
[GOAL]
α : Type u
r : ℕ → ℕ → Prop
n a : ℕ
⊢ Chain r a (range (succ n)) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m (succ m)
[PROOFSTEP]
rw [range_succ_eq_map, chain_cons, and_congr_right_iff, ← chain'_range_succ, range_succ_eq_map]
[GOAL]
α : Type u
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (Chain r 0 (map succ (range n)) ↔ Chain' (fun m => r m) (0 :: map succ (range n)))
[PROOFSTEP]
exact fun _ => Iff.rfl
[GOAL]
α : Type u
n : ℕ
⊢ Pairwise (fun x x_1 => x > x_1) (iota n)
[PROOFSTEP]
simpa only [iota_eq_reverse_range', pairwise_reverse] using pairwise_lt_range' 1 n
[GOAL]
α : Type u
n : ℕ
a : Fin n
⊢ { val := ↑a, isLt := (_ : ↑a < n) } = a
[PROOFSTEP]
cases a
[GOAL]
case mk
α : Type u
n val✝ : ℕ
isLt✝ : val✝ < n
⊢ { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := (_ : ↑{ val := val✝, isLt := isLt✝ } < n) } =
    { val := val✝, isLt := isLt✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
n : ℕ
⊢ length (finRange n) = n
[PROOFSTEP]
rw [finRange, length_pmap, length_range]
[GOAL]
α : Type u
n : ℕ
⊢ finRange n = [] ↔ n = 0
[PROOFSTEP]
rw [← length_eq_zero, length_finRange]
[GOAL]
α✝ α : Type u
inst✝ : Monoid α
f : ℕ → α
n : ℕ
⊢ prod (map f (range (succ n))) = prod (map f (range n)) * f n
[PROOFSTEP]
rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
[GOAL]
α✝ α : Type u
inst✝ : Monoid α
f : ℕ → α
n : ℕ
⊢ 1 * f 0 = f 0 * 1
[PROOFSTEP]
rw [one_mul, mul_one]
[GOAL]
α✝ α : Type u
inst✝ : Monoid α
f : ℕ → α
n x✝ : ℕ
hd : prod (map f (range (succ x✝))) = f 0 * prod (map (fun i => f (succ i)) (range x✝))
⊢ prod (map f (range (succ (succ x✝)))) = f 0 * prod (map (fun i => f (succ i)) (range (succ x✝)))
[PROOFSTEP]
rw [List.prod_range_succ, hd, mul_assoc, ← List.prod_range_succ]
[GOAL]
α : Type u
l : List α
⊢ unzip (enum l) = (range (length l), l)
[PROOFSTEP]
simp only [enum_eq_zip_range, unzip_zip, length_range]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ unzip (enumFrom n l) = (range' n (length l), l)
[PROOFSTEP]
simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
[GOAL]
α : Type u
n i : ℕ
h : i < length (finRange n)
⊢ get (finRange n) { val := i, isLt := h } = { val := i, isLt := (_ : i < n) }
[PROOFSTEP]
simp only [finRange, get_range, get_pmap]
  --Porting note: new theorem, corresponding theorem used to be in Data.List.FinRange
[GOAL]
α : Type u
l : List α
⊢ length (map (get l) (finRange (length l))) = length l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
⊢ ∀ (n : ℕ) (h₁ : n < length (map (get l) (finRange (length l)))) (h₂ : n < length l),
    get (map (get l) (finRange (length l))) { val := n, isLt := h₁ } = get l { val := n, isLt := h₂ }
[PROOFSTEP]
simp
