awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n.succ → α
zero : ∀ (f : Fin (Nat.succ 0) → α), ofFn f = concat (ofFn (n := 0) fun (i : Fin 0) ↦ f i.castSucc) (f (Fin.last 0))
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)))
⊢ ofFn f = concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc) (f (Fin.last n))

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]

Premises used: Fin.last_zero, Nat.succ_eq_add_one, List.concat_nil, List.concat_cons, Fin.castSucc_succ, List.ofFn_zero, Fin.castSucc_zero, Nat.zero, Fin.succ_last, Nat.succ, List.ofFn_succ
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
simp_rw :
  HAppend.hAppend (α := List α) (ofFn (n := m) fun (i : Fin m) ↦ Fin.append a b (Fin.castLE ⋯ i))
      (ofFn (n := n) fun (i : Fin n) ↦ Fin.append a b (Fin.natAdd m i)) =
    ofFn a ++ ofFn b
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b

Tactic:
simp_rw [ofFn_add]

Premises used: List.ofFn_add
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ HAppend.hAppend (α := List α) (ofFn (n := m) fun (i : Fin m) ↦ Fin.append a b (Fin.castLE ⋯ i))
      (ofFn (n := n) fun (i : Fin n) ↦ Fin.append a b (Fin.natAdd m i)) =
    ofFn a ++ ofFn b

Tactic:
simp [Fin.append_left', Fin.append_right]

Premises used: Fin.append_right, Fin.append_left'
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
rw : (↑i : ℕ) * n + n = (↑i : ℕ) * n + 1 * n
rw₁ rw₂ : (↑i : ℕ) * n + n = (↑i : ℕ) * n + n
⊢ (↑i : ℕ) * n + n = ((↑i : ℕ) + 1) * n

Tactic:
rw [Nat.add_mul, Nat.one_mul]

Premises used: Nat.one_mul, Nat.add_mul
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
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 : ℕ), ⋯⟩)

Tactic:
simp [ofFn_zero, Nat.zero_mul, ofFn_zero]

Premises used: Nat.zero_mul, List.ofFn_zero
-- Module: Mathlib.Data.List.OfFn
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) → α
succ :
  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 : ℕ), ⋯⟩)))
⊢ ofFn f =
    flatten (ofFn (n := m + 1) fun (i : Fin (m + 1)) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), ⋯⟩)

Tactic:
simp_rw [ofFn_succ', succ_mul]

Premises used: List.ofFn_succ', Nat.succ_mul
-- Module: Mathlib.Data.List.OfFn
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) → α
succ :
  Eq.{u + 1} (α := List α) (ofFn (n := n) fun (i : Fin n) ↦ f (Fin.cast ⋯ (Fin.natAdd (m * n) i)))
    (ofFn (n := n) fun (j : Fin n) ↦ f ⟨m * n + (↑j : ℕ), ⋯⟩)
⊢ 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 : ℕ), ⋯⟩)))

Tactic:
simp [ofFn_add, IH]

Premises used: List.ofFn_add
-- Module: Mathlib.Data.List.OfFn
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 := n) fun (i : Fin n) ↦ f (Fin.cast ⋯ (Fin.natAdd (m * n) i)))
    (ofFn (n := n) fun (j : Fin n) ↦ f ⟨m * n + (↑j : ℕ), ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.Data.List.OfFn
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 : ℕ), ⋯⟩)
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 : ℕ), ⋯⟩))
    (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 : ℕ), ⋯⟩)
⊢ ofFn f = flatten (ofFn (n := m) fun (i : Fin m) ↦ ofFn (n := n) fun (j : Fin n) ↦ f ⟨(↑i : ℕ) * n + (↑j : ℕ), ⋯⟩)

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

Premises used: List.ofFn_succ', List.ofFn_add, Nat.zero_mul, List.ofFn_zero, Nat.succ_mul, Nat.zero, Nat.succ
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
rw : m * (↑i : ℕ) + m = m * (↑i : ℕ) + m * 1
rw₁ rw₂ : m * (↑i : ℕ) + m = m * (↑i : ℕ) + m
⊢ m * (↑i : ℕ) + m = m * ((↑i : ℕ) + 1)

Tactic:
rw [Nat.mul_add, Nat.mul_one]

