awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (i.succAbove k)
rw :
  i.succAboveCases (α := fun (x : Fin (n + 1)) ↦ α x) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯
rw₁ :
  Eq.{u_1} (α := α j)
    (if hj : j = i then Eq.rec (motive := fun (x : Fin (n + 1)) (x_1 : i = x) ↦ α x) x ⋯
      else
        if hlt : j < i then
          Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
        else Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ :
      α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ : α j)
rw₂ :
  Eq.{u_1} (α := α j)
    (if hlt : j < i then
        Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
      else
        @Eq.rec _ (i.succAbove (j.pred ⋯)) (fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x)
          (p (j.pred ⋯) : α (i.succAbove (j.pred ⋯))) _ ⋯ :
      α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ : α j)
rw₃ rw₄ :
  Eq.{u_1} (α := α j)
    (@Eq.rec _ (i.succAbove (j.pred ⋯)) (fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x)
        (p (j.pred ⋯) : α (i.succAbove (j.pred ⋯))) _ ⋯ :
      α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ : α j)
⊢ i.insertNth (α := α) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯

Tactic:
rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]

Premises used: Fin.ne_of_gt, Fin.lt_asymm, Fin.insertNth, dif_neg
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ x = cons (α := α) x (fun (j : Fin n) ↦ cast ⋯ (p j)) 0

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
refine : p = removeNth (α := α) 0 (cons (α := α) x fun (j : Fin n) ↦ cast ⋯ (p j))
⊢ insertNth (α := α) 0 x p = cons (α := α) x fun (j : Fin n) ↦ cast ⋯ (p j)

Tactic:
refine insertNth_eq_iff.2 ⟨by simp, ?_⟩

Premises used: Iff.mpr, And.intro, Fin.insertNth_eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
h : ∀ (j : Fin n), p j = removeNth (α := α) 0 (cons (α := α) x fun (j : Fin n) ↦ cast ⋯ (p j)) j
⊢ p = removeNth (α := α) 0 (cons (α := α) x fun (j : Fin n) ↦ cast ⋯ (p j))

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
j : Fin n
⊢ p j = cons (α := α) x p j.succ

Tactic:
(cons_succ x p j).symm

Premises used: Fin.cons_succ, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
j : Fin n
⊢ p j = removeNth (α := α) 0 (cons (α := α) x fun (j : Fin n) ↦ cast ⋯ (p j)) j

Tactic:
convert! (cons_succ x p j).symm

Premises used: Fin.cons_succ, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ Eq.{u_2} (α := (j : Fin (n + 1)) → β) (insertNth (α := fun (x : Fin (n + 1)) ↦ β) 0 x p)
    (cons (α := fun (i : Fin (n + 1)) ↦ β) x p)

Tactic:
simp [insertNth_zero]

Premises used: Fin.insertNth_zero
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ x = snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x (last n)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
refine : p = (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x)
⊢ (last n).insertNth (α := α) x p = snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x

Tactic:
refine insertNth_eq_iff.2 ⟨by simp, ?_⟩

Premises used: Iff.mpr, And.intro, Fin.insertNth_eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
h : ∀ (j : Fin n), p j = (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j
⊢ p = (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x)

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
h : p j ≍ (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j
⊢ p j = (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j

Tactic:
apply eq_of_heq

Premises used: eq_of_heq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
trans : HEq (p j) (β := α j.castSucc) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x j.castSucc)
trans₁ :
  HEq (α := α j.castSucc) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x j.castSucc)
    ((last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j)
⊢ p j ≍ (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j

Tactic:
trans snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x j.castSucc

Premises used: Fin.succAbove_last_apply, cast, Fin.snoc, congr_arg, Fin.castSucc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
rw : p j ≍ cast ⋯ (p j)
⊢ HEq (p j) (β := α j.castSucc) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x j.castSucc)

Tactic:
rw [snoc_castSucc]

Premises used: Fin.snoc_castSucc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j ≍ cast ⋯ (p j)

Tactic:
(cast_heq _ _).symm

Premises used: HEq.symm, cast_heq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j ≍ cast ⋯ (p j)

Tactic:
exact (cast_heq _ _).symm

Premises used: HEq.symm, cast_heq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
a : j.castSucc = (last n).succAbove j
⊢ HEq (α := α j.castSucc) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x j.castSucc)
    ((last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j)

Tactic:
apply congr_arg_heq

Premises used: congr_arg_heq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
a a₁ : j.castSucc = j.castSucc
⊢ j.castSucc = (last n).succAbove j

Tactic:
rw [succAbove_last]

Premises used: Fin.succAbove_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ Eq.{u_2} (α := (j : Fin (n + 1)) → β) ((last n).insertNth (α := fun (x : Fin (n + 1)) ↦ β) x p)
    (snoc (α := fun (i : Fin (n + 1)) ↦ β) p x)

Tactic:
simp [insertNth_last]

Premises used: Fin.insertNth_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)
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))
⊢ 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 : α)

Tactic:
induction j using Fin.succAboveCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ Fin (n + 1)

Tactic:
exact rev i

Premises used: Fin.rev
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
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:
simp [rev_succAbove]

Premises used: Fin.rev_succAbove
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x : α
p : Fin n → α
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 : α)
⊢ 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))

