-- 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:
case cons.mpr
α : 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', l = L'.flatten ∧ ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ L'[i]?.getD []) →
    ∃ r₁ r₂, l = r₁ ++ r₂ ∧ l' <+ r₁ ∧ ∃ L', r₂ = L'.flatten ∧ ∀ (i : Nat) (x : i < L.length), L[i] <+ L'[i]?.getD []

Tactic:
rintro ⟨L', rfl, h⟩

Result:
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 []

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

Tactic:
intro _

Result:
case nil.mp
α : Type u_1
l : List α
a✝ : [].flatten <+ l
⊢ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < [].length), [][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 []
⊢ l' <+ []

Tactic:
simpa using h 0 (by simp)

Result:
no goals

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

Tactic:
rintro ⟨L', rfl, _⟩

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

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:
α : Type u_1
l : List α
a✝ : [].flatten <+ l
⊢ l = [l].flatten

Tactic:
simp

Result:
no goals

Proof state:
case 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 α
⊢ (∃ 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:
constructor

Result:
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 []

case cons.mpr
α : 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', l = L'.flatten ∧ ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ L'[i]?.getD []) →
    ∃ r₁ r₂, l = r₁ ++ r₂ ∧ l' <+ r₁ ∧ ∃ L', r₂ = L'.flatten ∧ ∀ (i : Nat) (x : 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 []
l₁ : List α
L' : List (List α)
h : ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ (l₁ :: L')[i]?.getD []
⊢ l' <+ l₁

Tactic:
simpa using h 0 (by simp)

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 []
i : Nat
lt : i < L.length
⊢ L[i] <+ L'[i]?.getD []

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

Result:
no goals

Proof state:
case 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' :: L).flatten <+ l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < (l' :: L).length), (l' :: L)[i] <+ L'[i]?.getD []

Tactic:
simp only [flatten_cons, append_sublist_iff, ih]

Result:
case 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 α
⊢ (∃ 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 []

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) (x : i < (l' :: L).length), (l' :: L)[i] <+ (l₁ :: L')[i]?.getD []

Tactic:
intro i lt

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
lt : i < (l' :: L).length
⊢ (l' :: L)[i] <+ (l₁ :: L')[i]?.getD []