awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j i₁ : Fin (n + 1)
x :
  Eq.{u_3} (α := α) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a f i.rev.rev : α)
    (i.rev.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a (f ∘ rev) i.rev)
⊢ Eq.{u_3} (α := α) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a f j.rev : α)
    (i.rev.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a (f ∘ rev) j : α)
have p : ∀ (j : Fin n),
  Eq.{u_3} (α := α) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a f (i.rev.succAbove j).rev : α)
    (i.rev.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a (f ∘ rev) (i.rev.succAbove j))
Tactic: induction j using Fin.succAboveCases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x : α
p : Fin n → α
⊢ Eq.{u_3} (α := Fin (n + 1) → α) (i.insertNth (α := fun (a : Fin (n + 1)) ↦ α) x p ∘ rev)
    (i.rev.insertNth (α := fun (j : Fin (n + 1)) ↦ α) x (p ∘ rev))
have h : ∀ (x_1 : Fin (n + 1)),
  Eq.{u_3} (α := α) ((i.insertNth (α := fun (a : Fin (n + 1)) ↦ α) x p ∘ rev) x_1 : α)
    (i.rev.insertNth (α := fun (j : Fin (n + 1)) ↦ α) x (p ∘ rev) x_1 : α)
Tactic: funext x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ Eq.{u_3} (α := (j : Fin (n + 1 + 1)) → α)
    (i.succ.insertNth (α := fun (a : Fin (n + 2)) ↦ α) x (cons (α := fun (j : Fin (n + 1)) ↦ α) a p))
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p))
have h : ∀ (j : Fin (n + 1 + 1)),
  Eq.{u_3} (α := α)
    (i.succ.insertNth (α := fun (a : Fin (n + 2)) ↦ α) x (cons (α := fun (j : Fin (n + 1)) ↦ α) a p) j : α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p) j)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1)
⊢ Eq.{u_3} (α := α)
    (i.succ.insertNth (α := fun (a : Fin (n + 2)) ↦ α) x (cons (α := fun (j : Fin (n + 1)) ↦ α) a p)
        (i.succ.succAbove j) :
      α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p)
      (i.succ.succAbove j))
have h : Eq.{u_3} (α := α) (cons (α := fun (j : Fin (n + 1)) ↦ α) a p j : α)
  (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p) (i.succ.succAbove j))
Tactic: simp only [insertNth_apply_succAbove]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1)
⊢ Eq.{u_3} (α := α) (cons (α := fun (j : Fin (n + 1)) ↦ α) a p j : α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p)
      (i.succ.succAbove j))
have h : Eq.{u_3} (α := α) (cons (α := fun (j : Fin (n + 1)) ↦ α) a p 0 : α)
  (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p) (i.succ.succAbove 0) :
    α)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1)
h :
  Eq.{u_3} (α := α) (cons (α := fun (j : Fin (n + 1)) ↦ α) a p 0 : α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p)
        (i.succ.succAbove 0) :
      α)
⊢ Eq.{u_3} (α := α) (cons (α := fun (j : Fin (n + 1)) ↦ α) a p j : α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p)
      (i.succ.succAbove j))
have h₁ : ∀ (i_1 : Fin n),
  Eq.{u_3} (α := α) (cons (α := fun (j : Fin (n + 1)) ↦ α) a p i_1.succ : α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p)
        (i.succ.succAbove i_1.succ) :
      α)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1 + 1)
⊢ Eq.{u_3} (α := α)
    (i.succ.insertNth (α := fun (a : Fin (n + 2)) ↦ α) x (cons (α := fun (j : Fin (n + 1)) ↦ α) a p) j : α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p) j)
have h : Eq.{u_3} (α := α)
  (i.succ.insertNth (α := fun (a : Fin (n + 2)) ↦ α) x (cons (α := fun (j : Fin (n + 1)) ↦ α) a p) i.succ : α)
  (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p) i.succ)
