awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
f : Fin (succ 0) → α
zero : ofFn f = concat [] (f (Fin.last 0))
zero₁ : ofFn f = [f (Fin.last 0)]
zero₂ : (f 0 :: ofFn (n := 0) fun (i : Fin 0) ↦ f i.succ) = [f (Fin.last 0)]
zero₃ : [f 0] = [f (Fin.last 0)]
⊢ ofFn f = concat (ofFn (n := 0) fun (i : Fin 0) ↦ f i.castSucc) (f (Fin.last 0))
have zero₄ : [f 0] = [f 0]
Tactic: rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc) (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ ofFn f = concat (ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ f i.castSucc) (f (Fin.last (n + 1)))
have succ : f 0 :: concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc.succ) (f (Fin.last n.succ)) =
  f 0 :: concat (ofFn (n := n) fun (i : Fin n) ↦ f i.succ.castSucc) (f (Fin.last (n + 1)))
Tactic: rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero, Fin.succ_last]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n : ℕ
f : Fin n.succ → α
⊢ ofFn f = concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc) (f (Fin.last n))
have zero : ∀ (f : Fin (succ 0) → α), ofFn f = concat (ofFn (n := 0) fun (i : Fin 0) ↦ f i.castSucc) (f (Fin.last 0))
Tactic: induction n with
  | zero => rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]
  | succ n IH =>
    rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero, Fin.succ_last]
    simp only [succ_eq_add_one, Fin.castSucc_succ]
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n : ℕ
f : Fin n.succ → α
zero : ∀ (f : Fin (succ 0) → α), ofFn f = concat (ofFn (n := 0) fun (i : Fin 0) ↦ f i.castSucc) (f (Fin.last 0))
⊢ ofFn f = concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc) (f (Fin.last n))
have succ : ∀ (n : ℕ) (IH : ∀ (f : Fin n.succ → α), ofFn f = concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc) (f (Fin.last n)))
  (f : Fin (n + 1).succ → α),
  ofFn f = concat (ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ f i.castSucc) (f (Fin.last (n + 1)))
Tactic: induction n with
  | zero => rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]
  | succ n IH =>
    rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero, Fin.succ_last]
    simp only [succ_eq_add_one, Fin.castSucc_succ]
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b
have simp_rw : HAppend.hAppend (α := List α) (ofFn (n := m) fun (i : Fin m) ↦ Fin.append a b (Fin.castLE sorry i))
    (ofFn (n := n) fun (i : Fin n) ↦ Fin.append a b (Fin.natAdd m i)) =
  ofFn a ++ ofFn b
Tactic: simp_rw [ofFn_add]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
⊢ (↑i : ℕ) * n + n = ((↑i : ℕ) + 1) * n
have rw : (↑i : ℕ) * n + n = (↑i : ℕ) * n + 1 * n
Tactic: rw [Nat.add_mul, Nat.one_mul]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
rw : (↑i : ℕ) * n + n = (↑i : ℕ) * n + 1 * n
⊢ (↑i : ℕ) * n + n = ((↑i : ℕ) + 1) * n
have rw₁ : (↑i : ℕ) * n + n = (↑i : ℕ) * n + n
Tactic: rw [Nat.add_mul, Nat.one_mul]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = flatten (ofFn (n := m) fun (i : Fin m) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), ⋯⟩)
f : Fin ((m + 1) * n) → α
⊢ ofFn f =
    flatten (ofFn (n := m + 1) fun (i : Fin (m + 1)) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), ⋯⟩)
have succ : Eq.{u + 1} (α := List α) (ofFn (n := m * n + n) fun (i : Fin (m * n + n)) ↦ f (Fin.cast sorry i))
  (flatten
    (concat (ofFn (n := m) fun (i : Fin m) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i.castSucc : ℕ) * n + (↑j : ℕ), sorry⟩)
      (ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑(Fin.last m) : ℕ) * n + (↑j : ℕ), sorry⟩)))
