awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i < n + 1 + m
h :
  Eq.{u_2} (α := α)
    (if h : i < n + 1 then cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨i, ⋯⟩ : Fin (n + 1))
      else
        @Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i, isLt⟩ : Fin (n + 1 + m))) ⋯))
          (fun (x : Fin (n + 1 + m))
              (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i, isLt⟩ : Fin (n + 1 + m))) ⋯) = x) ↦
            α)
          (bs (subNat (n + 1) (Fin.cast ⋯ (⟨i, isLt⟩ : Fin (n + 1 + m))) ⋯)) _ ⋯ :
      α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast ⋯ (⟨i, isLt⟩ : Fin (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))

Tactic:
simp only [append, addCases, cons, castLT, comp_apply]

Premises used: Fin.cons, Function.comp_apply, Fin.append, Fin.castLT
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i < n + 1 + m
h :
  ∀ (isLt : 0 < n + 1 + m),
    Eq.{u_2} (α := α)
      (if h : 0 < n + 1 then cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨0, ⋯⟩ : Fin (n + 1))
        else
          @Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨0, isLt⟩ : Fin (n + 1 + m))) ⋯))
            (fun (x : Fin (n + 1 + m))
                (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨0, isLt⟩ : Fin (n + 1 + m))) ⋯) = x) ↦
              α)
            (bs (subNat (n + 1) (Fin.cast ⋯ (⟨0, isLt⟩ : Fin (n + 1 + m))) ⋯)) _ ⋯ :
        α)
      (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
          (Fin.cast ⋯ (⟨0, isLt⟩ : Fin (n + 1 + m))) :
        α)
h₁ :
  ∀ (i : ℕ) (isLt : i + 1 < n + 1 + m),
    Eq.{u_2} (α := α)
      (if h : i + 1 < n + 1 then cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨i + 1, ⋯⟩ : Fin (n + 1))
        else
          @Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯))
            (fun (x : Fin (n + 1 + m))
                (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯) = x) ↦
              α)
            (bs (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯)) _ ⋯ :
        α)
      (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
          (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
        α)
⊢ Eq.{u_2} (α := α)
    (if h : i < n + 1 then cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨i, ⋯⟩ : Fin (n + 1))
      else
        @Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i, isLt⟩ : Fin (n + 1 + m))) ⋯))
          (fun (x : Fin (n + 1 + m))
              (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i, isLt⟩ : Fin (n + 1 + m))) ⋯) = x) ↦
            α)
          (bs (subNat (n + 1) (Fin.cast ⋯ (⟨i, isLt⟩ : Fin (n + 1 + m))) ⋯)) _ ⋯ :
      α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast ⋯ (⟨i, isLt⟩ : Fin (n + 1 + m))) :
      α)

Tactic:
rcases i with - | i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
isLt : 0 < n + 1 + m
⊢ Eq.{u_2} (α := α)
    (if h : 0 < n + 1 then cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨0, ⋯⟩ : Fin (n + 1))
      else
        @Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨0, isLt⟩ : Fin (n + 1 + m))) ⋯))
          (fun (x : Fin (n + 1 + m))
              (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨0, isLt⟩ : Fin (n + 1 + m))) ⋯) = x) ↦
            α)
          (bs (subNat (n + 1) (Fin.cast ⋯ (⟨0, isLt⟩ : Fin (n + 1 + m))) ⋯)) _ ⋯ :
      α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast ⋯ (⟨0, isLt⟩ : Fin (n + 1 + m))) :
      α)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i + 1 < n + 1 + m
pos :
  ∀ (h : i + 1 < n + 1),
    Eq.{u_2} (α := α) (cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨i + 1, ⋯⟩ : Fin (n + 1)) : α)
      (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
          (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
        α)
neg :
  ∀ (h : ¬i + 1 < n + 1),
    Eq.{u_2} (α := α)
      (@Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯))
          (fun (x : Fin (n + 1 + m))
              (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯) = x) ↦
            α)
          (bs (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯)) _ ⋯ :
        α)
      (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
          (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
        α)
⊢ Eq.{u_2} (α := α)
    (if h : i + 1 < n + 1 then cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨i + 1, ⋯⟩ : Fin (n + 1))
      else
        @Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯))
          (fun (x : Fin (n + 1 + m))
              (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯) = x) ↦
            α)
          (bs (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯)) _ ⋯ :
      α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
      α)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i + 1 < n + 1 + m
h : i + 1 < n + 1
⊢ i < n

