awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
h :
  ∀ (j : Fin (n + 1)),
    snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x j =
      update (β := α) (snoc (α := α) p x) i.castSucc y j
⊢ snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x =
    update (β := α) (snoc (α := α) p x) i.castSucc y

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin n
h :
  ∀ (y : α j.castSucc),
    Eq (α := α j.castSucc) (snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p j y) x j.castSucc)
      (update (β := α) (snoc (α := α) p x) j.castSucc y j.castSucc)
h₁ :
  ∀ (hne : j ≠ i),
    Eq (α := α j.castSucc) (snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x j.castSucc)
      (update (β := α) (snoc (α := α) p x) i.castSucc y j.castSucc)
⊢ Eq (α := α j.castSucc) (snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x j.castSucc)
    (update (β := α) (snoc (α := α) p x) i.castSucc y j.castSucc)

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
x : α (last n)
p : (i : Fin n) → α i.castSucc
j : Fin n
y : α j.castSucc
⊢ Eq (α := α j.castSucc) (snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p j y) x j.castSucc)
    (update (β := α) (snoc (α := α) p x) j.castSucc y j.castSucc)

Tactic:
simp [*]
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin n
hne : j ≠ i
⊢ Eq (α := α j.castSucc) (snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x j.castSucc)
    (update (β := α) (snoc (α := α) p x) i.castSucc y j.castSucc)

Tactic:
simp [*]
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
⊢ Eq (α := α (last n)) (snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x (last n))
    (update (β := α) (snoc (α := α) p x) i.castSucc y (last n))

Tactic:
simp [Ne.symm]

Premises used: Ne.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h :
  ∀ (j : Fin n),
    Eq (α := α j.castSucc) (snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x j.castSucc)
      (update (β := α) (snoc (α := α) p x) i.castSucc y j.castSucc)
h₁ :
  Eq (α := α (last n)) (snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x (last n))
    (update (β := α) (snoc (α := α) p x) i.castSucc y (last n))
⊢ snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x j =
    update (β := α) (snoc (α := α) p x) i.castSucc y j

Tactic:
cases j using lastCases with
  | cast j => rcases eq_or_ne j i with rfl | hne <;> simp [*]
  | last => simp [Ne.symm]

Premises used: cast, Ne.symm, Fin.last, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
h : ∀ (j : Fin (n + 1)), update (β := α) (snoc (α := α) p x) (last n) z j = snoc (α := α) p z j
⊢ update (β := α) (snoc (α := α) p x) (last n) z = snoc (α := α) p z

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
h : Eq (α := α (last n)) (update (β := α) (snoc (α := α) p x) (last n) z (last n)) (snoc (α := α) p z (last n))
h₁ :
  ∀ (i : Fin n),
    Eq (α := α i.castSucc) (update (β := α) (snoc (α := α) p x) (last n) z i.castSucc) (snoc (α := α) p z i.castSucc)
⊢ update (β := α) (snoc (α := α) p x) (last n) z j = snoc (α := α) p z j

Tactic:
cases j using lastCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
⊢ Eq (α := α (last n)) (update (β := α) (snoc (α := α) p x) (last n) z (last n)) (snoc (α := α) p z (last n))

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
i : Fin n
⊢ Eq (α := α i.castSucc) (update (β := α) (snoc (α := α) p x) (last n) z i.castSucc) (snoc (α := α) p z i.castSucc)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
f : Fin n → α
x : α
h :
  ∀ (x_1 : α),
    Membership.mem (γ := Set α) (Set.range (ι := Fin (n + 1)) (snoc (α := fun (a : Fin (n + 1)) ↦ α) f x)) x_1 ↔
      x_1 ∈ insert x (Set.range f)
⊢ Set.range (ι := Fin (n + 1)) (snoc (α := fun (a : Fin (n + 1)) ↦ α) f x) = insert x (Set.range f)

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
f : Fin n → α
x x_1 : α
⊢ Membership.mem (γ := Set α) (Set.range (ι := Fin (n + 1)) (snoc (α := fun (a : Fin (n + 1)) ↦ α) f x)) x_1 ↔
    x_1 ∈ insert x (Set.range f)