Tactic: simp_rw [ofFn_succ', succ_mul]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = flatten (ofFn (n := m) fun (i : Fin m) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), ⋯⟩)
f : Fin ((m + 1) * n) → α
⊢ Eq.{u + 1} (α := List α) (ofFn (n := m * n + n) fun (i : Fin (m * n + n)) ↦ f (Fin.cast ⋯ i))
    (flatten
      (concat (ofFn (n := m) fun (i : Fin m) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i.castSucc : ℕ) * n + (↑j : ℕ), ⋯⟩)
        (ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑(Fin.last m) : ℕ) * n + (↑j : ℕ), ⋯⟩)))
have succ : Eq.{u + 1} (α := List α) (ofFn (n := n) fun (i : Fin n) ↦ f (Fin.cast sorry (Fin.natAdd (m * n) i)))
  (ofFn (n := n) fun (j : Fin n) ↦ f ⟨m * n + (↑j : ℕ), sorry⟩)
Tactic: simp [ofFn_add, IH]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = flatten (ofFn (n := m) fun (i : Fin m) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), ⋯⟩)
have zero : ∀ (f : Fin (0 * n) → α),
  ofFn f = flatten (ofFn (n := 0) fun (i : Fin 0) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), sorry⟩)
Tactic: induction m with
  | zero => simp [ofFn_zero, Nat.zero_mul, ofFn_zero]
  | succ m IH =>
    simp_rw [ofFn_succ', succ_mul]
    simp [ofFn_add, IH]
    rfl
Cleared hypotheses: m, f
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
zero :
  ∀ (f : Fin (0 * n) → α),
    ofFn f = flatten (ofFn (n := 0) fun (i : Fin 0) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), ⋯⟩)
⊢ ofFn f = flatten (ofFn (n := m) fun (i : Fin m) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), ⋯⟩)
have succ : ∀ (m : ℕ)
  (IH :
    ∀ (f : Fin (m * n) → α),
      ofFn f = flatten (ofFn (n := m) fun (i : Fin m) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), sorry⟩))
  (f : Fin ((m + 1) * n) → α),
  ofFn f =
    flatten (ofFn (n := m + 1) fun (i : Fin (m + 1)) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), sorry⟩)
Tactic: induction m with
  | zero => simp [ofFn_zero, Nat.zero_mul, ofFn_zero]
  | succ m IH =>
    simp_rw [ofFn_succ', succ_mul]
    simp [ofFn_add, IH]
    rfl
Cleared hypotheses: m, f
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
⊢ m * (↑i : ℕ) + m = m * ((↑i : ℕ) + 1)
have rw : m * (↑i : ℕ) + m = m * (↑i : ℕ) + m * 1
Tactic: rw [Nat.mul_add, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
rw : m * (↑i : ℕ) + m = m * (↑i : ℕ) + m * 1
⊢ m * (↑i : ℕ) + m = m * ((↑i : ℕ) + 1)
have rw₁ : m * (↑i : ℕ) + m = m * (↑i : ℕ) + m
Tactic: rw [Nat.mul_add, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ f ⟨m * (↑i : ℕ) + (↑j : ℕ), ⋯⟩)
have simp_rw : Eq.{u + 1} (α := List α) (ofFn (n := n * m) fun (i : Fin (n * m)) ↦ f (Fin.cast sorry i))
  (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ f ⟨(↑i : ℕ) * m + (↑j : ℕ), sorry⟩))
Tactic: simp_rw [m.mul_comm, ofFn_mul, Fin.cast_mk]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
simp_rw :
  Eq.{u + 1} (α := List α) (ofFn (n := n * m) fun (i : Fin (n * m)) ↦ f (Fin.cast ⋯ i))
    (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ f ⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩))
⊢ ofFn f = flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ f ⟨m * (↑i : ℕ) + (↑j : ℕ), ⋯⟩)
have simp_rw₁ : Eq.{u + 1} (α := List α)
  (flatten
    (ofFn (n := n) fun (i : Fin n) ↦
      ofFn (n := m) fun (j : Fin m) ↦ f (Fin.cast sorry (⟨(↑i : ℕ) * m + (↑j : ℕ), sorry⟩ : Fin (n * m)))))
  (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ f ⟨(↑i : ℕ) * m + (↑j : ℕ), sorry⟩))
