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

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

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 <+ 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 []

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

Proof state:
α : Type u_1
⊢ [] = [].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 []
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:
α : 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 []
⊢ 0 < (l₁ :: L').length

Tactic:
simp

Result:
no goals

Proof state:
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 []

Tactic:
simp only [flatten_nil, sublist_nil] at w

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

Tactic:
simp

Result:
no goals

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

Tactic:
rintro ⟨L', rfl, h⟩

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

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

Tactic:
subst w

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

Proof state:
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 []

Tactic:
cases L' with
| nil =>
  exact ⟨[], [], by simp, by simp, [], by simp, fun i x => by cases x⟩
| 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 <+ 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₁ <+ l'

Tactic:
simpa using h 0 (by simp)

Result:
no goals

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 : List α), l ∈ L' → l = []

Tactic:
simp only [getElem?_nil, Option.getD_none, sublist_nil] at h

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

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

Tactic:
simp only [flatten_cons, sublist_append_iff, ih]

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

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

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

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 <+ 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
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 <+ 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 []
⊢ [] <+ l'

Tactic:
simp

Result:
no goals