α : Type u_1
β : Type ?u.24410
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List (List (Option α))
hm : m < length L
⊢ take m L = take (min m (length L)) (take n L) ↔ m ≤ n
α : Type u_1
β : Type ?u.24410
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List (List (Option α))
hm : m < length L
⊢ take m L <+: take n L ↔ m ≤ n
simp only [prefix_iff_eq_take, length_take]
no goals
α : Type u_1
β : Type ?u.24410
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List (List (Option α))
hm : m < length L
⊢ take m L = take (min m (length L)) (take n L) ↔ m ≤ n
induction m generalizing L n with
| zero => simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
| succ m IH =>
  cases L with
  | nil => exact (not_lt_bot hm).elim
  | cons l ls =>
    cases n with
    | zero =>
      refine' iff_of_false _ (zero_lt_succ _).not_le
      rw [take_zero, take_nil]
      simp only [take]
    | succ n =>
      simp only [length] at hm
      have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
      simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
      simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
      exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
no goals
case zero
α : Type u_1
β : Type ?u.24410
l l₁ l₂ l₃ : List α
a b : α
n : ℕ
L : List (List (Option α))
hm : zero < length L
⊢ take zero L = take (min zero (length L)) (take n L) ↔ zero ≤ n
simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
no goals
case succ
α : Type u_1
β : Type ?u.24410
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
L : List (List (Option α))
hm : succ m < length L
⊢ take (succ m) L = take (min (succ m) (length L)) (take n L) ↔ succ m ≤ n
cases L with
| nil => exact (not_lt_bot hm).elim
| cons l ls =>
  cases n with
  | zero =>
    refine' iff_of_false _ (zero_lt_succ _).not_le
    rw [take_zero, take_nil]
    simp only [take]
  | succ n =>
    simp only [length] at hm
    have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
    simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
    simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
    exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
no goals
case succ.nil
α : Type u_1
β : Type ?u.24410
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
hm : succ m < length []
⊢ take (succ m) [] = take (min (succ m) (length [])) (take n []) ↔ succ m ≤ n
exact (not_lt_bot hm).elim
no goals
case succ.cons
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take n (l :: ls)) ↔ succ m ≤ n
cases n with
| zero =>
  refine' iff_of_false _ (zero_lt_succ _).not_le
  rw [take_zero, take_nil]
  simp only [take]
| succ n =>
  simp only [length] at hm
  have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
  simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
  simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
  exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
case succ.cons.zero
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ ¬take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take zero (l :: ls))
case succ.cons.zero
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take zero (l :: ls)) ↔ succ m ≤ zero
refine' iff_of_false _ (zero_lt_succ _).not_le
case succ.cons.zero
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ ¬take (succ m) (l :: ls) = []
case succ.cons.zero
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ ¬take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take zero (l :: ls))
rw [take_zero, take_nil]
no goals
case succ.cons.zero
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ ¬take (succ m) (l :: ls) = []
simp only [take]
case succ.cons.succ
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
case succ.cons.succ
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
n : ℕ
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
simp only [length] at hm
case succ.cons.succ
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take (min m (length ls)) (take n ls) ↔ m ≤ n
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
case succ.cons.succ
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
case succ.cons.succ
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take m (take n ls) ↔ m ≤ n
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
case succ.cons.succ
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take (min m (length ls)) (take n ls) ↔ m ≤ n
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH
case succ.cons.succ
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take m (take n ls) ↔ m ≤ n
⊢ m ≤ n ↔ succ m ≤ succ n
case succ.cons.succ
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take m (take n ls) ↔ m ≤ n
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
no goals
case succ.cons.succ
α : Type u_1
β : Type ?u.24410
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take m (take n ls) ↔ m ≤ n
⊢ m ≤ n ↔ succ m ≤ succ n
exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