Tactic:
have : i < n := Nat.lt_of_succ_lt_succ h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i + 1 < n + 1 + m
h : i + 1 < n + 1
this : i < n
⊢ Eq.{u_2} (α := α) (cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨i + 1, ⋯⟩ : Fin (n + 1)) : α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
      α)

Tactic:
simp [addCases, this]
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
⊢ ¬i < n

Tactic:
have : ¬i < n := Nat.not_le_of_gt <| Nat.le_of_lt_succ <| Nat.gt_of_not_le h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
this : ¬i < n
⊢ Eq.{u_2} (α := α)
    (@Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯))
        (fun (x : Fin (n + 1 + m))
            (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯) = x) ↦
          α)
        (bs (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯)) _ ⋯ :
      α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
      α)

Tactic:
simp [addCases, this]
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
h :
  ∀ (i : Fin (n + (m + 1))),
    append as (snoc (α := fun (a : Fin (m + 1)) ↦ α) bs b) i =
      snoc (α := fun (i : Fin (n.add m + 1)) ↦ α) (append as bs) b i
⊢ append as (snoc (α := fun (a : Fin (m + 1)) ↦ α) bs b) = snoc (α := fun (i : Fin (n.add m + 1)) ↦ α) (append as bs) b

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

Tactic:
rcases i with ⟨i, isLt⟩

Premises used: Fin.isLt
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
h :
  Eq.{u_2} (α := α) (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b)
    (if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b)
⊢ append as (snoc (α := fun (a : Fin (m + 1)) ↦ α) bs b) (⟨i, isLt⟩ : Fin (n + (m + 1))) =
    snoc (α := fun (i : Fin (n.add m + 1)) ↦ α) (append as bs) b (⟨i, isLt⟩ : Fin (n + (m + 1)))

Tactic:
simp only [append, addCases, castLT, cast_mk, subNat_mk, natAdd_mk, cast, snoc.eq_1,
    eq_rec_constant, Nat.add_eq]

Premises used: Nat.add_eq, cast, Fin.subNat_mk, Fin.cast_mk, eq_rec_constant, Fin.natAdd_mk, Fin.snoc.eq_1, Fin.append, Fin.castLT
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
pos : ∀ (lt_n : i < n) (lt_add : i < n + m), as (⟨i, ⋯⟩ : Fin n) = as ⟨i, ⋯⟩
neg : ∀ (lt_n : i < n) (lt_add : ¬i < n + m), as (⟨i, ⋯⟩ : Fin n) = b
pos₁ : ∀ (lt_n : ¬i < n) (sub_lt : i - n < m) (nlt_add : i < n + m), bs (⟨i - n, ⋯⟩ : Fin m) = bs ⟨i - n, ⋯⟩
neg₁ : ∀ (lt_n : ¬i < n) (sub_lt : i - n < m) (nlt_add : ¬i < n + m), bs (⟨i - n, ⋯⟩ : Fin m) = b
pos₂ : ∀ (lt_n : ¬i < n) (sub_lt : ¬i - n < m) (lt_add : i < n + m), b = bs ⟨i - n, ⋯⟩
neg₂ : ∀ (lt_n : ¬i < n) (sub_lt : ¬i - n < m) (lt_add : ¬i < n + m), b = b
⊢ Eq.{u_2} (α := α) (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b)
    (if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b)

Tactic:
split_ifs with lt_n lt_add sub_lt nlt_add lt_add
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : i < n + m
⊢ as (⟨i, ⋯⟩ : Fin n) = as ⟨i, ⋯⟩

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : i < n + m
⊢ as (⟨i, ⋯⟩ : Fin n) = as ⟨i, ⋯⟩

Tactic:
try rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : i < n + m
⊢ bs (⟨i - n, ⋯⟩ : Fin m) = bs ⟨i - n, ⋯⟩

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : i < n + m
⊢ bs (⟨i - n, ⋯⟩ : Fin m) = bs ⟨i - n, ⋯⟩

Tactic:
try rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : ¬i < n + m
⊢ b = b

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : ¬i < n + m
⊢ b = b

Tactic:
try rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
⊢ i < n + m

Tactic:
have := Nat.lt_add_right m lt_n
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
this : i < n + m
⊢ as (⟨i, ⋯⟩ : Fin n) = b

Tactic:
contradiction
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
neg :
  ∀ (isLt : n + m < n + (m + 1)) (lt_n : ¬n + m < n) (sub_lt : n + m - n < m) (nlt_add : ¬n + m < n + m),
    bs (⟨n + m - n, ⋯⟩ : Fin m) = b
