awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin n
⊢ append xs ys (natAdd m i) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (natAdd m i).rev)

Tactic:
simp [cast_rev, rev_addNat]

Premises used: Fin.rev_addNat, Fin.cast_rev
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
⊢ append xs ys ∘ rev = append (ys ∘ rev) (xs ∘ rev) ∘ Fin.cast ⋯

Tactic:
funext <| append_rev xs ys

Premises used: funext, Fin.append_rev
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
f : Fin (m + n) → α
unfold :
  (fun (i : Fin (m + n)) ↦
      if hi : (↑i : ℕ) < m then
        Eq.rec (motive := fun (x : Fin (m + n)) (h : castAdd n (i.castLT hi) = x) ↦ (fun (x : Fin (m + n)) ↦ α) x)
          ((fun (i : Fin m) ↦ f (castAdd n i)) (i.castLT hi)) ⋯
      else
        Eq.rec (motive := fun (x : Fin (m + n)) (h : natAdd m (subNat m (Fin.cast ⋯ i) ⋯) = x) ↦
          (fun (x : Fin (m + n)) ↦ α) x) ((fun (i : Fin n) ↦ f (natAdd m i)) (subNat m (Fin.cast ⋯ i) ⋯)) ⋯) =
    f
⊢ (append (fun (i : Fin m) ↦ f (castAdd n i)) fun (i : Fin n) ↦ f (natAdd m i)) = f

Tactic:
unfold append addCases

Premises used: Fin.append
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
f : Fin (m + n) → α
⊢ (fun (i : Fin (m + n)) ↦
      if hi : (↑i : ℕ) < m then
        Eq.rec (motive := fun (x : Fin (m + n)) (h : castAdd n (i.castLT hi) = x) ↦ (fun (x : Fin (m + n)) ↦ α) x)
          ((fun (i : Fin m) ↦ f (castAdd n i)) (i.castLT hi)) ⋯
      else
        Eq.rec (motive := fun (x : Fin (m + n)) (h : natAdd m (subNat m (Fin.cast ⋯ i) ⋯) = x) ↦
          (fun (x : Fin (m + n)) ↦ α) x) ((fun (i : Fin n) ↦ f (natAdd m i)) (subNat m (Fin.cast ⋯ i) ⋯)) ⋯) =
    f

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
h :
  ∀ (i : Fin (m + 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)) i =
      v i
⊢ (fun (i : Fin (m + 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)) i) =
    v

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)
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)
⊢ 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

Tactic:
cases i using addCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
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)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)
h₁ : ∀ (j : Fin n), (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inr j) = Sum.elim xs ys (Sum.inr j)
⊢ append xs ys ∘ Sum.elim (castAdd n) (natAdd m) = Sum.elim xs ys

Tactic:
ext (i | j)
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
i : Fin m
⊢ (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inl i) = Sum.elim xs ys (Sum.inl i)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
j : Fin n
⊢ (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inr j) = Sum.elim xs ys (Sum.inr j)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)
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)
⊢ (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

Tactic:
rcases x with y | y
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
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

Tactic:
Fin.addCases (fun i => ?_) (fun i => ?_) x

Premises used: Fin.addCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ 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

Tactic:
refine Fin.addCases (fun i => ?_) (fun i => ?_) x
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
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))
rw₃ rw₄ :
  Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) ↔
    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

Tactic:
rw [← Sum.elim_injective, ← append_comp_sumElim, ← finSumFinEquiv.injective_comp,
    Equiv.coe_fn_mk]

Premises used: Sum.elim_injective, Equiv.injective_comp, Fin.append_comp_sumElim, Equiv.coe_fn_mk
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
a : Fin n → α
i : Fin (m * n)
⊢ «repeat» m a i = a i.modNat

Tactic:
rfl

Premises used: Fin.repeat, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
⊢ «repeat» 0 a = elim0 ∘ Fin.cast ⋯

Tactic:
funext fun x => (x.cast (Nat.zero_mul _)).elim0

Premises used: Nat.zero_mul, funext, Fin.cast, Fin.elim0
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
generalize_proofs : ∀ (h : 1 * n = n), «repeat» 1 a = a ∘ Fin.cast h
⊢ «repeat» 1 a = a ∘ Fin.cast ⋯

Tactic:
generalize_proofs h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
h₁ : ∀ (x : Fin (1 * n)), «repeat» 1 a x = (a ∘ Fin.cast h) x
⊢ «repeat» 1 a = a ∘ Fin.cast h

Tactic:
apply funext