Premises used: Nat.mul_one, Nat.mul_add
-- Module: Mathlib.Data.List.OfFn
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 : ℕ), ⋯⟩))
simp_rw₁ :
  Eq.{u + 1} (α := List α)
    (flatten
      (ofFn (n := n) fun (i : Fin n) ↦
        ofFn (n := m) fun (j : Fin m) ↦ f (Fin.cast ⋯ (⟨(↑i : ℕ) * m + (↑j : ℕ), ⋯⟩ : Fin (n * m)))))
    (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 : ℕ), ⋯⟩)

Tactic:
simp_rw [m.mul_comm, ofFn_mul, Fin.cast_mk]

Premises used: Nat.mul_comm, Fin.cast_mk, List.ofFn_mul
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
rw rw₁ : Eq.{u + 1} (α := List α) [] []
⊢ Eq.{u + 1} (α := List α) (ofFn (n := length.{u} (α := α) []) (get [])) []

Tactic:
rw [ofFn_zero]

Premises used: List.ofFn_zero
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
a : α
l : List α
rw : ((a :: l).get 0 :: ofFn (n := l.length) fun (i : Fin l.length) ↦ (a :: l).get i.succ) = a :: l
⊢ ofFn (a :: l).get = a :: l

Tactic:
rw [ofFn_succ]

Premises used: List.ofFn_succ
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
a : α
l : List α
e_tail : (ofFn (n := l.length) fun (i : Fin l.length) ↦ (a :: l).get i.succ) = l
⊢ ((a :: l).get 0 :: ofFn (n := l.length) fun (i : Fin l.length) ↦ (a :: l).get i.succ) = a :: l

Tactic:
congr
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
a : α
l : List α
⊢ (ofFn (n := l.length) fun (i : Fin l.length) ↦ (a :: l).get i.succ) = l

Tactic:
ofFn_get l

Premises used: List.get
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
a : α
l : List α
⊢ (ofFn (n := l.length) fun (i : Fin l.length) ↦ (a :: l).get i.succ) = l

Tactic:
exact ofFn_get l
-- Module: Mathlib.Data.List.OfFn
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
rw₂ rw₃ : map f l = 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

Tactic:
rw [← Function.comp_def, ← map_ofFn, ofFn_getElem]

Premises used: List.map_ofFn, Function.comp_def, List.ofFn_getElem
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ a ∈ Set.range f

Tactic:
grind
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
P : α → Prop
⊢ (∀ (i : α), i ∈ ofFn f → P i) ↔ ∀ (j : Fin n), P (f j)

Tactic:
simp
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
c : α
rw : [] = replicate 0 c
rw₁ rw₂ : Eq.{u + 1} (α := List α) [] []
⊢ (ofFn (n := 0) fun (x : Fin 0) ↦ c) = replicate 0 c

Tactic:
rw [ofFn_zero, replicate_zero]

Premises used: List.replicate_zero, List.ofFn_zero
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
c : α
rw : (ofFn (n := n + 1) fun (x : Fin (n + 1)) ↦ c) = c :: ofFn (n := n) fun (x : Fin n) ↦ c
⊢ (ofFn (n := n + 1) fun (x : Fin (n + 1)) ↦ c) = replicate (n + 1) c

Tactic:
rw [replicate, ← ofFn_const n]

Premises used: List.replicate
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
c : α
⊢ (ofFn (n := n + 1) fun (x : Fin (n + 1)) ↦ c) = c :: ofFn (n := n) fun (x : Fin n) ↦ c

Tactic:
simp
-- Module: Mathlib.Data.List.OfFn
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))
simp_rw₅ :
  Eq.{u + 1} (α := List α)
    (flatten (ofFn (n := n) fun (i : Fin n) ↦ ofFn (n := m) fun (j : Fin m) ↦ a ⟨(↑j : ℕ) % m, ⋯⟩))
    (flatten (ofFn (n := n) fun (x : Fin n) ↦ ofFn a))
⊢ ofFn (Fin.repeat n a) = (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 _)]

Premises used: Fin.repeat, Fin.is_lt, Fin.modNat, Nat.mod_eq_of_lt, List.ofFn_const, Nat.add_mul_mod_self_right, List.ofFn_mul, Nat.add_comm
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
R : α → α → Prop
n : ℕ
f : Fin n → α
⊢ Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)

