awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i : Fin (m + n)
h :
  ∀ (i : Fin m),
    addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i))
        (fun (j : Fin n) ↦ v (natAdd m j)) (castAdd n i) =
      v (castAdd n i)
⊢ addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i))
      (fun (j : Fin n) ↦ v (natAdd m j)) i =
    v i
have h₁ : ∀ (i : Fin n),
  addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i))
      (fun (j : Fin n) ↦ v (natAdd m j)) (natAdd m i) =
    v (natAdd m i)
Tactic: cases i using addCases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
⊢ append xs ys ∘ Sum.elim (castAdd n) (natAdd m) = Sum.elim xs ys
have h : ∀ (i : Fin m), (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inl i) = Sum.elim xs ys (Sum.inl i)
Tactic: ext (i | j)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
h : ∀ (i : Fin m), (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inl i) = Sum.elim xs ys (Sum.inl i)
⊢ append xs ys ∘ Sum.elim (castAdd n) (natAdd m) = Sum.elim xs ys
have h₁ : ∀ (j : Fin n), (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inr j) = Sum.elim xs ys (Sum.inr j)
Tactic: ext (i | j)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin m ⊕ Fin n
⊢ (fun (i : Fin (m + n)) ↦
        (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
      (Sum.elim (castAdd n) (natAdd m) x) =
    x
have inl : ∀ (y : Fin m),
  Eq (α := Fin m ⊕ Fin n)
    ((fun (i : Fin (m + n)) ↦
        (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
      (Sum.elim (castAdd n) (natAdd m) (Sum.inl y)))
    (Sum.inl y)
Tactic: rcases x with y | y
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin m ⊕ Fin n
inl :
  ∀ (y : Fin m),
    Eq (α := Fin m ⊕ Fin n)
      ((fun (i : Fin (m + n)) ↦
          (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        (Sum.elim (castAdd n) (natAdd m) (Sum.inl y)))
      (Sum.inl y)
⊢ (fun (i : Fin (m + n)) ↦
        (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
      (Sum.elim (castAdd n) (natAdd m) x) =
    x
have inr : ∀ (y : Fin n),
  Eq (α := Fin m ⊕ Fin n)
    ((fun (i : Fin (m + n)) ↦
        (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
      (Sum.elim (castAdd n) (natAdd m) (Sum.inr y)))
    (Sum.inr y)
Tactic: rcases x with y | y
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
⊢ Sum.elim (castAdd n) (natAdd m)
      ((fun (i : Fin (m + n)) ↦
          (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        x) =
    x
have refine_1 : ∀ (i : Fin m),
  Sum.elim (castAdd n) (natAdd m)
      ((fun (i : Fin (m + n)) ↦
          (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        (castAdd n i)) =
    castAdd n i
Tactic: refine Fin.addCases (fun i => ?_) (fun i => ?_) x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
refine_1 :
  ∀ (i : Fin m),
    Sum.elim (castAdd n) (natAdd m)
        ((fun (i : Fin (m + n)) ↦
            (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
          (castAdd n i)) =
      castAdd n i
⊢ Sum.elim (castAdd n) (natAdd m)
      ((fun (i : Fin (m + n)) ↦
          (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        x) =
    x
have refine_2 : ∀ (i : Fin n),
  Sum.elim (castAdd n) (natAdd m)
      ((fun (i : Fin (m + n)) ↦
          (addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        (natAdd m i)) =
    natAdd m i
Tactic: refine Fin.addCases (fun i => ?_) (fun i => ?_) x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m),
    invFun := fun (i : Fin (m + n)) ↦ addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Injective (append xs ys) ↔ Injective xs ∧ Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j
have rw : Injective (append xs ys) ↔ Injective (Sum.elim xs ys)
Tactic: rw [← Sum.elim_injective, ← append_comp_sumElim, ← finSumFinEquiv.injective_comp,
    Equiv.coe_fn_mk]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m),
    invFun := fun (i : Fin (m + n)) ↦ addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i,
    left_inv := ⋯, right_inv := ⋯ }
rw : Injective (append xs ys) ↔ Injective (Sum.elim xs ys)
⊢ Injective (append xs ys) ↔ Injective xs ∧ Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j
have rw₁ : Injective (append xs ys) ↔ Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))
Tactic: rw [← Sum.elim_injective, ← append_comp_sumElim, ← finSumFinEquiv.injective_comp,
    Equiv.coe_fn_mk]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m),
    invFun := fun (i : Fin (m + n)) ↦ addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i,
    left_inv := ⋯, right_inv := ⋯ }
rw : Injective (append xs ys) ↔ Injective (Sum.elim xs ys)
rw₁ : Injective (append xs ys) ↔ Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))
⊢ Injective (append xs ys) ↔ Injective xs ∧ Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j
have rw₂ : Injective (α := Fin m ⊕ Fin n) (append xs ys ∘ (⇑finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))) ↔
  Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))
Tactic: rw [← Sum.elim_injective, ← append_comp_sumElim, ← finSumFinEquiv.injective_comp,
    Equiv.coe_fn_mk]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m),
    invFun := fun (i : Fin (m + n)) ↦ addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i,
    left_inv := ⋯, right_inv := ⋯ }
rw : Injective (append xs ys) ↔ Injective (Sum.elim xs ys)
rw₁ : Injective (append xs ys) ↔ Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))
rw₂ :
  Injective (α := Fin m ⊕ Fin n) (append xs ys ∘ (⇑finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))) ↔
    Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))
⊢ Injective (append xs ys) ↔ Injective xs ∧ Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j
have rw₃ : Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) ↔ Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))
Tactic: rw [← Sum.elim_injective, ← append_comp_sumElim, ← finSumFinEquiv.injective_comp,
    Equiv.coe_fn_mk]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
