awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
hi : IsMax i
obtain :
  ∀ (hi : IsMax (last n)),
    (fun (i : Fin (n + 1)) ↦ (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
        (last n) =
      last n
⊢ (fun (i : Fin (n + 1)) ↦ (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
      i =
    i

Tactic:
obtain rfl : i = Fin.last n := by simpa using hi

Premises used: Fin.last, rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
hi : IsMax (last n)
⊢ (fun (i : Fin (n + 1)) ↦ (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
      (last n) =
    last n

Tactic:
simp
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 1) → Fin (n + 1)) Order.succ fun (i : Fin (n + 1)) ↦
    lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i

Tactic:
rfl

Premises used: Fin.reverseInduction, Order.succ, Fin.lastCases, rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Order.succ i = lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i

Tactic:
rfl

Premises used: Fin.reverseInduction, Order.succ, Fin.lastCases, rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
⊢ Order.succ (last n) = last n

Tactic:
simp [orderSucc_apply]

Premises used: Fin.orderSucc_apply
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin n
⊢ Order.succ i.castSucc = i.succ

Tactic:
simp [orderSucc_apply]

Premises used: Fin.orderSucc_apply
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
pred_le : ∀ (a : Fin 0), a.elim0 ≤ a
min_of_le_pred : ∀ {a : Fin 0}, a ≤ a.elim0 → IsMin a
le_pred_of_lt : ∀ {a b : Fin 0}, a < b → a ≤ b.elim0
pred : Fin 0 → Fin 0
⊢ PredOrder (Fin 0)

Tactic:
constructor
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ a.elim0 ≤ a

Tactic:
elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ a.elim0 ≤ a

Tactic:
exact elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
pred_le pred_le₁ : ∀ (a : Fin 0), a.elim0 ≤ a
⊢ ∀ (a : Fin 0), a.elim0 ≤ a

Tactic:
first | intro a; exact elim0 a
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ a ≤ a.elim0 → IsMin a

Tactic:
elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ a ≤ a.elim0 → IsMin a

Tactic:
exact elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
min_of_le_pred min_of_le_pred₁ : ∀ {a : Fin 0}, a ≤ a.elim0 → IsMin a
⊢ ∀ {a : Fin 0}, a ≤ a.elim0 → IsMin a

Tactic:
first | intro a; exact elim0 a
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a b : Fin 0
⊢ a < b → a ≤ b.elim0

Tactic:
elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → a ≤ b.elim0

Tactic:
exact elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
le_pred_of_lt le_pred_of_lt₁ : ∀ {a b : Fin 0}, a < b → a ≤ b.elim0
⊢ ∀ {a b : Fin 0}, a < b → a ≤ b.elim0

Tactic:
first | intro a; exact elim0 a
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
pred pred₁ : (a : Fin 0) → Fin 0
⊢ Fin 0 → Fin 0

Tactic:
first | intro a; exact elim0 a
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
hi : ¬IsMin i
j : Fin (n + 1)
⊢ i ≠ 0

Tactic:
simpa using hi
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
hi : ¬IsMin i
j : Fin (n + 1)
obtain :
  ∀ (i : Fin n) (hi : ¬IsMin i.succ),
    j < i.succ ↔
      j ≤
        (fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1)))
          i.succ
⊢ j < i ↔
    j ≤ (fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1))) i

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (by simpa using hi)

Premises used: Fin.eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
j : Fin (n + 1)
i : Fin n
hi : ¬IsMin i.succ
⊢ j < i.succ ↔
    j ≤
      (fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1)))
        i.succ

Tactic:
simp [le_castSucc_iff]

Premises used: Fin.le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
hi : IsMin i
⊢ i = 0

Tactic:
simpa using hi
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
hi : IsMin i
obtain :
  ∀ (hi : IsMin (α := Fin (n + 1)) 0),
    Eq (α := Fin (n + 1))
      ((fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1))) 0) 0
⊢ (fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1))) i = i

Tactic:
obtain rfl : i = 0 := by simpa using hi

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
hi : IsMin (α := Fin (n + 1)) 0
⊢ Eq (α := Fin (n + 1))
    ((fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1))) 0) 0

Tactic:
rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 1) → Fin (n + 1)) Order.pred fun (i : Fin (n + 1)) ↦
    cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i

Tactic:
rfl

Premises used: Fin.induction, Order.pred, Fin.cases, rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Order.pred i = cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i

Tactic:
rfl