Tactic:
simp only [pairwise_iff_getElem, length_ofFn, List.getElem_ofFn,
    Fin.forall_iff,
    Fin.mk_lt_mk, forall_comm (α := (_ : Prop)) (β := ℕ)]

Premises used: Fin.mk_lt_mk, List.length_ofFn, forall_comm, List.pairwise_iff_getElem, Fin.forall_iff, List.getElem_ofFn
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).getLast ⋯ = f (Fin.last n)

Tactic:
getLast_ofFn _

Premises used: List.getLast_ofFn, Nat.pred
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
a : α
f : Fin n → α
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
⊢ ofFn (n := n + 1) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ α) a f) = a :: ofFn f

Tactic:
rw [ofFn_succ]

Premises used: List.ofFn_succ
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ (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:
rfl
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
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 ⋯)) = true) ↔
    p b = true ∧ ∃ (i : Fin n), f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
⊢ find? p (ofFn f) = some b ↔ 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]

Premises used: List.find?_eq_some_iff_getElem
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
h_1 :
  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 ⋯)) = true
hpb : p b = true
i : ℕ
hi : i < (ofFn f).length
hfb : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) i hi = b
h : ∀ (j : ℕ) (hj : j < i), (!p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) j ⋯)) = true
⊢ f (⟨i, ⋯⟩ : Fin n) = b

Tactic:
simpa using hfb
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
h_1 :
  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 ⋯)) = true
hpb : p b = true
i : ℕ
hi : i < (ofFn f).length
hfb : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) i hi = b
h : ∀ (j : ℕ) (hj : j < i), (!p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) j ⋯)) = true
j : Fin n
hj : j < ⟨i, ⋯⟩
⊢ ¬p (f j) = true

Tactic:
simpa using h j hj

Premises used: Fin.val
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
h_1 : p b = true ∧ ∃ (i : Fin n), f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) (↑i : ℕ) ⋯ = b

Tactic:
simpa using hfb
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
h_1 : p b = true ∧ ∃ (i : Fin n), f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
j : ℕ
hj : j < (↑i : ℕ)
⊢ j < n

Tactic:
lia
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
h_1 : p b = true ∧ ∃ (i : Fin n), f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
j : ℕ
hj : j < (↑i : ℕ)
⊢ (⟨j, ⋯⟩ : Fin n) < i

Tactic:
simpa using hj
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
h_1 : p b = true ∧ ∃ (i : Fin n), f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
j : ℕ
hj : j < (↑i : ℕ)
⊢ (!p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) j ⋯)) = true

Tactic:
simpa using h ⟨j, by lia⟩ (by simpa using hj)

Premises used: Fin.mk
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
⊢ (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 ⋯)) = true) ↔
    p b = true ∧ ∃ (i : Fin n), f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true

Tactic:
exact ⟨fun ⟨hpb, i, hi, hfb, h⟩ ↦
      ⟨hpb, ⟨⟨i, length_ofFn (f := f) ▸ hi⟩, by simpa using hfb, fun j hj ↦ by simpa using h j hj⟩⟩,
    fun ⟨hpb, i, hfb, h⟩ ↦
      ⟨hpb, ⟨i, (length_ofFn (f := f)).symm ▸ i.isLt, by simpa using hfb,
        fun j hj ↦ by simpa using h ⟨j, by lia⟩ (by simpa using hj)⟩⟩⟩
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
i : Fin n
h : Function.Injective f
⊢ find? p (ofFn f) = some (f i) ↔ p (f i) = true ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true

Tactic:
simp only [find?_ofFn_eq_some, h.eq_iff, Bool.not_eq_true, exists_eq_left]

Premises used: Function.Injective.eq_iff, exists_eq_left, List.find?_ofFn_eq_some, Bool.not_eq_true
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
⊢ ofFnRec (C := C) h (ofFn f) = h n f

Tactic:
equivSigmaTuple.rightInverse_symm.cast_eq (fun s => h s.1 s.2) ⟨n, f⟩

Premises used: List.equivSigmaTuple, List.ofFn, Sigma.fst, Function.LeftInverse.cast_eq, Sigma.mk, Sigma.snd, Equiv.rightInverse_symm, List.ofFnRec
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
P : List α → Prop
⊢ (∃ (l : List α), P l) ↔ ∃ (n : ℕ), ∃ (f : Fin n → α), P (ofFn f)

