awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
⊢ update (β := α) (snoc (α := α) p x) (last n) z j = snoc (α := α) p z j
have h : Eq (α := α (last n)) (update (β := α) (snoc (α := α) p x) (last n) z (last n)) (snoc (α := α) p z (last n))
Tactic: cases j using lastCases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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))
⊢ update (β := α) (snoc (α := α) p x) (last n) z j = snoc (α := α) p z j
have h₁ : ∀ (i : Fin n),
  Eq (α := α i.castSucc) (update (β := α) (snoc (α := α) p x) (last n) z i.castSucc) (snoc (α := α) p z i.castSucc)
Tactic: cases j using lastCases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_2
f : Fin n → α
x : α
⊢ Set.range (ι := Fin (n + 1)) (snoc (α := fun (a : Fin (n + 1)) ↦ α) f x) = insert x (Set.range f)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
⊢ snoc (α := α) (init (α := α) q) (q (last n)) = q
have h : ∀ (j : Fin (n + 1)), snoc (α := α) (init (α := α) q) (q (last n)) j = q j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ snoc (α := α) (init (α := α) q) (q (last n)) j = q j
have h : Eq (α := α (last n)) (snoc (α := α) (init (α := α) q) (q (last n)) (last n)) (q (last n))
Tactic: cases j using Fin.lastCases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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))
⊢ snoc (α := α) (init (α := α) q) (q (last n)) j = q j
have h₁ : ∀ (i : Fin n), Eq (α := α i.castSucc) (snoc (α := α) (init (α := α) q) (q (last n)) i.castSucc) (q i.castSucc)
Tactic: cases j using Fin.lastCases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
⊢ init (α := α) (update (β := α) q (last n) z) = init (α := α) q
have h : ∀ (j : Fin n), init (α := α) (update (β := α) q (last n) z) j = init (α := α) q j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
⊢ init (α := α) (update (β := α) q i.castSucc y) = update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y
have h : ∀ (j : Fin n),
  init (α := α) (update (β := α) q i.castSucc y) j =
    update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
⊢ init (α := α) (update (β := α) q i.castSucc y) j =
    update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y j
have pos : ∀ (h : j = i),
  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
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ init (α := α) (update (β := α) q i.castSucc y) j =
    update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y j
have neg : ∀ (h : ¬j = i),
  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
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
have pos : init (α := α) (update (β := α) q i.castSucc y) i = update (β := fun (a : Fin n) ↦ α a.castSucc) (init (α := α) q) i y i
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
⊢ 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)
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
⊢ 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)
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
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)
have 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 : β)
Tactic: rw [cons_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
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)
have 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)
Tactic: cases j using Fin.lastCases with
    | last => simp
    | cast j =>
      rw [cons_succ]
      simp [← castSucc_succ]
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: cases j using Fin.lastCases with
    | last => simp
    | cast j =>
      rw [cons_succ]
      simp [← castSucc_succ]
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
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)
have 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 : β)
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]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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 : β)
⊢ 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)
have 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)
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]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
⊢ Eq (α := Fin (n + 1) → β) (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y)
    (snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y))
have 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
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
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
have 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
Tactic: by_cases h : j.val < n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) j = snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) j
have 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
Tactic: by_cases h : j.val < n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
have neg : (g ∘ snoc (α := fun (a : Fin (n + 1)) ↦ α) q y) (last n) = snoc (α := fun (i : Fin (n + 1)) ↦ β) (g ∘ q) (g y) (last n)
Tactic: rw [eq_last_of_not_lt h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ append x x₀ = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0)
have h : ∀ (i : Fin (n + 1)), append x x₀ i = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
have h : ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (castAdd 1 i)
Tactic: refine Fin.addCases ?_ ?_ i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
⊢ append x x₀ i = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) i
have h₁ : ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (natAdd n i)
Tactic: refine Fin.addCases ?_ ?_ i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ append x x₀ (castAdd 1 i) = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (castAdd 1 i)
have h : x i = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (castAdd 1 i)
Tactic: rw [Fin.append_left]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ append x x₀ (natAdd n i) = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (natAdd n i)
have h : x₀ 0 = snoc (α := fun (i : Fin (n + 1)) ↦ α) x (x₀ 0) (natAdd n 0)
Tactic: rw [Subsingleton.elim i 0, Fin.append_right]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ append (snoc (α := fun (a : Fin (n + 1)) ↦ α) xs x) ys =
    append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) x ys) ∘ Fin.cast ⋯
