Theorem: List.take_map_range (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n m : ℕ
f : ℕ → α
⊢ take m (map f (range n)) = map f (range (min n m))
Tactic:
induction' m with m ih
State after:
case zero
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
⊢ take 0 (map f (range n)) = map f (range (min n 0))

case succ
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
⊢ take (m + 1) (map f (range n)) = map f (range (min n (m + 1)))

State before:
case zero
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
⊢ take 0 (map f (range n)) = map f (range (min n 0))
Tactic:
simp
State after:
no goals

State before:
case succ
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
⊢ take (m + 1) (map f (range n)) = map f (range (min n (m + 1)))
Tactic:
simp[take_succ, ih]
State after:
case succ
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
⊢ map f (range (min n m)) ++ (Option.map f ((range n).get? m)).toList = map f (range (min n (m + 1)))

State before:
case succ
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
⊢ map f (range (min n m)) ++ (Option.map f ((range n).get? m)).toList = map f (range (min n (m + 1)))
Tactic:
rcases hm : ((range n).get? m) with (_ | i) <;> simp
State after:
case succ.none
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
⊢ map f (range (min n m)) = map f (range (min n (m + 1)))

case succ.some
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
⊢ map f (range (min n m)) ++ [f i] = map f (range (min n (m + 1)))

State before:
case succ.none
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
⊢ map f (range (min n m)) = map f (range (min n (m + 1)))
Tactic:
have : n ≤ m := by simpa using get?_eq_none.mp hm
State after:
case succ.none
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
this : n ≤ m
⊢ map f (range (min n m)) = map f (range (min n (m + 1)))

State before:
case succ.none
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
this : n ≤ m
⊢ map f (range (min n m)) = map f (range (min n (m + 1)))
Tactic:
simp[Nat.min_eq_left this, Nat.min_eq_left (Nat.le_step this)]
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
⊢ n ≤ m
Tactic:
simpa using get?_eq_none.mp hm
State after:
no goals

State before:
case succ.some
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
⊢ map f (range (min n m)) ++ [f i] = map f (range (min n (m + 1)))
Tactic:
have : m < n ∧ m = i := by simpa using get?_eq_some.mp hm
State after:
case succ.some
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
this : m < n ∧ m = i
⊢ map f (range (min n m)) ++ [f i] = map f (range (min n (m + 1)))

State before:
case succ.some
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
this : m < n ∧ m = i
⊢ map f (range (min n m)) ++ [f i] = map f (range (min n (m + 1)))
Tactic:
rcases this with ⟨lt, rfl⟩
State after:
case succ.some.intro
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
lt : m < n
hm : (range n).get? m = some m
⊢ map f (range (min n m)) ++ [f m] = map f (range (min n (m + 1)))

State before:
case succ.some.intro
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
lt : m < n
hm : (range n).get? m = some m
⊢ map f (range (min n m)) ++ [f m] = map f (range (min n (m + 1)))
Tactic:
simp[Nat.min_eq_right lt, Nat.min_eq_right (le_of_lt lt), range_succ]
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
⊢ m < n ∧ m = i
Tactic:
simpa using get?_eq_some.mp hm
State after:
no goals