awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
j : Fin n
pos :
  ∀ (h : j = i),
    tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j
neg :
  ∀ (h : ¬j = i),
    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) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j

Tactic:
by_cases h : j = i
-- 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
j : Fin n
h : j = i
pos : tail (α := α) (update (β := α) q i.succ y) i = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y i
⊢ tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j

Tactic:
rw [h]
-- 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
j : Fin n
h : j = i
⊢ tail (α := α) (update (β := α) q i.succ y) i = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y i

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
j : Fin n
h : ¬j = i
⊢ tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j

Tactic:
simp [tail, (Fin.succ_injective n).ne h, h]

Premises used: Function.Injective.ne, Fin.succ_injective, Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
h :
  ∀ (j : Fin (n + 1)),
    (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
⊢ Eq (α := Fin (n + 1) → β) (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q)
    (cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q))

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
pos :
  ∀ (h : j = 0),
    (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
neg :
  ∀ (h : ¬j = 0),
    (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j

Tactic:
by_cases h : j = 0
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
pos :
  comp (α := Fin (n + 1)) g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q) 0 =
    cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) 0
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j

Tactic:
rw [h]
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ comp (α := Fin (n + 1)) g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q) 0 =
    cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) 0

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ j'.succ = j

Tactic:
have : j'.succ = j := succ_pred j h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
neg :
  (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j'.succ
neg₁ : (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = (g ∘ q) j'
neg₂ : g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q j'.succ) = (g ∘ q) j'
neg₃ : g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q j'.succ) = g (q j')
neg₄ neg₅ : g (q j') = g (q j')
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j

Tactic:
rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]

Premises used: Fin.cons_succ, Function.comp_apply
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
h : ∀ (j : Fin n), (g ∘ tail (α := fun (i : Fin (n + 1)) ↦ α) q) j = tail (α := fun (a : Fin (n + 1)) ↦ β) (g ∘ q) j
⊢ g ∘ tail (α := fun (i : Fin (n + 1)) ↦ α) q = tail (α := fun (a : Fin (n + 1)) ↦ β) (g ∘ q)

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

Tactic:
simp [tail]

Premises used: Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (i : Fin (n + 1)) → Preorder (α i)
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
j : Fin n
⊢ LE.le (α := α j.succ) (q j.succ) (cons (α := α) x p j.succ) ↔ tail (α := α) q j ≤ p j

Tactic:
simp [tail]

Premises used: Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (i : Fin (n + 1)) → Preorder (α i)
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
⊢ cons (α := α) x p ≤ q ↔ x ≤ q 0 ∧ p ≤ tail (α := α) q

Tactic:
@le_cons _ (fun i ↦ (α i)ᵒᵈ) _ x q p

Premises used: Fin.le_cons, OrderDual
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (i : Fin (n + 1)) → Preorder (α i)
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
⊢ (∀ (i : Fin n), LE.le (α := α i.succ) (cons (α := α) x₀ x i.succ) (cons (α := α) y₀ y i.succ)) ↔ x ≤ y

Tactic:
simp only [cons_succ, Pi.le_def]

Premises used: Fin.cons_succ, Pi.le_def
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_1
f : Fin (n + 1) → α
⊢ Set.range f = insert (f 0) (Set.range (tail (α := fun (i : Fin (n + 1)) ↦ α) f))

Tactic:
Set.ext fun _ ↦ exists_fin_succ.trans <| eq_comm.or Iff.rfl

Premises used: Set.ext, Iff.rfl, eq_comm, Iff.or, Iff.trans, Fin.exists_fin_succ
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Type u_1
n : ℕ
x : α
b : Fin n → α
rw :
  insert (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x b 0 : α)
      (Set.range (ι := Fin n) (tail (α := fun (i : Fin (n + 1)) ↦ α) (cons (α := fun (a : Fin n.succ) ↦ α) x b))) =
    insert x (Set.range b)
rw₁ :
  insert x (Set.range (ι := Fin n) (tail (α := fun (i : Fin (n + 1)) ↦ α) (cons (α := fun (a : Fin n.succ) ↦ α) x b))) =
    insert x (Set.range b)
