-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem flatten_sublist_iff {L : List (List α)} {l} :
    L.flatten <+ l ↔
      ∃ L' : List (List α), l = L'.flatten ∧ ∀ i (_ : i < L.length), L[i] <+ L'[i]?.getD []

Proof state:
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
h : ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ [][i]?.getD []
i : Nat
x : i < L.length
⊢ L[i] <+ [][i]?.getD []

Tactic:
simpa using h (i+1) (Nat.add_lt_add_right x 1)

Result:
no goals

Proof state:
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
l₁ : List α
s : l' <+ l₁
L' : List (List α)
h : ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
⊢ l₁ ++ L'.flatten = (l₁ :: L').flatten

Tactic:
simp

Result:
no goals

Proof state:
case nil.mpr.intro.intro
α : Type u_1
L' : List (List α)
right✝ : ∀ (i : Nat) (x : i < [].length), [][i] <+ L'[i]?.getD []
⊢ [].flatten <+ L'.flatten

Tactic:
simp only [flatten_nil, nil_sublist]

Result:
no goals

Proof state:
case nil.mp
α : Type u_1
l : List α
a✝ : [].flatten <+ l
⊢ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < [].length), [][i] <+ L'[i]?.getD []

Tactic:
exact ⟨[l], by simp, fun i x => by cases x⟩

Result:
no goals

Proof state:
case cons.mpr.intro.intro.cons
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
l₁ : List α
L' : List (List α)
h : ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ (l₁ :: L')[i]?.getD []
⊢ ∃ r₁ r₂,
    (l₁ :: L').flatten = r₁ ++ r₂ ∧
      l' <+ r₁ ∧ ∃ L', r₂ = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []

Tactic:
exact ⟨l₁, L'.flatten, by simp, by simpa using h 0 (by simp), L', rfl,
  fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩

Result:
no goals

Proof state:
case cons.mpr.intro.intro.nil
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
h : ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ [][i]?.getD []
⊢ ∃ r₁ r₂,
    [].flatten = r₁ ++ r₂ ∧ l' <+ r₁ ∧ ∃ L', r₂ = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []

Tactic:
exact ⟨[], [], by simp, by simpa using h 0 (by simp), [], by simp,
  fun i x => by simpa using h (i+1) (Nat.add_lt_add_right x 1)⟩

Result:
no goals

Proof state:
case cons.mp
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
l : List α
⊢ (∃ r₁ r₂, l = r₁ ++ r₂ ∧ l' <+ r₁ ∧ ∃ L', r₂ = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []) →
    ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ L'[i]?.getD []

Tactic:
rintro ⟨l₁, l₂, rfl, s, L', rfl, h⟩

Result:
case cons.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
l₁ : List α
s : l' <+ l₁
L' : List (List α)
h : ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
⊢ ∃ L'_1, l₁ ++ L'.flatten = L'_1.flatten ∧ ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ L'_1[i]?.getD []

Proof state:
case cons.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
l₁ : List α
s : l' <+ l₁
L' : List (List α)
h : ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
i : Nat
lt : i < (l' :: L).length
⊢ (l' :: L)[i] <+ (l₁ :: L')[i]?.getD []

Tactic:
cases i <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
l₁ : List α
L' : List (List α)
h : ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ (l₁ :: L')[i]?.getD []
⊢ (l₁ :: L').flatten = l₁ ++ L'.flatten

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
a✝ : [].flatten <+ l
i : Nat
x : i < [].length
⊢ [][i] <+ [l][i]?.getD []

Tactic:
cases x

Result:
no goals

Proof state:
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
h : ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ [][i]?.getD []
⊢ [] = [].flatten

Tactic:
simp

Result:
no goals

Proof state:
case cons.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
l₁ : List α
s : l' <+ l₁
L' : List (List α)
h : ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
⊢ ∃ L'_1, l₁ ++ L'.flatten = L'_1.flatten ∧ ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ L'_1[i]?.getD []

Tactic:
refine ⟨l₁ :: L', by simp, ?_⟩

Result:
case cons.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
l₁ : List α
s : l' <+ l₁
L' : List (List α)
h : ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
⊢ ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ (l₁ :: L')[i]?.getD []

Proof state:
case nil
α : Type u_1
l : List α
⊢ [].flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < [].length), [][i] <+ L'[i]?.getD []

Tactic:
constructor

Result:
case nil.mp
α : Type u_1
l : List α
⊢ [].flatten <+ l → ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < [].length), [][i] <+ L'[i]?.getD []

case nil.mpr
α : Type u_1
l : List α
⊢ (∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < [].length), [][i] <+ L'[i]?.getD []) → [].flatten <+ l

Proof state:
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
h : ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ [][i]?.getD []
⊢ 0 < (l' :: L).length

Tactic:
simp

Result:
no goals

Proof state:
case cons.mpr.intro.intro
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
L' : List (List α)
h : ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ L'[i]?.getD []
⊢ ∃ r₁ r₂,
    L'.flatten = r₁ ++ r₂ ∧ l' <+ r₁ ∧ ∃ L', r₂ = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []

Tactic:
cases L' with
| nil =>
  exact ⟨[], [], by simp, by simpa using h 0 (by simp), [], by simp,
    fun i x => by simpa using h (i+1) (Nat.add_lt_add_right x 1)⟩
| cons l₁ L' =>
  exact ⟨l₁, L'.flatten, by simp, by simpa using h 0 (by simp), L', rfl,
    fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩

Result:
no goals

Proof state:
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, L.flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []
l₁ : List α
L' : List (List α)
h : ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ (l₁ :: L')[i]?.getD []
⊢ 0 < (l' :: L).length

Tactic:
simp

Result:
no goals