Tactic:
funext x
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x_1 : α
p : Fin n → α
x : Fin (n + 1)
⊢ Eq.{u_3} (α := α) ((i.insertNth (α := fun (a : Fin (n + 1)) ↦ α) x_1 p ∘ rev) x : α)
    (i.rev.insertNth (α := fun (j : Fin (n + 1)) ↦ α) x_1 (p ∘ rev) x : α)

Tactic:
apply insertNth_rev

Premises used: Fin.insertNth_rev
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
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)
⊢ 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))

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ 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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
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 j : α)
    (cons (α := fun (i : Fin (n + 1 + 1)) ↦ α) a (i.insertNth (α := fun (i : Fin (n + 1)) ↦ α) x p)
      (i.succ.succAbove j))
⊢ 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:
simp only [insertNth_apply_succAbove]

Premises used: Fin.insertNth_apply_succAbove
-- Module: Mathlib.Data.Fin.Tuple.Basic
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) :
      α)
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) :
        α)
⊢ 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:
cases j using Fin.cases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ 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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)
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))
⊢ 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:
cases j using Fin.succAboveCases i.succ with
  | x => simp
  | p j =>
    simp only [insertNth_apply_succAbove]
    cases j using Fin.cases <;> simp

Premises used: Fin.insertNth_apply_succAbove
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ Eq.{u_3} (α := α) (cons (α := fun (x : Fin (n + 1)) ↦ α) a f i.rev : α)
    (snoc (α := fun (x : Fin (n + 1)) ↦ α) (f ∘ rev) a i)

Tactic:
simpa using insertNth_rev 0 a f i

Premises used: Fin.insertNth_rev, OfNat.ofNat
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
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 : α)
⊢ Eq.{u_3} (α := Fin (n + 1) → α) (cons (α := fun (a : Fin (n + 1)) ↦ α) a f ∘ rev)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ rev) a)

Tactic:
funext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
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:
cons_rev ..

Premises used: Fin.cons, Fin.induction, Fin.cases, Fin.cons_rev
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
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:
exact cons_rev ..

Premises used: Fin.cons_rev
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ Eq.{u_3} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) f a i.rev : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a (f ∘ rev) i : α)

Tactic:
simpa using insertNth_rev (last n) a f i

Premises used: Fin.insertNth_rev, Fin.last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
⊢ Eq.{u_3} (α := Fin (n + 1) → α) (snoc (α := fun (a : Fin (n + 1)) ↦ α) f a ∘ rev)
    (cons (α := fun (i : Fin (n + 1)) ↦ α) a (f ∘ rev))

Tactic:
funext <| snoc_rev a f

Premises used: funext, Fin.snoc_rev
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)
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)
⊢ 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))

Tactic:
unfold removeNth

Premises used: Fin.removeNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
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))
      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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Type u_3
inst : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ i.insertNth (α := α) x p ≤ q ↔ x ≤ q i ∧ p ≤ fun (j : Fin n) ↦ q (i.succAbove j)

Tactic:
simp [Pi.le_def, forall_iff_succAbove i]

Premises used: Pi.le_def, Fin.forall_iff_succAbove
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Type u_3
inst : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ q ≤ i.insertNth (α := α) x p ↔ q i ≤ x ∧ (fun (j : Fin n) ↦ q (i.succAbove j)) ≤ p

Tactic:
simp [Pi.le_def, forall_iff_succAbove i]

Premises used: Pi.le_def, Fin.forall_iff_succAbove
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
h : ∀ (i : Fin n), p.removeNth (α := α) (update (β := α) f p x) i = p.removeNth (α := α) f i
⊢ p.removeNth (α := α) (update (β := α) f p x) = p.removeNth (α := α) f

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
i : Fin n
⊢ p.removeNth (α := α) (update (β := α) f p x) i = p.removeNth (α := α) f i

Tactic:
simp [removeNth]

Premises used: Fin.removeNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ p.removeNth (α := α) (update (β := α) f (p.succAbove i) x) =
    update (β := fun (a : Fin n) ↦ α (p.succAbove a)) (p.removeNth (α := α) f) i x

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ 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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
j : Fin n
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:
simp [removeNth, *]

Premises used: Fin.removeNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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:
simp [removeNth, *]

Premises used: Fin.removeNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
⊢ p.insertNth (α := α) x (p.removeNth (α := α) f) = update (β := α) f p x

Tactic:
simp [Fin.insertNth_eq_iff]

Premises used: Fin.insertNth_eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
⊢ p.insertNth (α := α) (f p) (p.removeNth (α := α) f) = f

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x y : α p
f : (i : Fin n) → α (p.succAbove i)
⊢ update (β := α) (p.insertNth (α := α) x f) p y = p.insertNth (α := α) y f

Tactic:
simp [eq_insertNth_iff]

Premises used: Fin.eq_insertNth_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
i : Fin n
y : α (p.succAbove i)
f : (j : Fin n) → α (p.succAbove j)
⊢ p.insertNth (α := α) x (update (β := fun (j : Fin n) ↦ α (p.succAbove j)) f i y) =
    update (β := α) (p.insertNth (α := α) x f) (p.succAbove i) y

Tactic:
simp [insertNth_eq_iff]

Premises used: Fin.insertNth_eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ (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

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)).1 =
    f.1

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
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))
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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : (i : Fin (n + 1)) → α i
⊢ (fun (f : α p × ((i : Fin n) → α (p.succAbove i))) ↦ p.insertNth (α := α) f.1 f.2)
      ((fun (f : (i : Fin (n + 1)) → α i) ↦ (f p, p.removeNth (α := α) f)) f) =
    f

Tactic:
simp