Tactic: simp_rw [m.mul_comm, ofFn_mul, Fin.cast_mk]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List α) (ofFn (n := length.{u} (α := α) []) (get [])) []
have rw : Eq.{u + 1} (α := List α) [] []
Tactic: rw [ofFn_zero]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
a : α
l : List α
⊢ ofFn (a :: l).get = a :: l
have rw : ((a :: l).get 0 :: ofFn (n := l.length) fun (i : Fin l.length) ↦ (a :: l).get i.succ) = a :: l
Tactic: rw [ofFn_succ]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
a : α
l : List α
⊢ ((a :: l).get 0 :: ofFn (n := l.length) fun (i : Fin l.length) ↦ (a :: l).get i.succ) = a :: l
have e_tail : (ofFn (n := l.length) fun (i : Fin l.length) ↦ (a :: l).get i.succ) = l
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
β : Type u_1
l : List α
f : α → β
⊢ (ofFn (n := l.length) fun (i : Fin l.length) ↦
      f (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯)) =
    map f l
have rw : ofFn (n := l.length)
    (f ∘ fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) =
  map f l
Tactic: rw [← Function.comp_def, ← map_ofFn, ofFn_getElem]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
β : Type u_1
l : List α
f : α → β
rw :
  ofFn (n := l.length)
      (f ∘ fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) =
    map f l
⊢ (ofFn (n := l.length) fun (i : Fin l.length) ↦
      f (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯)) =
    map f l
have rw₁ : map f
    (ofFn (n := l.length) fun (i : Fin l.length) ↦
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) =
  map f l
Tactic: rw [← Function.comp_def, ← map_ofFn, ofFn_getElem]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
β : Type u_1
l : List α
f : α → β
rw :
  ofFn (n := l.length)
      (f ∘ fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) =
    map f l
rw₁ :
  map f
      (ofFn (n := l.length) fun (i : Fin l.length) ↦
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) =
    map f l
⊢ (ofFn (n := l.length) fun (i : Fin l.length) ↦
      f (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯)) =
    map f l
have rw₂ : map f l = map f l
Tactic: rw [← Function.comp_def, ← map_ofFn, ofFn_getElem]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
c : α
⊢ (ofFn (n := 0) fun (x : Fin 0) ↦ c) = replicate 0 c
have rw : [] = replicate 0 c
Tactic: rw [ofFn_zero, replicate_zero]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
c : α
rw : [] = replicate 0 c
⊢ (ofFn (n := 0) fun (x : Fin 0) ↦ c) = replicate 0 c
have rw₁ : Eq.{u + 1} (α := List α) [] []
Tactic: rw [ofFn_zero, replicate_zero]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n : ℕ
c : α
⊢ (ofFn (n := n + 1) fun (x : Fin (n + 1)) ↦ c) = replicate (n + 1) c
have rw : (ofFn (n := n + 1) fun (x : Fin (n + 1)) ↦ c) = c :: ofFn (n := n) fun (x : Fin n) ↦ c
Tactic: rw [replicate, ← ofFn_const n]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten
have simp_rw : flatten
    (ofFn (n := n) fun (i : Fin n) ↦
      ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), sorry⟩ : Fin (n * m))) =
  (replicate n (ofFn a)).flatten
Tactic: simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
    Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
simp_rw :
  flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m))) =
    (replicate n (ofFn a)).flatten
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten
have simp_rw₁ : Eq.{u + 1} (α := List α)
  (flatten
    (ofFn (n := n) fun (i : Fin n) ↦
      ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), sorry⟩ : Fin (n * m))))
  (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
Tactic: simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
    Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
simp_rw :
  flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m))) =
    (replicate n (ofFn a)).flatten
simp_rw₁ :
  Eq.{u + 1} (α := List α)
    (flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m))))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten
have simp_rw₂ : Eq.{u + 1} (α := List α)
  (flatten
    (ofFn (n := n) fun (i : Fin n) ↦
      ofFn (n := m) fun (j : Fin m) ↦ a (⟨(↑i : ℕ) * m + (↑j : ℕ), sorry⟩ : Fin (n * m)).modNat))
  (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
Tactic: simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
    Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
simp_rw :
  flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m))) =
    (replicate n (ofFn a)).flatten