rw₂ rw₃ : insert x (Set.range b) = insert x (Set.range b)
⊢ Set.range (ι := Fin (n + 1)) (cons (α := fun (a : Fin n.succ) ↦ α) x b) = insert x (Set.range b)

Tactic:
rw [range_fin_succ, cons_zero, tail_cons]

Premises used: Fin.range_fin_succ, Fin.cons_zero, Fin.tail_cons
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
i : Fin m
⊢ append u v (castAdd n i) = u i

Tactic:
addCases_left _

Premises used: Fin.addCases_left, Fin.append
-- 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_1 : Fin n
y : α_1 i_1.succ
z : α_1 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
i : Fin m
⊢ m ≤ m + n

Tactic:
lia
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
i : Fin m
⊢ append u v (castLE ⋯ i) = u i

Tactic:
addCases_left _

Premises used: Fin.addCases_left, Fin.append
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
i : Fin n
⊢ append u v (natAdd m i) = v i

Tactic:
addCases_right _

Premises used: Fin.addCases_right, Fin.append
-- 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
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
rw : m + 0 = m
rw₁ rw₂ : m = m
⊢ m + n = m

Tactic:
rw [hv, Nat.add_zero]

Premises used: Nat.add_zero
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ append u v = u ∘ Fin.cast ⋯

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

Premises used: Fin.addCases, funext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
refine_1 : ∀ (l : Fin m), append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)
refine_2 : ∀ (r : Fin n), append u v (natAdd m r) = (u ∘ Fin.cast ⋯) (natAdd m r)
⊢ append u v = u ∘ Fin.cast ⋯

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

Premises used: Fin.addCases, funext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
refine_1 : u l = u (Fin.cast ⋯ (castAdd n l))
⊢ append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)

Tactic:
rw [append_left, Function.comp_apply]

Premises used: Fin.append_left, Function.comp_apply
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (Fin.cast ⋯ (castAdd n l))

Tactic:
congr_arg u (Fin.ext ?_)

Premises used: Fin.ext, congr_arg
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
refine_1 : (↑l : ℕ) = (↑(Fin.cast ⋯ (castAdd n l)) : ℕ)
⊢ u l = u (Fin.cast ⋯ (castAdd n l))

Tactic:
refine congr_arg u (Fin.ext ?_)