Tactic:
equivSigmaTuple.symm.surjective.exists.trans Sigma.exists

Premises used: Function.Surjective.exists, Sigma.exists, List.equivSigmaTuple, Iff.trans, Equiv.surjective, Equiv.symm
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
P : List α → Prop
⊢ (∀ (l : List α), P l) ↔ ∀ (n : ℕ) (f : Fin n → α), P (ofFn f)

Tactic:
equivSigmaTuple.symm.surjective.forall.trans Sigma.forall

Premises used: Function.Surjective.forall, List.equivSigmaTuple, Sigma.forall, Iff.trans, Equiv.surjective, Equiv.symm
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
m n : ℕ
f : Fin m → α
g : Fin n → α
⊢ ofFn f = ofFn g ↔
    Eq.{u + 1} (α := (n : ℕ) × (Fin n → α)) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → α) m f)
      (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → α) n g)

Tactic:
Iff.symm <| equivSigmaTuple.symm.injective.eq_iff.symm

Premises used: List.equivSigmaTuple, Function.Injective.eq_iff, Equiv.injective, Equiv.symm, Iff.symm
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f g : Fin n → α
h : ofFn f = ofFn g
⊢ 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

Premises used: List.ofFn_inj'
-- Module: Mathlib.Data.List.OfFn
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)
refl : f ≍ f
⊢ f ≍ g

Tactic:
cases h
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
⊢ f ≍ f

Tactic:
rfl
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f g : Fin n → α
⊢ ofFn f = ofFn g ↔ f = g

Tactic:
ofFn_injective.eq_iff

Premises used: Function.Injective.eq_iff, List.ofFn_injective
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List (α × α)) (offDiag []) []

Tactic:
rfl

Premises used: List.offDiag, rfl, List.flatten
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
a : α
l : List α
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
⊢ (a :: l).offDiag ~
    HAppend.hAppend (α := List (α × α)) (map (fun (x : α) ↦ (a, x)) l) (map (fun (x : α) ↦ (x, a)) l) ++ l.offDiag

Tactic:
simp only [offDiag, zipIdx_cons']

Premises used: List.offDiag, List.zipIdx_cons'
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
a : α
l : List α
rw : map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx
| map (fun (x : α) ↦ (x, a)) l

Tactic:
rw [← zipIdx_map_fst 0 l, map_map, Function.comp_def]

Premises used: List.map_map, Function.comp_def, List.zipIdx_map_fst, OfNat.ofNat
-- Module: Mathlib.Data.List.OffDiag
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)
conv_rhs₁ :
  Eq (α := List (α × α)) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx)
⊢ 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]

Premises used: List.map_map, Function.comp_def, List.zipIdx_map_fst, OfNat.ofNat
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
a : α
l : List α
⊢ 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]
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
a : α
l : List α
this : Eq (α := List (α × α)) (map (fun (x : α × ℕ) ↦ (x.fst, a)) l.zipIdx) (map (fun (x : α) ↦ (x, a)) l)
⊢ 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 [append_assoc, perm_append_left_iff, flatMap_map,
    ← (map_append_flatMap_perm _ _ _).congr_left, this]

Premises used: List.append_assoc, List.flatMap_map, List.Perm.congr_left, List.perm_append_left_iff, List.map_append_flatMap_perm
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
a : α
⊢ [a].offDiag = []

Tactic:
rfl

Premises used: List.offDiag, List.append, rfl, List.flatten
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
⊢ ∀ (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
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
this : ∀ (x : α × ℕ), x ∈ l.zipIdx → (l.eraseIdx x.snd).length = l.length - 1
⊢ l.offDiag.length = l.length * (l.length - 1)

Tactic:
simp [offDiag, map_congr_left this]

Premises used: List.map_congr_left, List.offDiag
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
⊢ l.offDiag.length = HPow.hPow (β := ℕ) l.length 2 - l.length

Tactic:
simp [length_offDiag', Nat.mul_sub, Nat.pow_two]

Premises used: List.length_offDiag', Nat.pow_two, Nat.mul_sub
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
x : α × α
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
⊢ 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

Tactic:
rcases x with ⟨x, y⟩