-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_flatten (l : Vector (Vector β m) n) (i : Nat) (hi : i < n * m) :
    l.flatten[i] =
      haveI : i / m < n

Proof state:
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
i : Nat
ih : ∀ (i : Nat) (hi : i < l.length * m), (List.map (Array.toList ∘ toArray) l).flatten[i] = l[i / m][i % m]
hi : i < l.length * m + m
h : m ≤ i
⊢ i - m < l.length * m

Tactic:
omega

Result:
no goals

Proof state:
β : Type u_1
m n : Nat
l : Vector (Vector β m) n
i : Nat
hi : i < n * m
⊢ l.flatten[i] = l[i / m][i % m]

Tactic:
rcases l with ⟨⟨l⟩, rfl⟩

Result:
case mk.mk
β : Type u_1
m i : Nat
l : List (Vector β m)
hi : i < { toList := l }.size * m
⊢ { toList := l, size_toArray := ⋯ }.flatten[i] = { toList := l, size_toArray := ⋯ }[i / m][i % m]

Proof state:
case mk.mk.cons
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
⊢ (a.toList ++ (List.map (Array.toList ∘ toArray) l).flatten)[i] = (a :: l)[i / m][i % m]

Tactic:
by_cases h : i < m

Result:
case pos
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : i < m
⊢ (a.toList ++ (List.map (Array.toList ∘ toArray) l).flatten)[i] = (a :: l)[i / m][i % m]

case neg
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : ¬i < m
⊢ (a.toList ++ (List.map (Array.toList ∘ toArray) l).flatten)[i] = (a :: l)[i / m][i % m]

Proof state:
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : ¬i < m
h₁ : a.toList.length ≤ i
⊢ i - m < { toList := l }.size * m

Tactic:
simp_all [Nat.add_one_mul]

Result:
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
i : Nat
ih : ∀ (i : Nat) (hi : i < l.length * m), (List.map (Array.toList ∘ toArray) l).flatten[i] = l[i / m][i % m]
hi : i < l.length * m + m
h : m ≤ i
⊢ i - m < l.length * m

Proof state:
case pos
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : i < m
⊢ (a.toList ++ (List.map (Array.toList ∘ toArray) l).flatten)[i] = (a :: l)[i / m][i % m]

Tactic:
rw [List.getElem_append_left (by simpa)]

Result:
case pos
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : i < m
⊢ a.toList[i] = (a :: l)[i / m][i % m]

Proof state:
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : i < m
⊢ i < a.toList.length

Tactic:
simpa

Result:
no goals

Proof state:
case neg
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : ¬i < m
h₁ : a.toList.length ≤ i
⊢ (List.map (Array.toList ∘ toArray) l).flatten[i - m] = (a :: l)[i / m][i % m]

Tactic:
specialize ih (i - m) (by simp_all [Nat.add_one_mul]; omega)

Result:
case neg
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
i : Nat
hi : i < { toList := a :: l }.size * m
h : ¬i < m
h₁ : a.toList.length ≤ i
ih : (List.map Array.toList (List.map toArray l)).flatten[i - m] = l[(i - m) / m][(i - m) % m]
⊢ (List.map (Array.toList ∘ toArray) l).flatten[i - m] = (a :: l)[i / m][i % m]

Proof state:
case pos
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : i < m
h₁ : i / m = 0
⊢ a.toList[i] = (a :: l)[i / m][i % m]

Tactic:
have h₂ : i % m = i := Nat.mod_eq_of_lt h

Result:
case pos
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : i < m
h₁ : i / m = 0
h₂ : i % m = i
⊢ a.toList[i] = (a :: l)[i / m][i % m]

Proof state:
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
i : Nat
hi : i < { toList := a :: l }.size * m
h : ¬i < m
h₁ : a.toList.length ≤ i
ih : (List.map Array.toList (List.map toArray l)).flatten[i - m] = l[(i - m) / m][(i - m) % m]
⊢ i = i - m + m

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk.cons
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
⊢ (List.map Array.toList (List.map toArray (a :: l))).flatten[i] = (a :: l)[i / m][i % m]

Tactic:
simp only [List.map_cons, List.map_map, List.flatten_cons]

Result:
case mk.mk.cons
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
⊢ (a.toList ++ (List.map (Array.toList ∘ toArray) l).flatten)[i] = (a :: l)[i / m][i % m]

Proof state:
case pos
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : i < m
h₁ : i / m = 0
h₂ : i % m = i
⊢ a.toList[i] = (a :: l)[i / m][i % m]

Tactic:
simp [h₁, h₂]

Result:
no goals

Proof state:
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : ¬i < m
⊢ m ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case neg
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
i : Nat
hi : i < { toList := a :: l }.size * m
h : ¬i < m
h₁ : a.toList.length ≤ i
ih : (List.map Array.toList (List.map toArray l)).flatten[i - m] = l[(i - m) / m][(i - m) % m]
⊢ (List.map (Array.toList ∘ toArray) l).flatten[i - m] = (a :: l)[i / m][i % m]

Tactic:
have h₂ : i / m = (i - m) / m + 1 := by
  conv => lhs; rw [show i = i - m + m by omega]
  rw [Nat.add_div_right]
  exact Nat.pos_of_lt_mul_left hi

Result:
case neg
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
i : Nat
hi : i < { toList := a :: l }.size * m
h : ¬i < m
h₁ : a.toList.length ≤ i
ih : (List.map Array.toList (List.map toArray l)).flatten[i - m] = l[(i - m) / m][(i - m) % m]
h₂ : i / m = (i - m) / m + 1
⊢ (List.map (Array.toList ∘ toArray) l).flatten[i - m] = (a :: l)[i / m][i % m]