simp_rw₁ :
  Eq.{u + 1} (α := List α)
    (flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m))))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
simp_rw₂ :
  Eq.{u + 1} (α := List α)
    (flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m)).modNat))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten
have simp_rw₃ : Eq.{u + 1} (α := List α)
  (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ a ⟨((↑i : ℕ) * m + (↑j : ℕ)) % m, sorry⟩))
  (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
Tactic: simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
    Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
simp_rw :
  flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m))) =
    (replicate n (ofFn a)).flatten
simp_rw₁ :
  Eq.{u + 1} (α := List α)
    (flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m))))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
simp_rw₂ :
  Eq.{u + 1} (α := List α)
    (flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m)).modNat))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
simp_rw₃ :
  Eq.{u + 1} (α := List α)
    (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ a ⟨((↑i : ℕ) * m + (↑j : ℕ)) % m, ⋯⟩))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten
have simp_rw₄ : Eq.{u + 1} (α := List α)
  (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ a ⟨((↑j : ℕ) + (↑i : ℕ) * m) % m, sorry⟩))
  (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
Tactic: simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
    Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
simp_rw :
  flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m))) =
    (replicate n (ofFn a)).flatten
simp_rw₁ :
  Eq.{u + 1} (α := List α)
    (flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ Fin.repeat n a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m))))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
simp_rw₂ :
  Eq.{u + 1} (α := List α)
    (flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ a (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m)).modNat))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
simp_rw₃ :
  Eq.{u + 1} (α := List α)
    (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ a ⟨((↑i : ℕ) * m + (↑j : ℕ)) % m, ⋯⟩))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
simp_rw₄ :
  Eq.{u + 1} (α := List α)
    (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ a ⟨((↑j : ℕ) + (↑i : ℕ) * m) % m, ⋯⟩))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten
have simp_rw₅ : Eq.{u + 1} (α := List α) (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ a ⟨(↑j : ℕ) % m, sorry⟩))
  (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
Tactic: simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
    Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ ofFn (n := n + 1) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ α) a f) = a :: ofFn f
have rw : (Fin.cons (α := fun (a : Fin (n + 1)) ↦ α) a f 0 ::
    ofFn (n := n) fun (i : Fin n) ↦ Fin.cons (α := fun (a : Fin (n + 1)) ↦ α) a f i.succ) =
  a :: ofFn f
Tactic: rw [ofFn_succ]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
⊢ find? p (ofFn f) = some b ↔ p b = true ∧ ∃ (i : Fin n), f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
have rw : (p b = true ∧
    ∃ (i : ℕ),
      ∃ (h : i < (ofFn f).length),
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) i h = b ∧
          ∀ (j : ℕ) (hj : j < i),
            (!p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) j sorry)) = true) ↔
  p b = true ∧ ∃ (i : Fin n), f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
Tactic: rw [find?_eq_some_iff_getElem]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (hypothesis)
Goal:
α : Type u
n : ℕ
f g : Fin n → α
h : ofFn f = ofFn g
⊢ f ≍ g
have h₁ : Eq.{u + 1} (α := (n : ℕ) × (Fin n → α)) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → α) n f)
  (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → α) n g)
Tactic: rw [ofFn_inj'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n : ℕ
f g : Fin n → α
h :
  Eq.{u + 1} (α := (n : ℕ) × (Fin n → α)) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → α) n f)
    (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → α) n g)
⊢ f ≍ g
have refl : f ≍ f
Tactic: cases h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
a : α
l : List α
⊢ (a :: l).offDiag ~
    HAppend.hAppend (α := List (α × α)) (map (fun (x : α) ↦ (a, x)) l) (map (fun (x : α) ↦ (x, a)) l) ++ l.offDiag