Tactic:
simp [Fin.exists_fin_succ', or_comm, eq_comm]

Premises used: Fin.exists_fin_succ', eq_comm, or_comm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc (α := α) x xₙ = snoc (α := α) y yₙ
i : Fin n
⊢ x i = y i

Tactic:
simpa using congr_fun h (castSucc i)

Premises used: congr_fun, Fin.castSucc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc (α := α) x xₙ = snoc (α := α) y yₙ
⊢ xₙ = yₙ

Tactic:
simpa using congr_fun h (last n)

Premises used: Fin.last, congr_fun
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
⊢ snoc (α := α) x xₙ = snoc (α := α) y yₙ ↔ x = y ∧ xₙ = yₙ

Tactic:
snoc_injective2.eq_iff

Premises used: Function.Injective2.eq_iff, Fin.snoc_injective2
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : (i : Fin n) → α i.castSucc
⊢ Injective (snoc (α := α) x)

Tactic:
snoc_injective2.right _

Premises used: Function.Injective2.right, Fin.snoc_injective2
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
xₙ : α (last n)
⊢ Injective (β := (i : Fin (n + 1)) → α i) fun (x : (i : Fin n) → α i.castSucc) ↦ snoc (α := α) x xₙ

Tactic:
snoc_injective2.left _

Premises used: Function.Injective2.left, Fin.snoc_injective2
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
h : ∀ (j : Fin (n + 1)), snoc (α := α) (init (α := α) q) (q (last n)) j = q j
⊢ snoc (α := α) (init (α := α) q) (q (last n)) = q

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : Eq (α := α (last n)) (snoc (α := α) (init (α := α) q) (q (last n)) (last n)) (q (last n))
h₁ : ∀ (i : Fin n), Eq (α := α i.castSucc) (snoc (α := α) (init (α := α) q) (q (last n)) i.castSucc) (q i.castSucc)
⊢ snoc (α := α) (init (α := α) q) (q (last n)) j = q j

Tactic:
cases j using Fin.lastCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
⊢ Eq (α := α (last n)) (snoc (α := α) (init (α := α) q) (q (last n)) (last n)) (q (last n))

Tactic:
simp [init]

Premises used: Fin.init
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
⊢ Eq (α := α i.castSucc) (snoc (α := α) (init (α := α) q) (q (last n)) i.castSucc) (q i.castSucc)

Tactic:
simp [init]

Premises used: Fin.init
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
h : ∀ (j : Fin n), init (α := α) (update (β := α) q (last n) z) j = init (α := α) q j
⊢ init (α := α) (update (β := α) q (last n) z) = init (α := α) q

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
j : Fin n
⊢ init (α := α) (update (β := α) q (last n) z) j = init (α := α) q j

Tactic:
simp [init, Fin.ne_of_lt]

Premises used: Fin.ne_of_lt, Fin.init
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
h :
  ∀ (j : Fin n),
    init (α := α) (update (β := α) q i.castSucc y) j =
      update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y j
⊢ init (α := α) (update (β := α) q i.castSucc y) = update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
pos :
  ∀ (h : j = i),
    init (α := α) (update (β := α) q i.castSucc y) j =
      update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y j
neg :
  ∀ (h : ¬j = i),
    init (α := α) (update (β := α) q i.castSucc y) j =
      update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y j
⊢ init (α := α) (update (β := α) q i.castSucc y) j =
    update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y j

Tactic:
by_cases h : j = i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
pos :
  init (α := α) (update (β := α) q i.castSucc y) i =
    update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y i
⊢ init (α := α) (update (β := α) q i.castSucc y) j =
    update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y j

Tactic:
rw [h]
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (α := α) (update (β := α) q i.castSucc y) i =
    update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y i

Tactic:
simp [init]

Premises used: Fin.init
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : ¬j = i
⊢ init (α := α) (update (β := α) q i.castSucc y) j =
    update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y j

Tactic:
simp [init, h, castSucc_inj]

Premises used: Fin.init, Fin.castSucc_inj
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
h :
  ∀ (i : Fin n),
    tail (α := fun (i : Fin (n + 1)) ↦ β) (init (α := fun (i : Fin (n + 1 + 1)) ↦ β) q) i =
      init (α := fun (i : Fin (n + 1)) ↦ β) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ β) q) i
⊢ tail (α := fun (i : Fin (n + 1)) ↦ β) (init (α := fun (i : Fin (n + 1 + 1)) ↦ β) q) =
    init (α := fun (i : Fin (n + 1)) ↦ β) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ β) q)

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
i : Fin n
⊢ tail (α := fun (i : Fin (n + 1)) ↦ β) (init (α := fun (i : Fin (n + 1 + 1)) ↦ β) q) i =
    init (α := fun (i : Fin (n + 1)) ↦ β) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ β) q) i