Premises used: Fin.induction, Order.pred, Fin.cases, rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 1)) (Order.pred 0) 0

Tactic:
rfl

Premises used: Eq.mpr, Fin.induction.go, Fin.ofNat, Fin.induction, Order.pred, Fin.cases, rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin n
⊢ Order.pred i.succ = i.castSucc

Tactic:
rfl

Premises used: Fin.induction.go, Fin.induction, Order.pred, Fin.cases, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Fin 0 → Sort u
⊢ Unique.{u} ((i : Fin 0) → α i)

Tactic:
infer_instance
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Fin 0 → Type u_1
inst : (i : Fin 0) → Preorder (α i)
f g : (i : Fin 0) → α i
⊢ f ≤ g

Tactic:
finZeroElim

Premises used: finZeroElim
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
⊢ Eq.{u_1} (α := (i : Fin n) → α i.succ) (tail (α := α) fun (k : Fin (n + 1)) ↦ q k) fun (k : Fin n) ↦ q k.succ

Tactic:
rfl

Premises used: Fin.tail, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
⊢ tail (α := α) (cons (α := α) x p) = p

Tactic:
simp +unfoldPartialApp [tail, cons]

Premises used: Fin.cons, Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
⊢ cons (α := α) x p i.succ = p i

Tactic:
simp [cons]

Premises used: Fin.cons
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
⊢ cons (α := α) x p 0 = x

Tactic:
simp [cons]

Premises used: Fin.cons
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
rw : Eq (α := α 1) (cons (α := α) x p 1) (cons (α := α) x p (succ 0))
⊢ Eq (α := α 1) (cons (α := α) x p 1 : α 1) (p 0)

Tactic:
rw [← cons_succ x p]

Premises used: Fin.cons_succ
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ Eq (α := α 1) (cons (α := α) x p 1) (cons (α := α) x p (succ 0))

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
rw : Eq (α := α (last (n + 1))) (cons (α := α) x p (last (n + 1))) (cons (α := α) x p (last n).succ)
⊢ Eq (α := α (last (n + 1))) (cons (α := α) x p (last (n + 1)) : α (last (n + 1))) (p (last n))

Tactic:
rw [← cons_succ x p]

Premises used: Fin.cons_succ
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ Eq (α := α (last (n + 1))) (cons (α := α) x p (last (n + 1))) (cons (α := α) x p (last n).succ)

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
h :
  ∀ (j : Fin (n + 1)),
    cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) j = update (β := α) (cons (α := α) x p) i.succ y j
⊢ cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) = update (β := α) (cons (α := α) x p) i.succ y

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h :
  Eq (α := α 0) (cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) 0)
    (update (β := α) (cons (α := α) x p) i.succ y 0)
h₁ :
  ∀ (i_1 : Fin n),
    Eq (α := α i_1.succ) (cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) i_1.succ)
      (update (β := α) (cons (α := α) x p) i.succ y i_1.succ)
⊢ cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) j = update (β := α) (cons (α := α) x p) i.succ y j

Tactic:
cases j using Fin.cases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
⊢ Eq (α := α 0) (cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) 0)
    (update (β := α) (cons (α := α) x p) i.succ y 0)

Tactic:
simp [Ne.symm, update_apply_of_injective _ (succ_injective _)]

Premises used: Function.update_apply_of_injective, Fin.succ_injective, Ne.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
i_1 : Fin n
⊢ Eq (α := α i_1.succ) (cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) i_1.succ)
    (update (β := α) (cons (α := α) x p) i.succ y i_1.succ)

Tactic:
simp [Ne.symm, update_apply_of_injective _ (succ_injective _)]

Premises used: Function.update_apply_of_injective, Fin.succ_injective, Ne.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
h : cons (α := α) x₀ x = cons (α := α) y₀ y
i : Fin n
⊢ x i = y i

Tactic:
simpa using congr_fun h (Fin.succ i)

Premises used: Fin.succ, congr_fun
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
⊢ cons (α := α) x₀ x = cons (α := α) y₀ y ↔ x₀ = y₀ ∧ x = y

Tactic:
cons_injective2.eq_iff

Premises used: Fin.cons_injective2, Function.Injective2.eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : (i : Fin n) → α i.succ
⊢ Injective (β := (i : Fin (n + 1)) → α i) fun (x₀ : α 0) ↦ cons (α := α) x₀ x

Tactic:
cons_injective2.left _

