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

Tactic:
simp only [flatten_mk, List.map_toArray, getElem_mk, List.getElem_toArray, Array.flatten_toArray]

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

Proof state:
β : Type ?u.282545
m n : Nat
l : Vector (Vector β m) n
i : Nat
hi : i < n * m
⊢ i / m < n

Tactic:
rwa [Nat.div_lt_iff_lt_mul (Nat.pos_of_lt_mul_left hi)]

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
⊢ (a.toList ++ (List.map (Array.toList ∘ toArray) l).flatten)[i] = (a :: l)[i / m][i % m]

Tactic:
rw [List.getElem_append_right h₁]

Result:
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 - a.toList.length] = (a :: l)[i / m][i % m]

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

Tactic:
simp at hi

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 - a.toList.length] = (a :: l)[i / m][i % m]

Tactic:
simp only [Array.length_toList, size_toArray]

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

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
⊢ (a.toList ++ (List.map (Array.toList ∘ toArray) l).flatten)[i] = (a :: l)[i / m][i % m]

Tactic:
have h₁ : a.toList.length ≤ i := by simp; omega

Result:
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
⊢ (a.toList ++ (List.map (Array.toList ∘ toArray) l).flatten)[i] = (a :: l)[i / m][i % m]

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]
h₂ : i / m = (i - m) / m + 1
h₁ : m ≤ i
h₃ : (i - m) % m = i % m
⊢ (List.map (Array.toList ∘ toArray) l).flatten[i - m] = (a :: l)[i / m][i % m]

Tactic:
simp_all

Result:
no goals

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 - m + m) / m = (i - m) / m + 1

Tactic:
rw [Nat.add_div_right]

Result:
case H
β : 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]
⊢ 0 < m

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]
h₂ : i / m = (i - m) / m + 1
h₁ : m ≤ i
⊢ (List.map (Array.toList ∘ toArray) l).flatten[i - m] = (a :: l)[i / m][i % m]

Tactic:
have h₃ : (i - m) % m = i % m := (Nat.mod_eq_sub_mod h₁).symm

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
h₁ : m ≤ i
h₃ : (i - m) % m = i % m
⊢ (List.map (Array.toList ∘ toArray) l).flatten[i - m] = (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 / m = (i - m) / m + 1

Tactic:
conv => lhs; rw [show i = i - m + m by omega]

Result:
β : 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 - m + m) / m = (i - m) / m + 1

Proof state:
case H
β : 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]
⊢ 0 < m

Tactic:
exact Nat.pos_of_lt_mul_left hi

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
⊢ a.toList.length ≤ i

Tactic:
simp

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

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]
h₂ : i / m = (i - m) / m + 1
⊢ (List.map (Array.toList ∘ toArray) l).flatten[i - m] = (a :: l)[i / m][i % m]

Tactic:
simp only [Array.length_toList, size_toArray] at h₁

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
h₁ : m ≤ i
⊢ (List.map (Array.toList ∘ toArray) l).flatten[i - m] = (a :: l)[i / m][i % m]