Tactic:
simp [tail, init]

Premises used: Fin.init, Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
h :
  ∀ (i : Fin (n.succ + 1)),
    Eq.{u_2} (α := β)
      (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
          (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) i :
        β)
      (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b i)
⊢ Eq.{u_2} (α := (i : Fin (n.succ + 1)) → β)
    (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
      (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b))
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b)

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
⊢ Eq.{u_2} (α := β)
    (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
        (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) 0 :
      β)
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b 0 : β)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
⊢ Eq.{u_2} (α := β)
    (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
        (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) (last n).succ :
      β)
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b (last n).succ)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
h :
  Eq.{u_2} (α := β)
    (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b j.castSucc :
      (fun (x : Fin (n.succ + 1)) ↦ β) j.castSucc.succ)
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b j.castSucc.succ : β)
⊢ Eq.{u_2} (α := β)
    (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
        (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) j.castSucc.succ :
      β)
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b j.castSucc.succ)

Tactic:
rw [cons_succ]

Premises used: Fin.cons_succ
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
⊢ Eq.{u_2} (α := β)
    (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b j.castSucc :
      (fun (x : Fin (n.succ + 1)) ↦ β) j.castSucc.succ)
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b j.castSucc.succ : β)

Tactic:
simp [← castSucc_succ]

Premises used: Fin.castSucc_succ
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin (n + 1)
h :
  Eq.{u_2} (α := β)
    (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
        (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) (last n).succ :
      β)
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b (last n).succ)
h₁ :
  ∀ (j : Fin n),
    Eq.{u_2} (α := β)
      (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
          (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) j.castSucc.succ :
        β)
      (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b j.castSucc.succ)
⊢ Eq.{u_2} (α := β)
    (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
        (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) j.succ :
      β)
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b j.succ)

Tactic:
cases j using Fin.lastCases with
    | last => simp
    | cast j =>
      rw [cons_succ]
      simp [← castSucc_succ]

Premises used: Fin.cons_succ, cast, Fin.castSucc_succ, Fin.last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h :
  Eq.{u_2} (α := β)
    (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
        (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) 0 :
      β)
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b 0 : β)
h₁ :
  ∀ (j : Fin (n + 1)),
    Eq.{u_2} (α := β)
      (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
          (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) j.succ :
        β)
      (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b j.succ)
⊢ Eq.{u_2} (α := β)
    (cons (α := fun (x : Fin (n.succ + 1)) ↦ β) a
        (snoc (α := fun (i : Fin n.succ) ↦ (fun (x : Fin (n.succ + 1)) ↦ β) i.succ) q b) i :
      β)
    (snoc (α := fun (i : Fin (n + 1 + 1)) ↦ β) (cons (α := fun (i : Fin (n + 1)) ↦ β) a q) b i)

Tactic:
cases i using Fin.cases with
  | zero => simp
  | succ j =>
    cases j using Fin.lastCases with
    | last => simp
    | cast j =>
      rw [cons_succ]
      simp [← castSucc_succ]

Premises used: Fin.cons_succ, Fin.succ, cast, Fin.castSucc_succ, Fin.last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
h :
  ∀ (j : Fin (n + 1)),
    (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) j = snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) j
⊢ Eq (α := Fin (n + 1) → β) (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y)
    (snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y))

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
pos :
  ∀ (h : (↑j : ℕ) < n),
    (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) j = snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) j
neg :
  ∀ (h : ¬(↑j : ℕ) < n),
    (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) j = snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) j
⊢ (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) j = snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) j

Tactic:
by_cases h : j.val < n

Premises used: Fin.val
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : (↑j : ℕ) < n
⊢ (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) j = snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) j

Tactic:
simp [h, snoc, castSucc_castLT]

Premises used: Fin.snoc, Fin.castSucc_castLT
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬(↑j : ℕ) < n
neg :
  (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) (last n) =
    snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) (last n)
⊢ (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) j = snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) j

Tactic:
rw [eq_last_of_not_lt h]

Premises used: Fin.eq_last_of_not_lt
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬(↑j : ℕ) < n
⊢ (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) (last n) =
    snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) (last n)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
h : ∀ (i : Fin (n + 1)), append x x₀ i = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) i
⊢ append x x₀ = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0)

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ append x x₀ i = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) i