⊢ «repeat» 1 a = a ∘ Fin.cast ⋯
have generalize_proofs : ∀ (h : 1 * n = n), «repeat» 1 a = a ∘ Fin.cast h
Tactic: generalize_proofs h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ «repeat» 1 a = a ∘ Fin.cast h
have h₁ : ∀ (x : Fin (1 * n)), «repeat» 1 a x = (a ∘ Fin.cast h) x
Tactic: apply funext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin (1 * n)), «repeat» 1 a x = (a ∘ Fin.cast h) x
have h₁ : ∀ (x : Fin n), «repeat» 1 a (Fin.cast sorry x) = (a ∘ Fin.cast h) (Fin.cast sorry x)
Tactic: rw [(Fin.rightInverse_cast h.symm).surjective.forall]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
⊢ «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast ⋯
have generalize_proofs : ∀ (h : m.succ * n = n + m * n), «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast h
Tactic: generalize_proofs h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast h
have h₁ : ∀ (x : Fin (m.succ * n)), «repeat» m.succ a x = (append a («repeat» m a) ∘ Fin.cast h) x
Tactic: apply funext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ ∀ (x : Fin (m.succ * n)), «repeat» m.succ a x = (append a («repeat» m a) ∘ Fin.cast h) x
have h₁ : ∀ (x : Fin (n + m * n)), «repeat» m.succ a (Fin.cast sorry x) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast sorry x)
Tactic: rw [(Fin.rightInverse_cast h.symm).surjective.forall]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ ∀ (x : Fin (n + m * n)), «repeat» m.succ a (Fin.cast ⋯ x) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ x)
have h₁ : ∀ (l : Fin n),
  «repeat» m.succ a (Fin.cast sorry (castAdd (m * n) l)) =
    (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast sorry (castAdd (m * n) l))
Tactic: refine Fin.addCases (fun l => ?_) fun r => ?_
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
h₁ :
  ∀ (l : Fin n),
    «repeat» m.succ a (Fin.cast ⋯ (castAdd (m * n) l)) =
      (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m * n) l))
⊢ ∀ (x : Fin (n + m * n)), «repeat» m.succ a (Fin.cast ⋯ x) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ x)
have h₂ : ∀ (r : Fin (m * n)),
  «repeat» m.succ a (Fin.cast sorry (natAdd n r)) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast sorry (natAdd n r))