⊢ bs (⟨i - n, ⋯⟩ : Fin m) = b

Tactic:
obtain rfl := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp nlt_add) isLt

Premises used: Nat.not_lt, Nat.eq_of_le_of_lt_succ, Iff.mp, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
isLt : n + m < n + (m + 1)
lt_n : ¬n + m < n
sub_lt : n + m - n < m
nlt_add : ¬n + m < n + m
⊢ bs (⟨n + m - n, ⋯⟩ : Fin m) = b

Tactic:
simp [Nat.add_comm n m] at sub_lt

Premises used: Nat.add_comm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ i - n < m

Tactic:
have := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp lt_n) lt_add
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
this : i - n < m
⊢ b = bs ⟨i - n, ⋯⟩

Tactic:
contradiction
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
h : ∀ (j : Fin n), (g ∘ init (α := fun (i : Fin (n + 1)) ↦ α) q) j = init (α := fun (a : Fin (n + 1)) ↦ β) (g ∘ q) j
⊢ g ∘ init (α := fun (i : Fin (n + 1)) ↦ α) q = init (α := fun (a : Fin (n + 1)) ↦ β) (g ∘ q)

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
j : Fin n
⊢ (g ∘ init (α := fun (i : Fin (n + 1)) ↦ α) q) j = init (α := fun (a : Fin (n + 1)) ↦ β) (g ∘ q) j

Tactic:
simp [init]

Premises used: Fin.init
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u_1
x : α_1 (last n)
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.castSucc
i : Fin n
y : α_1 i.castSucc
z : α_1 (last n)
α : Fin (n + 1) → Type u_2
f : α (last n) × ((i : Fin n) → α i.castSucc)
⊢ (fun (f : (i : Fin (n + 1)) → α i) ↦ ((f (last n), init (α := α) f) : α (last n) × ((i : Fin n) → α i.castSucc)))
      ((fun (f : α (last n) × ((i : Fin n) → α i.castSucc)) (x : Fin (n + 1)) ↦ snoc (α := α) f.2 f.1 x) f) =
    f

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u_1
x : α_1 (last n)
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.castSucc
i : Fin n
y : α_1 i.castSucc
z : α_1 (last n)
α : Fin (n + 1) → Type u_2
f : (i : Fin (n + 1)) → α i
⊢ (fun (f : α (last n) × ((i : Fin n) → α i.castSucc)) (x : Fin (n + 1)) ↦ snoc (α := α) f.2 f.1 x)
      ((fun (f : (i : Fin (n + 1)) → α i) ↦ ((f (last n), init (α := α) f) : α (last n) × ((i : Fin n) → α i.castSucc)))
        f) =
    f

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Fin (n + 1) → Sort u_1
x_1 : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
z : α (last n)
motive : ((i : Fin n.succ) → α i) → Sort u_2
snoc : (xs : (i : Fin n) → α i.castSucc) → (x : α (last n)) → motive (Fin.snoc (α := α) xs x)
x : (i : Fin n.succ) → α i
rw rw₁ : motive x = motive x
⊢ motive (Fin.snoc (α := α) (init (α := α) x) (x (last n))) = motive x

Tactic:
rw [Fin.snoc_init_self]

Premises used: Fin.snoc_init_self
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc (α := α) x x₀)
x : (i : Fin n) → init (α := fun (i : Fin (n + 1)) ↦ Sort u_1) α i
x₀ : α (last n)
rw : cast ⋯ (snoc (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))) = snoc x x₀
rw₁ :
  HEq (α := motive (Fin.snoc (α := α) (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))))
    (snoc (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))) (snoc x x₀)
rw₂ :
  HEq (α := motive (Fin.snoc (α := α) x (Fin.snoc (α := α) x x₀ (last n)))) (snoc x (Fin.snoc (α := α) x x₀ (last n)))
    (snoc x x₀)
rw₃ rw₄ : snoc x x₀ ≍ snoc x x₀
⊢ snocCases (α := α) (motive := fun (x : (i : Fin (n + 1)) → α i) ↦ motive x) snoc (Fin.snoc (α := α) x x₀) = snoc x x₀

Tactic:
rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]