Tactic:
Fin.addCases ?_ ?_ i

Premises used: Fin.addCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
h : ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (castAdd 1 i)
h₁ : ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (natAdd n i)
⊢ append x x₀ i = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) i

Tactic:
refine Fin.addCases ?_ ?_ i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
h : x i = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (castAdd 1 i)
⊢ append x x₀ (castAdd 1 i) = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (castAdd 1 i)

Tactic:
rw [Fin.append_left]

Premises used: Fin.append_left
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (castAdd 1 i)

Tactic:
(@snoc_castSucc _ (fun _ => α) _ _ i).symm

Premises used: Fin.snoc_castSucc, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (castAdd 1 i)

Tactic:
exact (@snoc_castSucc _ (fun _ => α) _ _ i).symm

Premises used: Fin.snoc_castSucc, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
h : x₀ 0 = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (natAdd n 0)
⊢ append x x₀ (natAdd n i) = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (natAdd n i)

Tactic:
rw [Subsingleton.elim i 0, Fin.append_right]

Premises used: Fin.append_right, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (natAdd n 0)

Tactic:
(@snoc_last _ (fun _ => α) _ _).symm

Premises used: Fin.natAdd, Eq.symm, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (natAdd n 0)

Tactic:
exact (@snoc_last _ (fun _ => α) _ _).symm

Premises used: Eq.symm, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_2
xs : Fin n → α
x : α
⊢ snoc (α := fun (a : Fin (n + HAdd.hAdd (α := ℕ) 0 1)) ↦ α) xs x =
    append xs (cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x elim0)

Tactic:
(append_right_eq_snoc xs (cons x Fin.elim0)).symm

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.append_right_eq_snoc, Fin.induction, Fin.cases, Eq.symm, Fin.elim0
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
rw :
  (append xs
          (cons (α := fun (a : Fin (m + 1)) ↦ α) (cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x elim0 0)
            ys) ∘
        Fin.cast ⋯) ∘
      Fin.cast ⋯ =
    append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) x ys) ∘ Fin.cast ⋯
⊢ append (snoc (α := fun (a : Fin (n + 1)) ↦ α) xs x) ys =
    append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) x ys) ∘ Fin.cast ⋯

Tactic:
rw [snoc_eq_append, append_assoc, append_left_eq_cons, append_cast_right]

Premises used: Fin.append_assoc, Fin.append_left_eq_cons, Fin.snoc_eq_append, Fin.append_cast_right
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ (append xs
          (cons (α := fun (a : Fin (m + 1)) ↦ α) (cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x elim0 0)
            ys) ∘
        Fin.cast ⋯) ∘
      Fin.cast ⋯ =
    append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) x ys) ∘ Fin.cast ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
rw :
  append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) y ys) =
    (append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) y ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯
⊢ append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) y ys) =
    append (snoc (α := fun (a : Fin (n + 1)) ↦ α) xs y) ys ∘ Fin.cast ⋯

Tactic:
rw [append_left_snoc]

Premises used: Fin.append_left_snoc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) y ys) =
    (append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) y ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
h :
  ∀ (i : Fin (n + 1 + m)),
    append (cons (α := fun (a : Fin (n + 1)) ↦ α) a as) bs i =
      (cons (α := fun (a : Fin (n + m + 1)) ↦ α) a (append as bs) ∘ Fin.cast ⋯) i
⊢ append (cons (α := fun (a : Fin (n + 1)) ↦ α) a as) bs =
    cons (α := fun (a : Fin (n + m + 1)) ↦ α) a (append as bs) ∘ Fin.cast ⋯

Tactic:
funext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : Fin (n + 1 + m)
h :
  ∀ (i : ℕ) (isLt : i < n + 1 + m),
    append (cons (α := fun (a : Fin (n + 1)) ↦ α) a as) bs (⟨i, isLt⟩ : Fin (n + 1 + m)) =
      (cons (α := fun (a : Fin (n + m + 1)) ↦ α) a (append as bs) ∘ Fin.cast ⋯) (⟨i, isLt⟩ : Fin (n + 1 + m))
⊢ append (cons (α := fun (a : Fin (n + 1)) ↦ α) a as) bs i =
    (cons (α := fun (a : Fin (n + m + 1)) ↦ α) a (append as bs) ∘ Fin.cast ⋯) i

Tactic:
rcases i with ⟨i, -⟩