-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
    L = L' ↔ L.flatten = L'.flatten ∧ map length L = map length L'
  | _, [] => by simp_all
  | [], x' :: L' => by simp_all
  | x :: L, x' :: L' => by
    simp
    rw [eq_iff_flatten_eq]
    constructor
    · rintro ⟨rfl, h₁, h₂⟩
      simp_all
    · rintro ⟨h₁, h₂, h₃⟩
      obtain ⟨rfl, h⟩ := append_inj h₁ h₂
      exact ⟨rfl, h, h₃⟩

Proof state:
α : Type u_1
x' : List α
L' : List (List α)
⊢ [] = x' :: L' ↔ [].flatten = (x' :: L').flatten ∧ map length [] = map length (x' :: L')

Tactic:
simp_all

Result:
no goals

Proof state:
case mp
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
⊢ x = x' ∧ L.flatten = L'.flatten ∧ map length L = map length L' →
    x ++ L.flatten = x' ++ L'.flatten ∧ x.length = x'.length ∧ map length L = map length L'

Tactic:
rintro ⟨rfl, h₁, h₂⟩

Result:
case mp.intro.intro
α : Type u_1
x : List α
L L' : List (List α)
h₁ : L.flatten = L'.flatten
h₂ : map length L = map length L'
⊢ x ++ L.flatten = x ++ L'.flatten ∧ x.length = x.length ∧ map length L = map length L'

Proof state:
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
⊢ x = x' ∧ L = L' ↔ x ++ L.flatten = x' ++ L'.flatten ∧ x.length = x'.length ∧ map length L = map length L'

Tactic:
rw [eq_iff_flatten_eq]

Result:
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
⊢ x = x' ∧ L.flatten = L'.flatten ∧ map length L = map length L' ↔
    x ++ L.flatten = x' ++ L'.flatten ∧ x.length = x'.length ∧ map length L = map length L'

Proof state:
case mp.intro.intro
α : Type u_1
x : List α
L L' : List (List α)
h₁ : L.flatten = L'.flatten
h₂ : map length L = map length L'
⊢ x ++ L.flatten = x ++ L'.flatten ∧ x.length = x.length ∧ map length L = map length L'

Tactic:
simp_all

Result:
no goals

Proof state:
case mpr
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
⊢ x ++ L.flatten = x' ++ L'.flatten ∧ x.length = x'.length ∧ map length L = map length L' →
    x = x' ∧ L.flatten = L'.flatten ∧ map length L = map length L'

Tactic:
rintro ⟨h₁, h₂, h₃⟩

Result:
case mpr.intro.intro
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
h₁ : x ++ L.flatten = x' ++ L'.flatten
h₂ : x.length = x'.length
h₃ : map length L = map length L'
⊢ x = x' ∧ L.flatten = L'.flatten ∧ map length L = map length L'

Proof state:
case mpr.intro.intro.intro
α : Type u_1
x : List α
L L' : List (List α)
h₃ : map length L = map length L'
h : L.flatten = L'.flatten
h₁ : x ++ L.flatten = x ++ L'.flatten
h₂ : x.length = x.length
⊢ x = x ∧ L.flatten = L'.flatten ∧ map length L = map length L'

Tactic:
exact ⟨rfl, h, h₃⟩

Result:
no goals

Proof state:
α : Type u_1
x✝ : List (List α)
⊢ x✝ = [] ↔ x✝.flatten = [].flatten ∧ map length x✝ = map length []

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
⊢ x :: L = x' :: L' ↔ (x :: L).flatten = (x' :: L').flatten ∧ map length (x :: L) = map length (x' :: L')

Tactic:
simp

Result:
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
⊢ x = x' ∧ L = L' ↔ x ++ L.flatten = x' ++ L'.flatten ∧ x.length = x'.length ∧ map length L = map length L'

Proof state:
case mpr.intro.intro
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
h₁ : x ++ L.flatten = x' ++ L'.flatten
h₂ : x.length = x'.length
h₃ : map length L = map length L'
⊢ x = x' ∧ L.flatten = L'.flatten ∧ map length L = map length L'

Tactic:
obtain ⟨rfl, h⟩ := append_inj h₁ h₂

Result:
case mpr.intro.intro.intro
α : Type u_1
x : List α
L L' : List (List α)
h₃ : map length L = map length L'
h : L.flatten = L'.flatten
h₁ : x ++ L.flatten = x ++ L'.flatten
h₂ : x.length = x.length
⊢ x = x ∧ L.flatten = L'.flatten ∧ map length L = map length L'

Proof state:
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
⊢ x = x' ∧ L.flatten = L'.flatten ∧ map length L = map length L' ↔
    x ++ L.flatten = x' ++ L'.flatten ∧ x.length = x'.length ∧ map length L = map length L'

Tactic:
constructor

Result:
case mp
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
⊢ x = x' ∧ L.flatten = L'.flatten ∧ map length L = map length L' →
    x ++ L.flatten = x' ++ L'.flatten ∧ x.length = x'.length ∧ map length L = map length L'

case mpr
α : Type u_1
x : List α
L : List (List α)
x' : List α
L' : List (List α)
⊢ x ++ L.flatten = x' ++ L'.flatten ∧ x.length = x'.length ∧ map length L = map length L' →
    x = x' ∧ L.flatten = L'.flatten ∧ map length L = map length L'