flatMap — Mathlib

Lean4
/-- The `flatMap` function on lists is well defined on `ListBlank`s provided that the default
element is sent to a sequence of default elements. -/
def flatMap {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (l : ListBlank Γ) (f : Γ → List Γ')
    (hf : ∃ n, f default = List.replicate n default) : ListBlank Γ' :=
  by
  apply l.liftOn (fun l ↦ ListBlank.mk (l.flatMap f))
  rintro l _ ⟨i, rfl⟩; obtain ⟨n, e⟩ := hf; refine Quotient.sound' (Or.inl ⟨i * n, ?_⟩)
  rw [List.flatMap_append, mul_comm]; congr
  induction i with
  | zero => rfl
  | succ i IH => simp only [IH, e, List.replicate_add, Nat.mul_succ, add_comm, List.replicate_succ, List.flatMap_cons]
Похожие утверждения