Premises used: Fin.cons_injective2, Function.Injective2.left
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x₀ : α 0
⊢ Injective (cons (α := α) x₀)

Tactic:
cons_injective2.right _

Premises used: Function.Injective2.right, Fin.cons_injective2
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
h : ∀ (j : Fin (n + 1)), update (β := α) (cons (α := α) x p) 0 z j = cons (α := α) z p j
⊢ update (β := α) (cons (α := α) x p) 0 z = cons (α := α) z p

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

Tactic:
cases j using Fin.cases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ Eq (α := α 0) (update (β := α) (cons (α := α) x p) 0 z 0) (cons (α := α) z p 0)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
i : Fin n
⊢ Eq (α := α i.succ) (update (β := α) (cons (α := α) x p) 0 z i.succ) (cons (α := α) z p i.succ)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
h : ∀ (j : Fin (n + 1)), cons (α := α) (q 0) (tail (α := α) q) j = q j
⊢ cons (α := α) (q 0) (tail (α := α) q) = q

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : Eq (α := α 0) (cons (α := α) (q 0) (tail (α := α) q) 0) (q 0)
h₁ : ∀ (i : Fin n), Eq (α := α i.succ) (cons (α := α) (q 0) (tail (α := α) q) i.succ) (q i.succ)
⊢ cons (α := α) (q 0) (tail (α := α) q) j = q j

Tactic:
cases j using Fin.cases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
⊢ Eq (α := α 0) (cons (α := α) (q 0) (tail (α := α) q) 0) (q 0)

Tactic:
simp [tail]

Premises used: Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
⊢ Eq (α := α i.succ) (cons (α := α) (q 0) (tail (α := α) q) i.succ) (q i.succ)

Tactic:
simp [tail]

Premises used: Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u
x : α_1 0
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.succ
i : Fin n
y : α_1 i.succ
z : α_1 0
α : Fin (n + 1) → Type u_1
f : α 0 × ((i : Fin n) → α i.succ)
⊢ (fun (f : (i : Fin (n + 1)) → α i) ↦ ((f 0, tail (α := α) f) : α 0 × ((i : Fin n) → α i.succ)))
      ((fun (f : α 0 × ((i : Fin n) → α i.succ)) ↦ cons (α := α) f.1 f.2) f) =
    f

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u
x : α_1 0
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.succ
i : Fin n
y : α_1 i.succ
z : α_1 0
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
⊢ (fun (f : α 0 × ((i : Fin n) → α i.succ)) ↦ cons (α := α) f.1 f.2)
      ((fun (f : (i : Fin (n + 1)) → α i) ↦ ((f 0, tail (α := α) f) : α 0 × ((i : Fin n) → α i.succ))) f) =
    f

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Fin (n + 1) → Sort u
x_1 : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
z : α 0
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons (α := α) x₀ x)
x : (i : Fin n.succ) → α i
rw rw₁ : motive x = motive x
⊢ motive (Fin.cons (α := α) (x 0) (tail (α := α) x)) = motive x

Tactic:
rw [cons_self_tail]

Premises used: Fin.cons_self_tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons (α := α) x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
rw : cons (Fin.cons (α := α) x₀ x 0) (tail (α := α) (Fin.cons (α := α) x₀ x)) = cons x₀ x
⊢ consCases (α := α) (motive := fun (x : (i : Fin (n + 1)) → α i) ↦ motive x) cons (Fin.cons (α := α) x₀ x) = cons x₀ x

Tactic:
rw [consCases, cast_eq]

Premises used: cast_eq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons (α := α) x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ cons (Fin.cons (α := α) x₀ x 0) (tail (α := α) (Fin.cons (α := α) x₀ x)) = cons x₀ x

Tactic:
congr
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u
x_1 : α_1 0
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.succ
i : Fin n
y : α_1 i.succ
z : α_1 0
α : Sort u_1
motive : {n : ℕ} → (Fin n → α) → Sort v
elim0 : motive Fin.elim0
cons :
  {n : ℕ} → (x₀ : α) → (x : Fin n → α) → motive x → motive (n := n + 1) (Fin.cons (α := 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_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i j : Fin (n + 1)
zero :
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
    0 = j
succ :
  ∀ (i : Fin n),
    Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
        (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
      i.succ = j
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j) →
    i = j

Tactic:
cases i using Fin.cases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
zero :
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
    Eq (α := Fin (n + 1)) 0 0
zero₁ :
  ∀ (i : Fin n),
    Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
        (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α) →
      0 = i.succ
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
    0 = j

Tactic:
cases j using Fin.cases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
i : Fin n
succ :
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
    i.succ = 0
succ₁ :
  ∀ (i_1 : Fin n),
    Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
        (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i_1.succ : α) →
      i.succ = i_1.succ
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
    i.succ = j

Tactic:
cases j using Fin.cases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
    Eq (α := Fin (n + 1)) 0 0

Tactic:
aesop (add simp [hx.eq_iff])

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i : Fin n
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α) →
    0 = i.succ

Tactic:
aesop (add simp [hx.eq_iff])

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i : Fin n
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
    i.succ = 0

Tactic:
aesop (add simp [hx.eq_iff])

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i i_1 : Fin n
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i_1.succ : α) →
    i.succ = i_1.succ