Tactic: refine Fin.addCases (fun l => ?_) fun r => ?_
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
⊢ «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast ⋯
have generalize_proofs : ∀ (h : (m₁ + m₂) * n = m₁ * n + m₂ * n), «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h
Tactic: generalize_proofs h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h
have h₁ : ∀ (x : Fin ((m₁ + m₂) * n)), «repeat» (m₁ + m₂) a x = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) x
Tactic: apply funext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin ((m₁ + m₂) * n)), «repeat» (m₁ + m₂) a x = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) x
have h₁ : ∀ (x : Fin (m₁ * n + m₂ * n)),
  «repeat» (m₁ + m₂) a (Fin.cast sorry x) = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast sorry x)
Tactic: rw [(Fin.rightInverse_cast h.symm).surjective.forall]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin (m₁ * n + m₂ * n)),
    «repeat» (m₁ + m₂) a (Fin.cast ⋯ x) = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ x)
have h₁ : ∀ (l : Fin (m₁ * n)),
  «repeat» (m₁ + m₂) a (Fin.cast sorry (castAdd (m₂ * n) l)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast sorry (castAdd (m₂ * n) l))
Tactic: refine Fin.addCases (fun l => ?_) fun r => ?_
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
h₁ :
  ∀ (l : Fin (m₁ * n)),
    «repeat» (m₁ + m₂) a (Fin.cast ⋯ (castAdd (m₂ * n) l)) =
      (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m₂ * n) l))
⊢ ∀ (x : Fin (m₁ * n + m₂ * n)),
    «repeat» (m₁ + m₂) a (Fin.cast ⋯ x) = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ x)
have h₂ : ∀ (r : Fin (m₂ * n)),
  «repeat» (m₁ + m₂) a (Fin.cast sorry (natAdd (m₁ * n) r)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast sorry (natAdd (m₁ * n) r))
