awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Type u_3
H :
  ∀ (x : (i : Fin (n + 1)) → α i),
    Eq.{u_3 + 1} (α := α 0)
      ((Equiv.symm (insertNthEquiv α 0) : (a : (i : Fin (n + 1)) → α i) → α 0 × ((i : Fin n) → α (succAbove 0 i))) x).1
      (((consEquiv α).symm : (a : (i : Fin (n + 1)) → α i) → α 0 × ((i : Fin n) → α (succAbove 0 i))) x).1
H₁ :
  ∀ (x : (i : Fin (n + 1)) → α i) (x_1 : Fin n),
    Eq.{u_3 + 1} (α := α (succAbove 0 x_1))
      (((Equiv.symm (insertNthEquiv α 0) : (a : (i : Fin (n + 1)) → α i) → α 0 × ((i : Fin n) → α (succAbove 0 i))) x).2
        x_1)
      ((((consEquiv α).symm : (a : (i : Fin (n + 1)) → α i) → α 0 × ((i : Fin n) → α (succAbove 0 i))) x).2 x_1)
⊢ Equiv.symm (insertNthEquiv α 0) = (consEquiv α).symm

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Type u_3
x : (i : Fin (n + 1)) → α i
⊢ Eq.{u_3 + 1} (α := α 0)
    ((Equiv.symm (insertNthEquiv α 0) : (a : (i : Fin (n + 1)) → α i) → α 0 × ((i : Fin n) → α (succAbove 0 i))) x).1
    (((consEquiv α).symm : (a : (i : Fin (n + 1)) → α i) → α 0 × ((i : Fin n) → α (succAbove 0 i))) x).1

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Type u_3
x : (i : Fin (n + 1)) → α i
x_1 : Fin n
⊢ Eq.{u_3 + 1} (α := α (succAbove 0 x_1))
    (((Equiv.symm (insertNthEquiv α 0) : (a : (i : Fin (n + 1)) → α i) → α 0 × ((i : Fin n) → α (succAbove 0 i))) x).2
      x_1)
    ((((consEquiv α).symm : (a : (i : Fin (n + 1)) → α i) → α 0 × ((i : Fin n) → α (succAbove 0 i))) x).2 x_1)

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_3
H :
  ∀ (x : α × ((i : Fin n) → α)) (x_1 : Fin (n + 1)),
    Eq (α := α)
      (((insertNthEquiv.{u_3} (fun (x : Fin (n + 1)) ↦ α) (last n) : α × ((i : Fin n) → α) ≃ ((i : Fin (n + 1)) → α)) :
            (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
          x x_1 :
        α)
      (((snocEquiv.{u_3} (n := n) fun (x : Fin (n + 1)) ↦ α : α × ((i : Fin n) → α) ≃ ((i : Fin (n + 1)) → α)) :
            (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
          x x_1 :
        α)
⊢ Eq.{u_3 + 1} (α := α × ((i : Fin n) → α) ≃ ((i : Fin (n + 1)) → α))
    (insertNthEquiv.{u_3} (fun (x : Fin (n + 1)) ↦ α) (last n) : α × ((i : Fin n) → α) ≃ ((i : Fin (n + 1)) → α))
    (snocEquiv.{u_3} (n := n) fun (x : Fin (n + 1)) ↦ α : α × ((i : Fin n) → α) ≃ ((i : Fin (n + 1)) → α))

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_3
x : α × ((i : Fin n) → α)
x_1 : Fin (n + 1)
⊢ Eq (α := α)
    (((insertNthEquiv.{u_3} (fun (x : Fin (n + 1)) ↦ α) (last n) : α × ((i : Fin n) → α) ≃ ((i : Fin (n + 1)) → α)) :
          (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
        x x_1 :
      α)
    (((snocEquiv.{u_3} (n := n) fun (x : Fin (n + 1)) ↦ α : α × ((i : Fin n) → α) ≃ ((i : Fin (n + 1)) → α)) :
          (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
        x x_1 :
      α)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
apply :
  ∀ (a a' : Fin n),
    a ≍ a' →
      i.removeNth (α := fun (i : Fin (n + 1)) ↦ α (j.succAbove i)) (j.removeNth (α := α) m) a ≍
        (i.predAbove j).removeNth (α := fun (i_1 : Fin (n + 1)) ↦ α ((j.succAbove i).succAbove i_1))
          ((j.succAbove i).removeNth (α := α) m) a'
⊢ i.removeNth (α := fun (i : Fin (n + 1)) ↦ α (j.succAbove i)) (j.removeNth (α := α) m) ≍
    (i.predAbove j).removeNth (α := fun (i_1 : Fin (n + 1)) ↦ α ((j.succAbove i).succAbove i_1))
      ((j.succAbove i).removeNth (α := α) m)

Tactic:
apply Function.hfunext rfl

Premises used: Function.hfunext, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
simp :
  ∀ (a a' : Fin n),
    a = a' →
      i.removeNth (α := fun (i : Fin (n + 1)) ↦ α (j.succAbove i)) (j.removeNth (α := α) m) a ≍
        (i.predAbove j).removeNth (α := fun (i_1 : Fin (n + 1)) ↦ α ((j.succAbove i).succAbove i_1))
          ((j.succAbove i).removeNth (α := α) m) a'
⊢ ∀ (a a' : Fin n),
    a ≍ a' →
      i.removeNth (α := fun (i : Fin (n + 1)) ↦ α (j.succAbove i)) (j.removeNth (α := α) m) a ≍
        (i.predAbove j).removeNth (α := fun (i_1 : Fin (n + 1)) ↦ α ((j.succAbove i).succAbove i_1))
          ((j.succAbove i).removeNth (α := α) m) a'

Tactic:
simp only [heq_iff_eq]

Premises used: heq_iff_eq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
unfold :
  HEq (α := α (j.succAbove (i.succAbove k))) (m (j.succAbove (i.succAbove k))) (β :=
    α ((j.succAbove i).succAbove ((i.predAbove j).succAbove k)))
    (m ((j.succAbove i).succAbove ((i.predAbove j).succAbove k)))
⊢ i.removeNth (α := fun (i : Fin (n + 1)) ↦ α (j.succAbove i)) (j.removeNth (α := α) m) k ≍
    (i.predAbove j).removeNth (α := fun (i_1 : Fin (n + 1)) ↦ α ((j.succAbove i).succAbove i_1))
      ((j.succAbove i).removeNth (α := α) m) k

Tactic:
unfold removeNth

Premises used: Fin.removeNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
a : j.succAbove (i.succAbove k) = (j.succAbove i).succAbove ((i.predAbove j).succAbove k)
⊢ HEq (α := α (j.succAbove (i.succAbove k))) (m (j.succAbove (i.succAbove k))) (β :=
    α ((j.succAbove i).succAbove ((i.predAbove j).succAbove k)))
    (m ((j.succAbove i).succAbove ((i.predAbove j).succAbove k)))

Tactic:
apply congr_arg_heq

Premises used: congr_arg_heq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
a a₁ : j.succAbove (i.succAbove k) = j.succAbove (i.succAbove k)
⊢ j.succAbove (i.succAbove k) = (j.succAbove i).succAbove ((i.predAbove j).succAbove k)

Tactic:
rw [succAbove_succAbove_succAbove_predAbove]

Premises used: Fin.succAbove_succAbove_succAbove_predAbove
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
m : Fin (n + 2) → α
i : Fin (n + 1)
j : Fin (n + 2)
⊢ i.removeNth (α := fun (i : Fin (n + 1)) ↦ α) (j.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ α) m) =
    (i.predAbove j).removeNth (α := fun (i : Fin (n + 1)) ↦ α)
      ((j.succAbove i).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ α) m)

Tactic:
heq_iff_eq.mp (removeNth_removeNth_heq_swap m i j)

Premises used: heq_iff_eq, Fin.removeNth_removeNth_heq_swap, Iff.mp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m_1 n_1 : ℕ
p_1 q : Fin n_1 → Prop
inst : DecidablePred p_1
inst_1 : DecidablePred q
i j_1 : Fin n_1
n : ℕ
p : Fin n → Prop
inst_2 : DecidablePred p
h : ∃ (k : Fin n), p k
m j : ℕ
hm : j < n - m
⊢ j < n

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m_1 n_1 : ℕ
p_1 q : Fin n_1 → Prop
inst : DecidablePred p_1
inst_1 : DecidablePred q
i j : Fin n_1
n : ℕ
p : Fin n → Prop
inst_2 : DecidablePred p
h : ∃ (k : Fin n), p k
m_2 m : ℕ
hj : ∀ (j : ℕ) (hm : j < n - (m + 1)), ¬p ⟨j, ⋯⟩
⊢ 0 < m + 1

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m_1 n_1 : ℕ
p_1 q : Fin n_1 → Prop
inst : DecidablePred p_1
inst_1 : DecidablePred q
i j : Fin n_1
n : ℕ
p : Fin n → Prop
inst_2 : DecidablePred p
h : ∃ (k : Fin n), p k
m_2 m : ℕ
hj : ∀ (j : ℕ) (hm : j < n - (m + 1)), ¬p ⟨j, ⋯⟩
hnm : ¬p ⟨n - (m + 1), ⋯⟩
⊢ ∀ (j : ℕ) (hm : j < n - m), ¬p ⟨j, ⋯⟩

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m_1 n_1 : ℕ
p_1 q : Fin n_1 → Prop
inst : DecidablePred p_1
inst_1 : DecidablePred q
i j : Fin n_1
n : ℕ
p : Fin n → Prop
inst_2 : DecidablePred p
h : ∃ (k : Fin n), p k
m : ℕ
hj : ∀ (j : ℕ) (hm : j < n - 0), ¬p ⟨j, ⋯⟩
h_1 : ∃ (k : Fin n), p k
val : ℕ
isLt : val < n
h_2 : p ⟨val, isLt⟩
⊢ False

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n_1 : ℕ
p_1 q : Fin n_1 → Prop
inst : DecidablePred p_1
inst_1 : DecidablePred q
i j : Fin n_1
n : ℕ
p : Fin n → Prop
inst_2 : DecidablePred p
h : ∃ (k : Fin n), p k
⊢ ∀ (j : ℕ) (hm : j < n - n), ¬p ⟨j, ⋯⟩

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
⊢ p (Fin.find p h)

Tactic:
(Fin.findX p h).2.1

Premises used: And.left, Fin.find, Subtype.property, _private.0.Fin.findX
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
⊢ ∀ {j : Fin n}, j < Fin.find p h → ¬p j

Tactic:
@(Fin.findX p h).2.2

Premises used: And.right, Subtype.property, _private.0.Fin.findX
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
j : Fin n
⊢ p j → Fin.find p h ≤ j

Tactic:
(j.find_min _ <| lt_of_not_ge ·).mtr

Premises used: lt_of_not_ge, Function.mtr, Fin.find_min
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
i : Fin n
h : ∃ (k : Fin n), p k
⊢ Fin.find p h = i ↔ p i ∧ ∀ (j : Fin n), j < i → ¬p j

Tactic:
⟨?_, fun ⟨hm, hlt⟩ => have := Fin.find_le_of_pos h hm; ?_⟩

Premises used: _private.0.Fin.find_eq_iff.match_1, Fin.find_le_of_pos, Iff.intro, Fin.find, Eq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
i : Fin n
h : ∃ (k : Fin n), p k
refine_1 : Fin.find p h = i → p i ∧ ∀ (j : Fin n), j < i → ¬p j
refine_2 :
  (p i ∧ ∀ (j : Fin n), j < i → ¬p j) →
    ∀ (hm : p i) (hlt : ∀ (j : Fin n), j < i → ¬p j) (this : Fin.find p h ≤ i), Fin.find p h = i
⊢ Fin.find p h = i ↔ p i ∧ ∀ (j : Fin n), j < i → ¬p j

Tactic:
refine ⟨?_, fun ⟨hm, hlt⟩ => have := Fin.find_le_of_pos h hm; ?_⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
i : Fin n
h : ∃ (k : Fin n), p k
⊢ Fin.find p h = i → p i ∧ ∀ (j : Fin n), j < i → ¬p j

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
i : Fin n
h : ∃ (k : Fin n), p k
h_1 : p i ∧ ∀ (j : Fin n), j < i → ¬p j
hm : p i
hlt : ∀ (j : Fin n), j < i → ¬p j
this : Fin.find p h ≤ i
⊢ Fin.find p h = i

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
⊢ (↑(Fin.find p h) : ℕ) = Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (h : n_1 < n), p ⟨n_1, h⟩) ⋯

Tactic:
((Nat.find_eq_iff _).mpr ⟨⟨is_lt _, Fin.find_spec _⟩,
    fun _ hm ⟨_, hi⟩ => Fin.find_min h hm hi⟩).symm

Premises used: Iff.mpr, And.intro, Eq.symm, Nat.find_eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p_1 q : Fin n → Prop
inst : DecidablePred p_1
inst_1 : DecidablePred q
i j : Fin n
p : ℕ → Prop
inst_2 : DecidablePred p
h : ∃ (k : ℕ), k < n ∧ p k
⊢ ∃ (n : ℕ), p n

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p_1 q : Fin n → Prop
inst : DecidablePred p_1
inst_1 : DecidablePred q
i j : Fin n
p : ℕ → Prop
inst_2 : DecidablePred p
h : ∃ (k : ℕ), k < n ∧ p k
⊢ ∃ (i : ℕ), ∃ (h : i < n), p (↑(⟨i, h⟩ : Fin n) : ℕ)

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (k : ℕ), k < n ∧ p k
rw : Nat.find (p := p) ⋯ = Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (h : n_1 < n), p (↑(⟨n_1, h⟩ : Fin n) : ℕ)) ⋯
⊢ Nat.find (p := p) ⋯ = (↑(Fin.find (fun (x : Fin n) ↦ p (↑x : ℕ)) ⋯) : ℕ)

Tactic:
rw [val_find]

Premises used: Fin.val_find
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (k : ℕ), k < n ∧ p k
⊢ h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k) < n ∧ p (h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k))

Tactic:
have := h.choose_spec
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (k : ℕ), k < n ∧ p k
this : h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k) < n ∧ p (h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k))
⊢ p (h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k))

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (k : ℕ), k < n ∧ p k
this : h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k) < n ∧ p (h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k))
⊢ ∀ (n_1 : ℕ), n_1 ≤ h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k) → (p n_1 ↔ ∃ (h : n_1 < n), p (↑(⟨n_1, h⟩ : Fin n) : ℕ))

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (k : ℕ), k < n ∧ p k
this : h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k) < n ∧ p (h.choose (p := fun (k : ℕ) ↦ k < n ∧ p k))
⊢ Nat.find (p := p) ⋯ = Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (h : n_1 < n), p (↑(⟨n_1, h⟩ : Fin n) : ℕ)) ⋯