Premises used: funext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
h₁ : ∀ (x : Fin n), «repeat» 1 a (Fin.cast ⋯ x) = (a ∘ Fin.cast h) (Fin.cast ⋯ x)
⊢ ∀ (x : Fin (1 * n)), «repeat» 1 a x = (a ∘ Fin.cast h) x

Tactic:
rw [(Fin.rightInverse_cast h.symm).surjective.forall]

Premises used: Function.Surjective.forall, Fin.rightInverse_cast, Function.RightInverse.surjective, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
i : Fin n
⊢ «repeat» 1 a (Fin.cast ⋯ i) = (a ∘ Fin.cast h) (Fin.cast ⋯ i)

Tactic:
simp [modNat, Nat.mod_eq_of_lt i.is_lt]

Premises used: Fin.is_lt, Fin.modNat, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
generalize_proofs : ∀ (h : m.succ * n = n + m * n), «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast h
⊢ «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast ⋯

Tactic:
generalize_proofs h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
h₁ : ∀ (x : Fin (m.succ * n)), «repeat» m.succ a x = (append a («repeat» m a) ∘ Fin.cast h) x
⊢ «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast h

Tactic:
apply funext

Premises used: funext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
h₁ : ∀ (x : Fin (n + m * n)), «repeat» m.succ a (Fin.cast ⋯ x) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ x)
⊢ ∀ (x : Fin (m.succ * n)), «repeat» m.succ a x = (append a («repeat» m a) ∘ Fin.cast h) x

Tactic:
rw [(Fin.rightInverse_cast h.symm).surjective.forall]

Premises used: Function.Surjective.forall, Fin.rightInverse_cast, Function.RightInverse.surjective, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)

Tactic:
Fin.addCases (fun l => ?_) fun r => ?_

Premises used: Fin.addCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
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))
h₂ :
  ∀ (r : Fin (m * n)),
    «repeat» m.succ a (Fin.cast ⋯ (natAdd n r)) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd n r))
⊢ ∀ (x : Fin (n + m * n)), «repeat» m.succ a (Fin.cast ⋯ x) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ x)

Tactic:
refine Fin.addCases (fun l => ?_) fun r => ?_
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
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))

Tactic:
simp [modNat, Nat.mod_eq_of_lt l.is_lt]

Premises used: Fin.is_lt, Fin.modNat, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
r : Fin (m * n)
⊢ «repeat» m.succ a (Fin.cast ⋯ (natAdd n r)) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd n r))

Tactic:
simp [modNat]

Premises used: Fin.modNat
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
generalize_proofs :
  ∀ (h : (m₁ + m₂) * n = m₁ * n + m₂ * n), «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h
⊢ «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast ⋯

Tactic:
generalize_proofs h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
h₁ : ∀ (x : Fin ((m₁ + m₂) * n)), «repeat» (m₁ + m₂) a x = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) x
⊢ «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h

Tactic:
apply funext

Premises used: funext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
h₁ :
  ∀ (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)
⊢ ∀ (x : Fin ((m₁ + m₂) * n)), «repeat» (m₁ + m₂) a x = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) x

Tactic:
rw [(Fin.rightInverse_cast h.symm).surjective.forall]

Premises used: Function.Surjective.forall, Fin.rightInverse_cast, Function.RightInverse.surjective, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)

Tactic:
Fin.addCases (fun l => ?_) fun r => ?_

Premises used: Fin.addCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
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))
h₂ :
  ∀ (r : Fin (m₂ * n)),
    «repeat» (m₁ + m₂) a (Fin.cast ⋯ (natAdd (m₁ * n) r)) =
      (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd (m₁ * n) r))
⊢ ∀ (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)

Tactic:
refine Fin.addCases (fun l => ?_) fun r => ?_
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
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))

Tactic:
simp [modNat]

Premises used: Fin.modNat
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
r : Fin (m₂ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (natAdd (m₁ * n) r)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd (m₁ * n) r))

Tactic:
simp [modNat, Nat.add_mod]

Premises used: Fin.modNat, Nat.add_mod
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
a : Fin n → α
k : Fin (m * n)
⊢ «repeat» m a k.rev = «repeat» m (a ∘ rev) k

Tactic:
congr_arg a k.modNat_rev

Premises used: Fin.repeat, congr_arg, Fin.modNat_rev
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
a : Fin n → α
⊢ «repeat» m a ∘ rev = «repeat» m (a ∘ rev)

Tactic:
funext <| repeat_rev a

Premises used: funext, Fin.repeat_rev
-- 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.castSucc) (init (α := α) fun (k : Fin (n + 1)) ↦ q k) fun (k : Fin n) ↦ q k.castSucc