Tactic: cases j using Fin.succAboveCases i.succ with
  | x => simp
  | p j =>
    simp only [insertNth_apply_succAbove]
    cases j using Fin.cases <;> simp
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1 + 1)
h :
  Eq.{u_3} (α := α)
    (i.succ.insertNth (α := fun (a : Fin (n + 2)) ↦ α) x (cons (α := fun (j : Fin (n + 1)) ↦ α) a p) i.succ : α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p) i.succ)
⊢ Eq.{u_3} (α := α)
    (i.succ.insertNth (α := fun (a : Fin (n + 2)) ↦ α) x (cons (α := fun (j : Fin (n + 1)) ↦ α) a p) j : α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p) j)
have h₁ : ∀ (j : Fin (n + 1)),
  Eq.{u_3} (α := α)
    (i.succ.insertNth (α := fun (a : Fin (n + 2)) ↦ α) x (cons (α := fun (j : Fin (n + 1)) ↦ α) a p)
        (i.succ.succAbove j) :
      α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p)
      (i.succ.succAbove j))
Tactic: cases j using Fin.succAboveCases i.succ with
  | x => simp
  | p j =>
    simp only [insertNth_apply_succAbove]
    cases j using Fin.cases <;> simp
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
⊢ Eq.{u_3} (α := Fin (n + 1) → α) (cons (α := fun (a : Fin (n + 1)) ↦ α) a f ∘ rev)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ rev) a)
have h : ∀ (i : Fin (n + 1)),
  Eq.{u_3} (α := α) ((cons (α := fun (a : Fin (n + 1)) ↦ α) a f ∘ rev) i : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ rev) a i : α)
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth (α := α) x p i) (i.insertNth (α := α) y q i) ∧
    Eq.{u_1} (α := (i_1 : Fin n) → α (i.succAbove i_1)) (fun (j : Fin n) ↦ op (i.succAbove j) (p j) (q j))
      (i.removeNth (α := α) fun (j : Fin (n + 1)) ↦ op j (i.insertNth (α := α) x p j) (i.insertNth (α := α) y q j))
have unfold : op i x y = op i (i.insertNth (α := α) x p i) (i.insertNth (α := α) y q i) ∧
  Eq.{u_1} (α := (i_1 : Fin n) → α (i.succAbove i_1)) (fun (j : Fin n) ↦ op (i.succAbove j) (p j) (q j))
    fun (i_1 : Fin n) ↦
    (fun (j : Fin (n + 1)) ↦ op j (i.insertNth (α := α) x p j) (i.insertNth (α := α) y q j)) (i.succAbove i_1)
Tactic: unfold removeNth
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
⊢ p.removeNth (α := α) (update (β := α) f p x) = p.removeNth (α := α) f
have h : ∀ (i : Fin n), p.removeNth (α := α) (update (β := α) f p x) i = p.removeNth (α := α) f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
⊢ p.removeNth (α := α) (update (β := α) f (p.succAbove i) x) =
    update (β := fun (a : Fin n) ↦ α (p.succAbove a)) (p.removeNth (α := α) f) i x
have h : ∀ (j : Fin n),
  p.removeNth (α := α) (update (β := α) f (p.succAbove i) x) j =
    update (β := fun (a : Fin n) ↦ α (p.succAbove a)) (p.removeNth (α := α) f) i x j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
j : Fin n
⊢ p.removeNth (α := α) (update (β := α) f (p.succAbove i) x) j =
    update (β := fun (a : Fin n) ↦ α (p.succAbove a)) (p.removeNth (α := α) f) i x j
have h : ∀ (x : α (p.succAbove j)),
  p.removeNth (α := α) (update (β := α) f (p.succAbove j) x) j =
    update (β := fun (a : Fin n) ↦ α (p.succAbove a)) (p.removeNth (α := α) f) j x j
Tactic: rcases eq_or_ne j i with rfl | hne
Cleared hypotheses: i, x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
j : Fin n
h :
  ∀ (x : α (p.succAbove j)),
    p.removeNth (α := α) (update (β := α) f (p.succAbove j) x) j =
      update (β := fun (a : Fin n) ↦ α (p.succAbove a)) (p.removeNth (α := α) f) j x j