Premises used: Fin.ext, congr_arg
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ (↑l : ℕ) = (↑(Fin.cast ⋯ (castAdd n l)) : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
r : Fin n
⊢ append u v (natAdd m r) = (u ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
(Fin.cast hv r).elim0

Premises used: Fin.cast, Fin.elim0
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
r : Fin n
⊢ append u v (natAdd m r) = (u ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
exact (Fin.cast hv r).elim0

Premises used: Fin.cast, Fin.elim0
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m : ℕ
α : Sort u_1
u : Fin m → α
⊢ append u elim0 = u ∘ Fin.cast ⋯

Tactic:
append_right_nil _ _ rfl

Premises used: Fin.append_right_nil, rfl
-- 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
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
rw : 0 + n = n
rw₁ rw₂ : n = n
⊢ m + n = n

Tactic:
rw [hu, Nat.zero_add]

Premises used: Nat.zero_add
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ append u v = v ∘ Fin.cast ⋯

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

Premises used: Fin.addCases, funext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
refine_1 : ∀ (l : Fin m), append u v (castAdd n l) = (v ∘ Fin.cast ⋯) (castAdd n l)
refine_2 : ∀ (r : Fin n), append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)
⊢ append u v = v ∘ Fin.cast ⋯

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

Premises used: Fin.addCases, funext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
l : Fin m
⊢ append u v (castAdd n l) = (v ∘ Fin.cast ⋯) (castAdd n l)

Tactic:
(Fin.cast hu l).elim0

Premises used: Fin.cast, Fin.elim0
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
l : Fin m
⊢ append u v (castAdd n l) = (v ∘ Fin.cast ⋯) (castAdd n l)

Tactic:
exact (Fin.cast hu l).elim0

Premises used: Fin.cast, Fin.elim0
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
refine_2 : v r = v (Fin.cast ⋯ (natAdd m r))
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
rw [append_right, Function.comp_apply]

Premises used: Fin.append_right, Function.comp_apply
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (Fin.cast ⋯ (natAdd m r))

Tactic:
congr_arg v (Fin.ext ?_)

Premises used: Fin.ext, congr_arg
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
refine_2 : (↑r : ℕ) = (↑(Fin.cast ⋯ (natAdd m r)) : ℕ)
⊢ v r = v (Fin.cast ⋯ (natAdd m r))

Tactic:
refine congr_arg v (Fin.ext ?_)

Premises used: Fin.ext, congr_arg
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ (↑r : ℕ) = (↑(Fin.cast ⋯ (natAdd m r)) : ℕ)

Tactic:
simp [hu]
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
v : Fin n → α
⊢ append elim0 v = v ∘ Fin.cast ⋯

Tactic:
append_left_nil _ _ rfl

Premises used: Fin.append_left_nil, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
h : ∀ (i : Fin (m + n + p)), append (append a b) c i = (append a (append b c) ∘ Fin.cast ⋯) i
⊢ append (append a b) c = append a (append b c) ∘ Fin.cast ⋯

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
h : append (append a b) c i = append a (append b c) (Fin.cast ⋯ i)
⊢ append (append a b) c i = (append a (append b c) ∘ Fin.cast ⋯) i

Tactic:
rw [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = append a (append b c) (Fin.cast ⋯ i)

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

Premises used: Fin.addCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
h : ∀ (l : Fin (m + n)), append (append a b) c (castAdd p l) = append a (append b c) (Fin.cast ⋯ (castAdd p l))
h₁ : ∀ (r : Fin p), append (append a b) c (natAdd (m + n) r) = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))
⊢ append (append a b) c i = append a (append b c) (Fin.cast ⋯ i)

Tactic:
refine Fin.addCases (fun l => ?_) (fun r => ?_) i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
h : append a b l = append a (append b c) (Fin.cast ⋯ (castAdd p l))
⊢ append (append a b) c (castAdd p l) = append a (append b c) (Fin.cast ⋯ (castAdd p l))

Tactic:
rw [append_left]

Premises used: Fin.append_left
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
⊢ append a b l = append a (append b c) (Fin.cast ⋯ (castAdd p l))

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

Premises used: Fin.addCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
h : ∀ (ll : Fin m), append a b (castAdd n ll) = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))
h₁ : ∀ (lr : Fin n), append a b (natAdd m lr) = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))
⊢ append a b l = append a (append b c) (Fin.cast ⋯ (castAdd p l))

Tactic:
refine Fin.addCases (fun ll => ?_) (fun lr => ?_) l
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
h : a ll = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))
⊢ append a b (castAdd n ll) = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))

Tactic:
rw [append_left]

Premises used: Fin.append_left
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
⊢ a ll = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))

Tactic:
simp [castAdd_castAdd]

Premises used: Fin.castAdd_castAdd
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
h : b lr = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))
⊢ append a b (natAdd m lr) = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))

Tactic:
rw [append_right]

Premises used: Fin.append_right
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ b lr = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))

Tactic:
simp [castAdd_natAdd]

Premises used: Fin.castAdd_natAdd
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
h : c r = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))
⊢ append (append a b) c (natAdd (m + n) r) = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))

Tactic:
rw [append_right]

Premises used: Fin.append_right
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ c r = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))

Tactic:
simp [← natAdd_natAdd]

Premises used: Fin.natAdd_natAdd
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
h : ∀ (i : Fin (1 + n)), append x₀ x i = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) i
⊢ append x₀ x = cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ append x₀ x i = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) i

Tactic:
Fin.addCases ?_ ?_ i

Premises used: Fin.addCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
h :
  ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)
h₁ :
  ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)
⊢ append x₀ x i = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) i

Tactic:
refine Fin.addCases ?_ ?_ i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
h : cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x (Fin.cast ⋯ (castAdd n 0)) = x₀ 0
⊢ append x₀ x (castAdd n i) = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)