Tactic:
exact Nat.find_congr (x := h.choose) (by grind) (by grind)

Premises used: Nat.find_congr
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
i : Fin n
⊢ Fin.find p h < i → ∃ (m : Fin n), m < i ∧ p m

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
i : Fin n
⊢ Fin.find p h ≤ i → ∃ (m : Fin n), m ≤ i ∧ p m

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
i : Fin n
simp_rw : ¬Fin.find p h ≤ i ↔ ∀ (m : Fin n), m ≤ i → ¬p m
simp_rw₁ : (¬∃ (m : Fin n), m ≤ i ∧ p m) ↔ ∀ (m : Fin n), m ≤ i → ¬p m
simp_rw₂ : (∀ (x : Fin n), ¬(x ≤ i ∧ p x)) ↔ ∀ (m : Fin n), m ≤ i → ¬p m
⊢ i < Fin.find p h ↔ ∀ (m : Fin n), m ≤ i → ¬p m

Tactic:
simp_rw [← not_le, find_le_iff, not_exists, not_and]

Premises used: not_le, Fin.find_le_iff, not_exists, not_and
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
i : Fin n
simp_rw : ¬Fin.find p h < i ↔ ∀ (m : Fin n), m < i → ¬p m
simp_rw₁ : (¬∃ (m : Fin n), m < i ∧ p m) ↔ ∀ (m : Fin n), m < i → ¬p m
simp_rw₂ : (∀ (x : Fin n), ¬(x < i ∧ p x)) ↔ ∀ (m : Fin n), m < i → ¬p m
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m