Tactic:
rfl

Premises used: Fin.init, rfl
-- 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_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
rw rw₁ : α i = α i
⊢ α (i.castLT h).castSucc = α i

Tactic:
rw [Fin.castSucc_castLT i h]

Premises used: Fin.castSucc_castLT
-- 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_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
rw rw₁ : α (last n) = α (last n)
⊢ α (last n) = α i

Tactic:
rw [eq_last_of_not_lt h]

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

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
h : cast (α := α (i.castSucc.castLT ⋯).castSucc) ⋯ (p (i.castSucc.castLT ⋯)) = p i
⊢ init (α := α) (snoc (α := α) p x) i = p i

Tactic:
simp only [init, snoc, val_castSucc, is_lt, dite_true]

Premises used: Fin.snoc, Fin.is_lt, Fin.init, dite_true, Fin.val_castSucc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ cast ⋯ (p i) = p i

Tactic:
cast_eq rfl (p i)

Premises used: cast_eq, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ cast (α := α (i.castSucc.castLT ⋯).castSucc) ⋯ (p (i.castSucc.castLT ⋯)) = p i

Tactic:
convert! cast_eq rfl (p i)

Premises used: cast_eq, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
simp : cast (α := α (i.castSucc.castLT ⋯).castSucc) ⋯ (p (i.castSucc.castLT ⋯)) = p i
⊢ snoc (α := α) p x i.castSucc = p i

Tactic:
simp only [snoc, val_castSucc, is_lt, dite_true]

Premises used: Fin.snoc, Fin.is_lt, dite_true, Fin.val_castSucc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
inst : NeZero n
⊢ Eq (α := α 0) (snoc (α := α) p x 0 : α 0) (p 0 : α (castSucc 0))

Tactic:
snoc_castSucc x p 0

Premises used: Fin.snoc_castSucc, Fin.ofNat, Nat.mod, OfNat.ofNat
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
rw₁ rw₂ : f i = f i
⊢ (snoc (α := fun (a : Fin (n + 1)) ↦ α) f a ∘ castSucc) i = f i

Tactic:
rw [Function.comp_apply, snoc_castSucc]

Premises used: Fin.snoc_castSucc, Function.comp_apply
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
⊢ snoc (α := α) p x (last n) = x

Tactic:
simp [snoc]

Premises used: Fin.snoc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_2
p : Fin 0 → α
x : α
⊢ Eq.{u_2} (α := (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) → α) (snoc (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) p x)
    fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x

Tactic:
rfl

Premises used: cast, Fin.snoc, dite, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
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 : α)
⊢ 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)) → α)

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
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 : α)

Tactic:
Fin.lastCases ?_ (fun i ↦ ?_) i

Premises used: Fin.lastCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
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) : α)
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 : α)
⊢ 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:
refine Fin.lastCases ?_ (fun i ↦ ?_) i
-- Module: Mathlib.Data.Fin.Tuple.Basic
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) (last n) : α)
    (snoc (α := fun (i : Fin (n + 1)) ↦ α) (f ∘ natAdd m) a (last n) : α)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
h₂ h₃ : a = 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) : α)

Tactic:
rw [snoc_last, natAdd_last, snoc_last]

Premises used: Fin.natAdd_last, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)
⊢ 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:
simp only [comp_apply, snoc_castSucc]

Premises used: Fin.snoc_castSucc, Function.comp_apply
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)
h₁ h₂ : f (natAdd m i) = f (natAdd m i)
⊢ snoc (α := fun (a : Fin (m + n + 1)) ↦ α) f a (natAdd m i.castSucc) = f (natAdd m i)

Tactic:
rw [natAdd_castSucc, snoc_castSucc]

Premises used: Fin.snoc_castSucc, Fin.natAdd_castSucc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Fin (n + m + 1) → Sort u_2
f : (i : Fin (n + m)) → α i.castSucc
a : α (last (n + m))
i : Fin n
⊢ Eq (α := α (castAdd (m + 1) i)) (snoc (α := α) f a (castAdd (m + 1) i) : α (castAdd (m + 1) i))
    (f (castAdd m i) : α (castAdd m i).castSucc)

Tactic:
dif_pos _

Premises used: cast, dif_pos, Fin.snoc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n m : ℕ
α : Sort u_2
f : Fin (n + m) → α
a : α
⊢ snoc (α := fun (a : Fin (n + m + 1)) ↦ α) f a ∘ castAdd (m + 1) = f ∘ castAdd m

Tactic:
funext (snoc_castAdd _ _)

Premises used: funext, Fin.snoc_castAdd