Tactic:
rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]

Premises used: eq_comm, Fin.append_left, Function.comp_apply, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x (Fin.cast ⋯ (castAdd n 0)) = x₀ 0

Tactic:
Fin.cons_zero _ _

Premises used: Fin.ofNat, Nat.mod, Fin.cons_zero
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x (Fin.cast ⋯ (castAdd n 0)) = x₀ 0

Tactic:
exact Fin.cons_zero _ _

Premises used: Fin.cons_zero
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
h : cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x i.succ = x i
⊢ append x₀ x (natAdd 1 i) = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)

Tactic:
rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]

Premises used: Fin.addNat_one, Fin.append_right, eq_comm, Fin.cast_natAdd, Function.comp_apply
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x i.succ = x i

Tactic:
Fin.cons_succ _ _ _

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

Tactic:
exact Fin.cons_succ _ _ _

Premises used: Fin.cons_succ
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
h :
  ∀ (i : Fin (n + 1)),
    cons (α := fun (a : Fin (n + HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x xs i =
      (append (cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x elim0) xs ∘ Fin.cast ⋯) i
⊢ cons (α := fun (a : Fin (n + HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x xs =
    append (cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x elim0) xs ∘ Fin.cast ⋯

Tactic:
funext i
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
i : Fin (n + 1)
⊢ cons (α := fun (a : Fin (n + HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x xs i =
    (append (cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x elim0) xs ∘ Fin.cast ⋯) i

Tactic:
simp [append_left_eq_cons]

Premises used: Fin.append_left_eq_cons
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m_1 n_1 : ℕ
α_1 : Fin (n_1 + 1) → Sort u
x : α_1 0
q : (i : Fin (n_1 + 1)) → α_1 i
p : (i : Fin n_1) → α_1 i.succ
i : Fin n_1
y : α_1 i.succ
z : α_1 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
rw rw₁ : n + m = n + m
⊢ n' + m = n + m

Tactic:
rw [h]
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
subst : ∀ (xs : Fin n' → α), append (xs ∘ Fin.cast ⋯) ys = append xs ys ∘ Fin.cast ⋯
⊢ append (xs ∘ Fin.cast h) ys = append xs ys ∘ Fin.cast ⋯

Tactic:
subst h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
m : ℕ
ys : Fin m → α
n' : ℕ
xs : Fin n' → α
⊢ append (xs ∘ Fin.cast ⋯) ys = append xs ys ∘ Fin.cast ⋯

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m_1 n_1 : ℕ
α_1 : Fin (n_1 + 1) → Sort u
x : α_1 0
q : (i : Fin (n_1 + 1)) → α_1 i
p : (i : Fin n_1) → α_1 i.succ
i : Fin n_1
y : α_1 i.succ
z : α_1 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
rw rw₁ : n + m = n + m
⊢ n + m' = n + m

Tactic:
rw [h]
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
subst : ∀ (ys : Fin m' → α), append xs (ys ∘ Fin.cast ⋯) = append xs ys ∘ Fin.cast ⋯
⊢ append xs (ys ∘ Fin.cast h) = append xs ys ∘ Fin.cast ⋯

Tactic:
subst h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
n : ℕ
xs : Fin n → α
m' : ℕ
ys : Fin m' → α
⊢ append xs (ys ∘ Fin.cast ⋯) = append xs ys ∘ Fin.cast ⋯

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
rcases : ∀ (i : Fin (m + n)), append xs ys i.rev.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)
⊢ append xs ys i.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i)

Tactic:
rcases rev_surjective i with ⟨i, rfl⟩

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

Tactic:
rw [rev_rev]

Premises used: Fin.rev_rev
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
left : ∀ (i : Fin m), append xs ys (castAdd n i) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (castAdd n i).rev)
right : ∀ (i : Fin n), append xs ys (natAdd m i) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (natAdd m i).rev)
⊢ append xs ys i = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)

Tactic:
induction i using Fin.addCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin m
⊢ append xs ys (castAdd n i) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (castAdd n i).rev)

Tactic:
simp [rev_castAdd]

Premises used: Fin.rev_castAdd