Tactic:
simp_rw [← not_lt, find_lt_iff, not_exists, not_and]

Premises used: not_exists, not_lt, Fin.find_lt_iff, not_and
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (k : Fin (n + 1)), p k
⊢ Fin.find p h = 0 ↔ p 0

Tactic:
simp [find_eq_iff]

Premises used: Fin.find_eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (i : Fin (n + 1)), p i
h0 : ¬p 0
simp_rw :
  p (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ ∧
    ∀ (i : Fin n), i < Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯ → ¬p i.succ
⊢ Fin.find p h = (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ

Tactic:
simp_rw [find_eq_iff, forall_fin_succ, h0, not_false_eq_true,
    implies_true, true_and, succ_lt_succ_iff]

Premises used: Fin.find_eq_iff, Fin.succ_lt_succ_iff, Fin.forall_fin_succ, implies_true, not_false_eq_true, true_and
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (i : Fin (n + 1)), p i
h0 : ¬p 0
⊢ p (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ ∧
    ∀ (i : Fin n), i < Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯ → ¬p i.succ

Tactic:
⟨Fin.find_spec (p := fun i => p i.succ) _, fun j => Fin.find_min _⟩

Premises used: Or.resolve_left, Fin.find_spec, And.intro, Iff.mp, Fin.find_min, Fin.exists_fin_succ
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (i : Fin (n + 1)), p i
h0 : ¬p 0
⊢ p (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ ∧
    ∀ (i : Fin n), i < Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯ → ¬p i.succ

Tactic:
exact ⟨Fin.find_spec (p := fun i => p i.succ) _, fun j => Fin.find_min _⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (i : Fin (n + 1)), p i
pos : p 0 → Fin.find p h = 0
neg : ∀ (h_1 : ¬p 0), Fin.find p h = (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ
⊢ Fin.find p h = if h0 : p 0 then 0 else (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ

Tactic:
split_ifs
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (i : Fin (n + 1)), p i
h_1 : p 0
⊢ Fin.find p h = 0

Tactic:
grind [find_eq_zero]

Premises used: Fin.find_eq_zero
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (i : Fin (n + 1)), p i
h_1 : ¬p 0
⊢ Fin.find p h = (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ

Tactic:
grind [find_of_not_zero]

Premises used: Fin.find_of_not_zero
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p q : Fin n → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
i : Fin n
hi : q i
hpq : ∀ (j : Fin n), j ≤ i → q j → p j
⊢ Fin.find p ⋯ ≤ Fin.find q ⋯

Tactic:
Fin.find_le_of_pos _ (hpq _ (Fin.find_le_of_pos _ hi) (Fin.find_spec ⟨i, hi⟩))

Premises used: Fin.find_le_of_pos, Fin.find_spec, Exists.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p q : Fin n → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∀ (i : Fin n), q i → p i
hp : ∃ (i : Fin n), p i
hq : ∃ (i : Fin n), q i
⊢ Fin.find p hp ≤ Fin.find q hq

Tactic:
let ⟨_, hq⟩ := hq; find_mono_of_le hq fun _ _ ↦ h _

Premises used: Fin.find_mono_of_le, _private.0.Fin.find_mono.match_1, LE.le, Fin.find
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p q : Fin n → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
i : Fin n
hi : p i
hpq : ∀ (j : Fin n), j ≤ i → (p j ↔ q j)
⊢ Fin.find p ⋯ = Fin.find q ⋯

Tactic:
le_antisymm (find_mono_of_le (hpq _ le_rfl |>.1 hi) fun _ h ↦ (hpq _ h).mpr)
    (find_mono_of_le hi fun _ h ↦ (hpq _ h).mp)

Premises used: Iff.mpr, le_rfl, Fin.find_mono_of_le, le_antisymm, Iff.mp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p q : Fin n → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
hp : ∃ (i : Fin n), p i
hq : ∃ (i : Fin n), q i
hpq : ∀ {i : Fin n}, p i ↔ q i
⊢ Fin.find p hp = Fin.find q hq

Tactic:
let ⟨_, hp⟩ := hp; find_congr hp fun _ _ ↦ hpq

Premises used: _private.0.Fin.find_mono.match_1, Fin.find_congr, Fin.find, Eq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
i : Fin n
hi : p i
⊢ Fin.find p ⋯ ≤ i

Tactic:
(Fin.find_le_iff _ _).2 ⟨i, le_refl _, hi⟩

Premises used: Iff.mpr, le_refl, Fin.find_le_iff, And.intro, Exists.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (i : Fin (n + 1)), p i
⊢ 0 < Fin.find p h ↔ ¬p 0

Tactic:
Fin.pos_iff_ne_zero.trans (Fin.find_eq_zero _).not

Premises used: Fin.find_eq_zero, Iff.not, Fin.pos_iff_ne_zero, Iff.trans
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p_1 q : Fin n → Prop
inst : DecidablePred p_1
inst_1 : DecidablePred q
i j : Fin n
p : Fin (m + n) → Prop
inst_2 : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
⊢ (fun (j : Fin n) ↦ p (natAdd m j)) (subNat m (Fin.cast ⋯ (Fin.find p hᵢ)) hm)

Tactic:
simp [Fin.find_spec]

Premises used: Fin.find_spec
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
⊢ p (natAdd m (subNat m (Fin.cast ⋯ (Fin.find p hᵢ)) hm))

Tactic:
simp [Fin.find_spec]

Premises used: Fin.find_spec
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
⊢ ∃ (j : Fin n), p (natAdd m j)

Tactic:
have hⱼ : ∃ j : Fin n, p (j.natAdd m) :=
    ⟨(Fin.cast (Nat.add_comm _ _) (Fin.find p hᵢ)).subNat _ hm, by simp [Fin.find_spec]⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
⊢ Fin.find p hᵢ = natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)

Tactic:
(find_eq_iff _).2 ⟨Fin.find_spec hⱼ, fun i hi ↦ ?_⟩

Premises used: Iff.mpr, Fin.find_eq_iff, Fin.find_spec, And.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
refine : ∀ (i : Fin (m + n)) (hi : i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)), ¬p i
⊢ Fin.find p hᵢ = natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)

Tactic:
refine (find_eq_iff _).2 ⟨Fin.find_spec hⱼ, fun i hi ↦ ?_⟩

Premises used: Iff.mpr, Fin.find_eq_iff, Fin.find_spec, And.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
i : Fin m
hi : castAdd n i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)
⊢ ¬p (castAdd n i)

Tactic:
_
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
i : Fin n
hi : natAdd m i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)
⊢ ¬p (natAdd m i)

Tactic:
_
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
i : Fin (m + n)
hi : i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)
left : ∀ (i : Fin m) (hi : castAdd n i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)), ¬p (castAdd n i)
right : ∀ (i : Fin n) (hi : natAdd m i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)), ¬p (natAdd m i)
⊢ ¬p i

