-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_flatten_iff {L : List (List α)} {l} :
    l <+ L.flatten ↔
      ∃ L' : List (List α), l = L'.flatten ∧ ∀ i (_ : i < L'.length), 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 <+ L.flatten ↔ ∃ 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'_1.length), L'_1[i] <+ (l' :: L)[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 <+ L.flatten ↔ ∃ 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 cons
α : Type u_1
l' : List α
L : List (List α)
ih : ∀ {l : List α}, l <+ L.flatten ↔ ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L'.length), L'[i] <+ L[i]?.getD []
l : List α
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ l' ∧ ∃ L', l₂ = L'.flatten ∧ ∀ (i : Nat) (x : i < L'.length), L'[i] <+ L[i]?.getD []) ↔
    ∃ L', l = L'.flatten ∧ ∀ (i : Nat) (x : i < L'.length), L'[i] <+ (l' :: L)[i]?.getD []

Tactic:
constructor

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

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

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

Tactic:
intro w

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

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

Tactic:
cases x

Result:
no goals

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

Tactic:
constructor

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

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

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

Tactic:
simp only [flatten_nil, sublist_nil, flatten_eq_nil_iff]

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

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

Tactic:
simp

Result:
no goals

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