⊢ p.removeNth (α := α) (update (β := α) f (p.succAbove i) x) j =
    update (β := fun (a : Fin n) ↦ α (p.succAbove a)) (p.removeNth (α := α) f) i x j
have h₁ : ∀ (hne : j ≠ i),
  p.removeNth (α := α) (update (β := α) f (p.succAbove i) x) j =
    update (β := fun (a : Fin n) ↦ α (p.succAbove a)) (p.removeNth (α := α) f) i x j
Tactic: rcases eq_or_ne j i with rfl | hne
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
⊢ (fun (f : (i : Fin (n + 1)) → α i) ↦ (f p, p.removeNth (α := α) f))
      ((fun (f : α p × ((i : Fin n) → α (p.succAbove i))) ↦ p.insertNth (α := α) f.1 f.2) f) =
    f
have fst : ((fun (f : (i : Fin (n + 1)) → α i) ↦ (f p, p.removeNth (α := α) f))
      ((fun (f : α p × ((i : Fin n) → α (p.succAbove i))) ↦ p.insertNth (α := α) f.1 f.2) f)).1 =
  f.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
fst :
  ((fun (f : (i : Fin (n + 1)) → α i) ↦ (f p, p.removeNth (α := α) f))
        ((fun (f : α p × ((i : Fin n) → α (p.succAbove i))) ↦ p.insertNth (α := α) f.1 f.2) f)).1 =
    f.1
⊢ (fun (f : (i : Fin (n + 1)) → α i) ↦ (f p, p.removeNth (α := α) f))
      ((fun (f : α p × ((i : Fin n) → α (p.succAbove i))) ↦ p.insertNth (α := α) f.1 f.2) f) =
    f
have snd : ∀ (x : Fin n),
  ((fun (f : (i : Fin (n + 1)) → α i) ↦ (f p, p.removeNth (α := α) f))
          ((fun (f : α p × ((i : Fin n) → α (p.succAbove i))) ↦ p.insertNth (α := α) f.1 f.2) f)).2
      x =
    f.2 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Type u_3
⊢ Equiv.symm (insertNthEquiv α 0) = (consEquiv α).symm
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ Equiv.symm (insertNthEquiv α 0) = (consEquiv α).symm
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_3
⊢ 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)) → α))
have 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 :
      α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