Tactic:
aesop (add simp [hx.eq_iff])

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
⊢ Injective.{1, u_1 + 1} (α := Fin (n + 1)) (β := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x) ↔
    ¬x₀ ∈ Set.range x ∧ Injective x

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

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

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective.{1, u_1 + 1} (α := Fin (n + 1)) (β := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x)
i : Fin n
hi : x i = x₀
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
    i.succ = 0

Tactic:
replace h := @h i.succ 0
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
i : Fin n
hi : x i = x₀
h :
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
    i.succ = 0
⊢ False

Tactic:
simp [hi] at h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective.{1, u_1 + 1} (α := Fin (n + 1)) (β := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x)
⊢ Injective x

Tactic:
simpa [Function.comp] using h.comp (Fin.succ_injective _)

Premises used: Function.comp, Fin.succ_injective, Function.Injective.comp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
q : (i : Fin (n + 1)) → α i
⊢ ∃ (x₀ : α 0), ∃ (x : (i : Fin n) → α i.succ), q = cons (α := α) x₀ x

Tactic:
⟨q 0, tail q, (cons_self_tail q).symm⟩

Premises used: Fin.cons_self_tail, Exists.intro, OfNat.ofNat, Eq.symm, Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Fin 0 → Sort u_1
P : ((i : Fin 0) → α i) → Prop
⊢ (∀ (x : (i : Fin 0) → α i), P x) ↔ P (finZeroElim (α := α))

Tactic:
⟨fun h ↦ h _, fun h x ↦ Subsingleton.elim finZeroElim x ▸ h⟩

Premises used: finZeroElim, Eq.rec, Iff.intro, Subsingleton.elim
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Fin 0 → Sort u_1
P : ((i : Fin 0) → α i) → Prop
⊢ (∃ (x : (i : Fin 0) → α i), P x) ↔ P (finZeroElim (α := α))

Tactic:
⟨fun ⟨x, h⟩ ↦ Subsingleton.elim x finZeroElim ▸ h, fun h ↦ ⟨_, h⟩⟩

Premises used: _private.0.Fin.exists_fin_zero_pi.match_1, finZeroElim, Eq.rec, Iff.intro, Exists.intro, Subsingleton.elim
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
P : ((i : Fin (n + 1)) → α i) → Prop
⊢ (∀ (x : (i : Fin (n + 1)) → α i), P x) ↔ ∀ (a : α 0) (v : (i : Fin n) → α i.succ), P (cons (α := α) a v)

Tactic:
⟨fun h a v ↦ h (Fin.cons a v), consCases⟩

Premises used: Fin.cons, Iff.intro, Fin.consCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
P : ((i : Fin (n + 1)) → α i) → Prop
⊢ (∃ (x : (i : Fin (n + 1)) → α i), P x) ↔ ∃ (a : α 0), ∃ (v : (i : Fin n) → α i.succ), P (cons (α := α) a v)

Tactic:
⟨fun ⟨x, h⟩ ↦ ⟨x 0, tail x, (cons_self_tail x).symm ▸ h⟩, fun ⟨_, _, h⟩ ↦ ⟨_, h⟩⟩

Premises used: _private.0.Fin.exists_fin_succ_pi.match_1, Fin.cons, Exists, Eq.rec, Fin.cons_self_tail, _private.0.Fin.exists_fin_succ_pi.match_2, Iff.intro, Exists.intro, OfNat.ofNat, Eq.symm, Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
h : ∀ (j : Fin n), tail (α := α) (update (β := α) q 0 z) j = tail (α := α) q j
⊢ tail (α := α) (update (β := α) q 0 z) = tail (α := α) q

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

Tactic:
simp [tail]

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

Tactic:
ext j