Tactic: refine Fin.addCases (fun l => ?_) fun r => ?_
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Fin (n + 1) → Sort u_1
x_1 : α (last n)
q : (i : Fin (n + 1)) → α i
p_1 : (i : Fin n) → α i.castSucc
i_1 : Fin n
y : α i_1.castSucc
z : α (last n)
p : (i : Fin n) → α i.castSucc
x : α (last n)
i : Fin (n + 1)
h : (↑i : ℕ) < n
⊢ α (i.castLT h).castSucc = α i
have rw : α i = α i
Tactic: rw [Fin.castSucc_castLT i h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Fin (n + 1) → Sort u_1
x_1 : α (last n)
q : (i : Fin (n + 1)) → α i
p_1 : (i : Fin n) → α i.castSucc
i_1 : Fin n
y : α i_1.castSucc
z : α (last n)
p : (i : Fin n) → α i.castSucc
x : α (last n)
i : Fin (n + 1)
h : ¬(↑i : ℕ) < n
⊢ α (last n) = α i
have rw : α (last n) = α (last n)
Tactic: rw [eq_last_of_not_lt h]
-- 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
⊢ init (α := α) (snoc (α := α) p x) = p
have h : ∀ (i : Fin n), init (α := α) (snoc (α := α) p x) i = p i
Tactic: ext i
-- 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
i : Fin n
⊢ init (α := α) (snoc (α := α) p x) i = p i
have h : cast (α := α (i.castSucc.castLT sorry).castSucc) sorry (p (i.castSucc.castLT sorry)) = p i
Tactic: simp only [init, snoc, val_castSucc, is_lt, dite_true]
-- 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
i : Fin n
⊢ snoc (α := α) p x i.castSucc = p i
have simp : cast (α := α (i.castSucc.castLT sorry).castSucc) sorry (p (i.castSucc.castLT sorry)) = p i
Tactic: simp only [snoc, val_castSucc, is_lt, dite_true]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_2
a : α
f : Fin n → α
i : Fin n
⊢ (snoc (α := fun (a : Fin (n + 1)) ↦ α) f a ∘ castSucc) i = f i
have rw : snoc (α := fun (a : Fin (n + 1)) ↦ α) f a i.castSucc = f i
Tactic: rw [Function.comp_apply, snoc_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_2
a : α
f : Fin n → α
i : Fin n
rw : snoc (α := fun (a : Fin (n + 1)) ↦ α) f a i.castSucc = f i
⊢ (snoc (α := fun (a : Fin (n + 1)) ↦ α) f a ∘ castSucc) i = f i
have rw₁ : f i = f i
Tactic: rw [Function.comp_apply, snoc_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
⊢ Eq.{u_2} (α := Fin (n + 1) → α) (snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a ∘ natAdd m : Fin (n + 1) → α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a : (i : Fin (n + 1)) → α)
have h : ∀ (i : Fin (n + 1)),
  Eq.{u_2} (α := α) ((snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a ∘ natAdd m) i : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a i : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ Eq.{u_2} (α := α) ((snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a ∘ natAdd m) i : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a i : α)
have h : Eq.{u_2} (α := α) ((snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a ∘ natAdd m) (last n) : α)
  (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a (last n) : α)
Tactic: refine Fin.lastCases ?_ (fun i ↦ ?_) i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
h :
  Eq.{u_2} (α := α) ((snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a ∘ natAdd m) (last n) : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a (last n) : α)
⊢ Eq.{u_2} (α := α) ((snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a ∘ natAdd m) i : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a i : α)
have h₁ : ∀ (i : Fin n),
  Eq.{u_2} (α := α) ((snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a ∘ natAdd m) i.castSucc : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a i.castSucc : α)
Tactic: refine Fin.lastCases ?_ (fun i ↦ ?_) i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ Eq.{u_2} (α := α) ((snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a ∘ natAdd m) (last n) : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a (last n) : α)
have h : Eq.{u_2} (α := α) (snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m (last n)) : α)
  (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a (last n) : α)
Tactic: simp only [Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ Eq.{u_2} (α := α) (snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m (last n)) : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a (last n) : α)
have h : snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m (last n)) = a
Tactic: rw [snoc_last, natAdd_last, snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
h : snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m (last n)) = a
⊢ Eq.{u_2} (α := α) (snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m (last n)) : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a (last n) : α)
have h₁ : snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (last (m + n)) = a
Tactic: rw [snoc_last, natAdd_last, snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
h : snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m (last n)) = a
h₁ : snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (last (m + n)) = a
⊢ Eq.{u_2} (α := α) (snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m (last n)) : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a (last n) : α)
have h₂ : a = a
Tactic: rw [snoc_last, natAdd_last, snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i_1 : Fin (n + 1)
i : Fin n
⊢ Eq.{u_2} (α := α) ((snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a ∘ natAdd m) i.castSucc : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a i.castSucc : α)
have h : snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m i.castSucc) = f (natAdd m i)
Tactic: simp only [comp_apply, snoc_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i_1 : Fin (n + 1)
i : Fin n
⊢ snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m i.castSucc) = f (natAdd m i)
have h : snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m i).castSucc = f (natAdd m i)
Tactic: rw [natAdd_castSucc, snoc_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i_1 : Fin (n + 1)
i : Fin n
h : snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m i).castSucc = f (natAdd m i)
⊢ snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m i.castSucc) = f (natAdd m i)
have h₁ : f (natAdd m i) = f (natAdd m i)
Tactic: rw [natAdd_castSucc, snoc_castSucc]
-- 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
i : Fin n
y : α i.castSucc
⊢ snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x =
    update (β := α) (snoc (α := α) p x) i.castSucc y
have 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
Tactic: ext 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
i : Fin n
y : α i.castSucc
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)
have 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)
Tactic: rcases eq_or_ne j i with rfl | hne
Cleared hypotheses: i, y
-- 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
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)
⊢ 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)
have 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)
Tactic: rcases eq_or_ne j i with rfl | hne
-- 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
i : Fin n
y : α i.castSucc
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
have 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)
Tactic: cases j using lastCases with
  | cast j => rcases eq_or_ne j i with rfl | hne <;> simp [*]
  | last => simp [Ne.symm]
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
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)
⊢ snoc (α := α) (update (β := fun (i : Fin n) ↦ α i.castSucc) p i y) x j =
    update (β := α) (snoc (α := α) p x) i.castSucc y j
have 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))
Tactic: cases j using lastCases with
  | cast j => rcases eq_or_ne j i with rfl | hne <;> simp [*]
  | last => simp [Ne.symm]
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)
⊢ update (β := α) (snoc (α := α) p x) (last n) z = snoc (α := α) p z
have h : ∀ (j : Fin (n + 1)), update (β := α) (snoc (α := α) p x) (last n) z j = snoc (α := α) p z j
Tactic: ext j