Tactic:
cases i using addCases with | left i => _ | right i => _
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
i : Fin m
hi : castAdd n i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)
⊢ ¬p (castAdd n i)

Tactic:
Fin.find_min hᵢ (Fin.lt_def.mpr <| (Fin.castAdd_lt _ _).trans_le hm)

Premises used: Iff.mpr, Fin.lt_def, LT.lt.trans_le, Fin.castAdd_lt, Fin.find_min
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
i : Fin m
hi : castAdd n i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)
⊢ ¬p (castAdd n i)

Tactic:
exact Fin.find_min hᵢ (Fin.lt_def.mpr <| (Fin.castAdd_lt _ _).trans_le hm)

Premises used: Iff.mpr, Fin.lt_def, LT.lt.trans_le, Fin.castAdd_lt, Fin.find_min
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
i : Fin n
hi : natAdd m i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)
⊢ i < Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯

Tactic:
rw [Fin.natAdd_lt_natAdd_iff] at hi

Premises used: Fin.natAdd_lt_natAdd_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
i : Fin n
hi : i < Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯
⊢ ¬p (natAdd m i)

Tactic:
Fin.find_min hⱼ hi

Premises used: Fin.find_min
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
hⱼ : ∃ (j : Fin n), p (natAdd m j)
i : Fin n
hi : i < Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯
⊢ ¬p (natAdd m i)

Tactic:
exact Fin.find_min hⱼ hi

Premises used: Fin.find_min
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Bool
pos : ∀ (h : ∃ (i : Fin n), p i = true), find? p = some (Fin.find (fun (x : Fin n) ↦ p x = true) h)
neg : (¬∃ (i : Fin n), p i = true) → find? p = none
⊢ find? p = if h : ∃ (i : Fin n), p i = true then some (Fin.find (fun (x : Fin n) ↦ p x = true) h) else none

Tactic:
split_ifs
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Bool
h : ∃ (i : Fin n), p i = true
⊢ find? p = some (Fin.find (fun (x : Fin n) ↦ p x = true) h)

Tactic:
grind
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Bool
h : ¬∃ (i : Fin n), p i = true
⊢ find? p = none

Tactic:
grind