Premises used: cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u_1
x_1 : α_1 (last n)
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.castSucc
i : Fin n
y : α_1 i.castSucc
z : α_1 (last n)
α : Sort u_2
motive : {n : ℕ} → (Fin n → α) → Sort u_3
elim0 : motive Fin.elim0
snoc :
  {n : ℕ} → (x : Fin n → α) → (x₀ : α) → motive x → motive (n := n + 1) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ α) x x₀)
x : Fin 0 → α
⊢ motive x

Tactic:
convert! elim0
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i j : Fin n
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j.castSucc : α)
⊢ i.castSucc = j.castSucc

Tactic:
simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h

Premises used: Fin.snoc_castSucc, Function.Injective.eq_iff, Fin.castSucc_inj
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)
⊢ x i = x₀

Tactic:
simp only [snoc_castSucc, snoc_last] at h

Premises used: Fin.snoc_castSucc, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h : x i = x₀
⊢ ¬x i ∈ Set.range x

Tactic:
rw [← h] at hx₀
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h : x i = x₀
hx₁ : ¬x i ∈ Set.range x
⊢ x i = x₀

Tactic:
rw [← h] at hx₀
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
i : Fin n
hx₀ : ¬x i ∈ Set.range x
h : x i = x₀
⊢ i.castSucc = last n

Tactic:
apply hx₀.elim (Set.mem_range_self i)

Premises used: Set.mem_range_self, Not.elim
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin (n + 1)
i : Fin n
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)
cast :
  ∀ (j : Fin n)
    (h :
      Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
        (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j.castSucc : α)),
    i.castSucc = j.castSucc
cast₁ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
        (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)),
    i.castSucc = last n
⊢ i.castSucc = j

Tactic:
induction j using lastCases with
    | cast j =>
      simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
    | last =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)

Premises used: Fin.snoc_castSucc, Function.Injective.eq_iff, cast, Not.elim, Fin.castSucc_inj, Fin.last, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j.castSucc : α)
⊢ x₀ = x j

Tactic:
simp only [snoc_castSucc, snoc_last] at h

Premises used: Fin.snoc_castSucc, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h : x₀ = x j
⊢ ¬x j ∈ Set.range x

Tactic:
rw [h] at hx₀
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h : x₀ = x j
hx₁ : ¬x j ∈ Set.range x
⊢ x₀ = x j

Tactic:
rw [h] at hx₀
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
j : Fin n
hx₀ : ¬x j ∈ Set.range x
h : x₀ = x j
⊢ last n = j.castSucc

Tactic:
apply hx₀.elim (Set.mem_range_self j)

Premises used: Set.mem_range_self, Not.elim
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)
⊢ last n = last n

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin (n + 1)
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (Fin.last n) : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)
last :
  ∀ (j : Fin n)
    (h :
      Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (Fin.last n) : α)
        (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j.castSucc : α)),
    Fin.last n = j.castSucc
last₁ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (Fin.last n) : α)
        (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (Fin.last n) : α)),
    Fin.last n = Fin.last n
⊢ Fin.last n = j

Tactic:
induction j using lastCases with
    | cast j =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [h] at hx₀
      apply hx₀.elim (Set.mem_range_self j)
    | last => simp

Premises used: Fin.snoc_castSucc, cast, Not.elim, Fin.last, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i j : Fin (n + 1)
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)
cast :
  ∀ (i : Fin n)
    (h :
      Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
        (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)),
    i.castSucc = j
last :
  ∀
    (h :
      Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (Fin.last n) : α)
        (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)),
    Fin.last n = j
⊢ i = j

Tactic:
induction i using lastCases with
  | cast i =>
    induction j using lastCases with
    | cast j =>
      simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
    | last =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)
  | last =>
    induction j using lastCases with
    | cast j =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [h] at hx₀
      apply hx₀.elim (Set.mem_range_self j)
    | last => simp

Premises used: Fin.snoc_castSucc, Function.Injective.eq_iff, cast, Not.elim, Fin.castSucc_inj, Fin.last, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
⊢ Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀) ↔
    Injective x ∧ ¬x₀ ∈ Set.range x

Tactic:
⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ snoc_injective_of_injective h.1 h.2⟩

Premises used: And.right, And.left, And.intro, Iff.intro, Fin.snoc_injective_of_injective
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
refine_1 :
  ∀ (h : Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀)), Injective x
refine_2 :
  ∀ (h : Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀)),
    ¬x₀ ∈ Set.range x
⊢ Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀) ↔
    Injective x ∧ ¬x₀ ∈ Set.range x

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ snoc_injective_of_injective h.1 h.2⟩