⊢ 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)
have 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'
Tactic: apply Function.hfunext rfl
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
⊢ ∀ (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'
have 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'
Tactic: simp only [heq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ 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
have 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)))
Tactic: unfold removeNth
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ 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)))
have a : j.succAbove (i.succAbove k) = (j.succAbove i).succAbove ((i.predAbove j).succAbove k)
Tactic: apply congr_arg_heq
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ j.succAbove (i.succAbove k) = (j.succAbove i).succAbove ((i.predAbove j).succAbove k)
have a : j.succAbove (i.succAbove k) = j.succAbove (i.succAbove k)
Tactic: rw [succAbove_succAbove_succAbove_predAbove]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
have refine_1 : 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; ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ Fin.find p h = i ↔ p i ∧ ∀ (j : Fin n), j < i → ¬p j
have 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
Tactic: refine ⟨?_, fun ⟨hm, hlt⟩ => have := Fin.find_le_of_pos h hm; ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (k : ℕ), k < n ∧ p k
⊢ Nat.find (p := p) ⋯ = (↑(Fin.find (fun (x : Fin n) ↦ p (↑x : ℕ)) ⋯) : ℕ)
have rw : Nat.find (p := p) sorry = Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (h : n_1 < n), p (↑(⟨n_1, h⟩ : Fin n) : ℕ)) sorry
Tactic: rw [val_find]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (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) : ℕ)) ⋯
have this : 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
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
i : Fin n
⊢ i < Fin.find p h ↔ ∀ (m : Fin n), m ≤ i → ¬p m
have simp_rw : ¬Fin.find p h ≤ i ↔ ∀ (m : Fin n), m ≤ i → ¬p m
Tactic: simp_rw [← not_le, find_le_iff, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ i < Fin.find p h ↔ ∀ (m : Fin n), m ≤ i → ¬p m
have simp_rw₁ : (¬∃ (m : Fin n), m ≤ i ∧ p m) ↔ ∀ (m : Fin n), m ≤ i → ¬p m
Tactic: simp_rw [← not_le, find_le_iff, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ i < Fin.find p h ↔ ∀ (m : Fin n), m ≤ i → ¬p m
have simp_rw₂ : (∀ (x : Fin n), ¬(x ≤ i ∧ p x)) ↔ ∀ (m : Fin n), m ≤ i → ¬p m
Tactic: simp_rw [← not_le, find_le_iff, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (k : Fin n), p k
i : Fin n
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m
have simp_rw : ¬Fin.find p h < i ↔ ∀ (m : Fin n), m < i → ¬p m
Tactic: simp_rw [← not_lt, find_lt_iff, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m
have simp_rw₁ : (¬∃ (m : Fin n), m < i ∧ p m) ↔ ∀ (m : Fin n), m < i → ¬p m
Tactic: simp_rw [← not_lt, find_lt_iff, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m
have simp_rw₂ : (∀ (x : Fin n), ¬(x < i ∧ p x)) ↔ ∀ (m : Fin n), m < i → ¬p m
Tactic: simp_rw [← not_lt, find_lt_iff, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (i : Fin (n + 1)), p i
h0 : ¬p 0
⊢ Fin.find p h = (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ
have simp_rw : p (Fin.find (fun (k : Fin n) ↦ p k.succ) sorry).succ ∧
  ∀ (i : Fin n), i < Fin.find (fun (k : Fin n) ↦ p k.succ) sorry → ¬p i.succ
Tactic: simp_rw [find_eq_iff, forall_fin_succ, h0, not_false_eq_true,
    implies_true, true_and, succ_lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ∃ (i : Fin (n + 1)), p i
⊢ Fin.find p h = if h0 : p 0 then 0 else (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ
have pos : p 0 → Fin.find p h = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ Fin.find p h = if h0 : p 0 then 0 else (Fin.find (fun (k : Fin n) ↦ p k.succ) ⋯).succ
have neg : ∀ (h_1 : ¬p 0), Fin.find p h = (Fin.find (fun (k : Fin n) ↦ p k.succ) sorry).succ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
m n : ℕ
p : Fin (m + n) → Prop
inst : DecidablePred p
hᵢ : ∃ (i : Fin (m + n)), p i
hm : m ≤ (↑(Fin.find p hᵢ) : ℕ)
⊢ Fin.find p hᵢ = natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) ⋯)
have 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]⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)) ⋯)
have refine : ∀ (i : Fin (m + n)) (hi : i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) sorry)), ¬p i
Tactic: refine (find_eq_iff _).2 ⟨Fin.find_spec hⱼ, fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)) ⋯)
⊢ ¬p i
have left : ∀ (i : Fin m) (hi : castAdd n i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) sorry)), ¬p (castAdd n i)
Tactic: cases i using addCases with | left i => _ | right i => _
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
⊢ ¬p i
have right : ∀ (i : Fin n) (hi : natAdd m i < natAdd m (Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) sorry)), ¬p (natAdd m i)
Tactic: cases i using addCases with | left i => _ | right i => _
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
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)
have hi₁ : i < Fin.find (fun (j : Fin n) ↦ p (natAdd m j)) sorry
Tactic: rw [Fin.natAdd_lt_natAdd_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : Fin n → Bool
⊢ find? p = if h : ∃ (i : Fin n), p i = true then some (Fin.find (fun (x : Fin n) ↦ p x = true) h) else none
have pos : ∀ (h : ∃ (i : Fin n), p i = true), find? p = some (Fin.find (fun (x : Fin n) ↦ p x = true) h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
⊢ find? p = if h : ∃ (i : Fin n), p i = true then some (Fin.find (fun (x : Fin n) ↦ p x = true) h) else none
have neg : (¬∃ (i : Fin n), p i = true) → find? p = none
Tactic: split_ifs