have simp : flatMap (fun (x : α × ℕ) ↦ map (Prod.mk x.fst) ((a :: l).eraseIdx x.snd))
    ((a, 0) :: map (Prod.map id fun (x : ℕ) ↦ x + 1) l.zipIdx) ~
  HAppend.hAppend (α := List (α × α)) (map (fun (x : α) ↦ (a, x)) l) (map (fun (x : α) ↦ (x, a)) l) ++
    flatMap (fun (x : α × ℕ) ↦ map (Prod.mk x.fst) (l.eraseIdx x.snd)) l.zipIdx
Tactic: simp only [offDiag, zipIdx_cons']
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
a : α
l : List α
| map (fun (x : α) ↦ (x, a)) l
have rw : map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx
Tactic: rw [← zipIdx_map_fst 0 l, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
a : α
l : List α
⊢ Eq (α := List (α × α)) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx) (map (fun (x : α) ↦ (x, a)) l)
have conv_rhs : Eq (α := List (α × α)) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx) (map (fun (x : α) ↦ (x, a)) l)
Tactic: conv_rhs => rw [← zipIdx_map_fst 0 l, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
a : α
l : List α
conv_rhs : Eq (α := List (α × α)) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx) (map (fun (x : α) ↦ (x, a)) l)
⊢ Eq (α := List (α × α)) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx) (map (fun (x : α) ↦ (x, a)) l)
have conv_rhs₁ : Eq (α := List (α × α)) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx)
Tactic: conv_rhs => rw [← zipIdx_map_fst 0 l, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (hypothesis)
Goal:
α : Type u_1
a : α
l : List α
⊢ flatMap (fun (x : α × ℕ) ↦ map (Prod.mk x.fst) ((a :: l).eraseIdx x.snd))
      ((a, 0) :: map (Prod.map id fun (x : ℕ) ↦ x + 1) l.zipIdx) ~
    HAppend.hAppend (α := List (α × α)) (map (fun (x : α) ↦ (a, x)) l) (map (fun (x : α) ↦ (x, a)) l) ++
      flatMap (fun (x : α × ℕ) ↦ map (Prod.mk x.fst) (l.eraseIdx x.snd)) l.zipIdx
have this : Eq (α := List (α × α)) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx) (map (fun (x : α) ↦ (x, a)) l)
Tactic: have : map (fun x ↦ (x.fst, a)) l.zipIdx = map (·, a) l := by
    conv_rhs => rw [← zipIdx_map_fst 0 l, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (hypothesis)
Goal:
α : Type u_1
l : List α
⊢ l.offDiag.length = l.length * (l.length - 1)
have this : ∀ (x : α × ℕ), x ∈ l.zipIdx → (l.eraseIdx x.snd).length = l.length - 1
Tactic: have : ∀ x ∈ l.zipIdx, length (eraseIdx l x.2) = length l - 1 := fun x hx ↦
    length_eraseIdx_of_lt <| snd_lt_of_mem_zipIdx hx
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
x : α × α
⊢ x ∈ l.offDiag ↔
    ∃ (i : ℕ),
      ∃ (x_1 : i < l.length),
        ∃ (j : ℕ),
          ∃ (x_2 : j < l.length),
            i ≠ j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x_1 = x.fst ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j x_2 = x.snd
have rcases : ∀ (x y : α),
  (x, y) ∈ l.offDiag ↔
    ∃ (i : ℕ),
      ∃ (x_1 : i < l.length),
        ∃ (j : ℕ),
          ∃ (x_2 : j < l.length),
            i ≠ j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x_1 = (x, y).fst ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j x_2 = (x, y).snd
Tactic: rcases x with ⟨x, y⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
⊢ count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
have pos : ∀ (h : z = x), count (x, y) (map (fun (x : α) ↦ (z, x)) l) = count y l
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
pos : ∀ (h : z = x), count (x, y) (map (fun (x : α) ↦ (z, x)) l) = count y l
⊢ count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
have neg : ∀ (h : ¬z = x), count (x, y) (map (fun (x : α) ↦ (z, x)) l) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : z = x
⊢ count (x, y) (map (fun (x : α) ↦ (z, x)) l) = count y l
have pos : count (x, y) (map (fun (x_1 : α) ↦ (x, x_1)) l) = count y l
Tactic: rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]