have rw : (append xs
        (cons (α := fun (a : Fin (m + 1)) ↦ α) (cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x elim0 0) ys) ∘
      Fin.cast sorry) ∘
    Fin.cast sorry =
  append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) x ys) ∘ Fin.cast sorry
Tactic: rw [snoc_eq_append, append_assoc, append_left_eq_cons, append_cast_right]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) y ys) =
    append (snoc (α := fun (a : Fin (n + 1)) ↦ α) xs y) ys ∘ Fin.cast ⋯
have rw : append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) y ys) =
  (append xs (cons (α := fun (a : Fin (m + 1)) ↦ α) y ys) ∘ Fin.cast sorry) ∘ Fin.cast sorry
Tactic: rw [append_left_snoc]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
⊢ append (cons (α := fun (a : Fin (n + 1)) ↦ α) a as) bs =
    cons (α := fun (a : Fin (n + m + 1)) ↦ α) a (append as bs) ∘ Fin.cast ⋯
have 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 sorry) i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
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
have 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 sorry) (⟨i, isLt⟩ : Fin (n + 1 + m))
Tactic: rcases i with ⟨i, -⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
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))
have h : Eq.{u_2} (α := α)
  (if h : i < n + 1 then cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨i, sorry⟩ : Fin (n + 1))
    else
      @Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast sorry (⟨i, isLt⟩ : Fin (n + 1 + m))) sorry))
        (fun (x : Fin (n + 1 + m))
            (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast sorry (⟨i, isLt⟩ : Fin (n + 1 + m))) sorry) = x) ↦
          α)
        (bs (subNat (n + 1) (Fin.cast sorry (⟨i, isLt⟩ : Fin (n + 1 + m))) sorry)) _ sorry :
    α)
  (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
      (Fin.cast sorry (⟨i, isLt⟩ : Fin (n + 1 + m))) :
    α)
Tactic: simp only [append, addCases, cons, castLT, comp_apply]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i < 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))) :
      α)
have 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, sorry⟩ : Fin (n + 1))
      else
        @Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast sorry (⟨0, isLt⟩ : Fin (n + 1 + m))) sorry))
          (fun (x : Fin (n + 1 + m))
              (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast sorry (⟨0, isLt⟩ : Fin (n + 1 + m))) sorry) = x) ↦
            α)
          (bs (subNat (n + 1) (Fin.cast sorry (⟨0, isLt⟩ : Fin (n + 1 + m))) sorry)) _ sorry :
      α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast sorry (⟨0, isLt⟩ : Fin (n + 1 + m))) :
      α)
Tactic: rcases i with - | i
Cleared hypotheses: i, isLt
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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))) :
        α)
⊢ 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))) :
      α)
have 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, sorry⟩ : Fin (n + 1))
      else
        @Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast sorry (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) sorry))
          (fun (x : Fin (n + 1 + m))
              (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast sorry (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) sorry) = x) ↦
            α)
          (bs (subNat (n + 1) (Fin.cast sorry (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) sorry)) _ sorry :
      α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast sorry (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
      α)
Tactic: rcases i with - | i
Cleared hypotheses: i, isLt
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
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))) :
      α)
have pos : ∀ (h : i + 1 < n + 1),
  Eq.{u_2} (α := α) (cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨i + 1, sorry⟩ : Fin (n + 1)) : α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast sorry (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
      α)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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))) :
        α)
⊢ 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))) :
      α)
have neg : ∀ (h : ¬i + 1 < n + 1),
  Eq.{u_2} (α := α)
    (@Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast sorry (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) sorry))
        (fun (x : Fin (n + 1 + m))
            (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast sorry (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) sorry) = x) ↦
          α)
        (bs (subNat (n + 1) (Fin.cast sorry (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) sorry)) _ sorry :
      α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast sorry (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
      α)
Tactic: split_ifs with h