m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
⊢ repeat (Nat.succ m) a = append a (repeat m a) ∘ ↑(cast h)
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
⊢ repeat (Nat.succ m) a = append a (repeat m a) ∘ ↑(cast (_ : Nat.succ m * n = n + m * n))
generalize_proofs h
case h
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
⊢ ∀ (x : Fin (Nat.succ m * n)), repeat (Nat.succ m) a x = (append a (repeat m a) ∘ ↑(cast h)) x
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
⊢ repeat (Nat.succ m) a = append a (repeat m a) ∘ ↑(cast h)
apply funext
case h
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
⊢ ∀ (x : Fin (n + m * n)),
    repeat (Nat.succ m) a (↑(cast (_ : n + m * n = Nat.succ m * n)) x) =
      (append a (repeat m a) ∘ ↑(cast h)) (↑(cast (_ : n + m * n = Nat.succ m * n)) x)
case h
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
⊢ ∀ (x : Fin (Nat.succ m * n)), repeat (Nat.succ m) a x = (append a (repeat m a) ∘ ↑(cast h)) x
rw [(Fin.cast h.symm).surjective.forall]
case h.refine'_1
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
l : Fin n
⊢ repeat (Nat.succ m) a (↑(cast (_ : n + m * n = Nat.succ m * n)) (↑(castAdd (m * n)) l)) =
    (append a (repeat m a) ∘ ↑(cast h)) (↑(cast (_ : n + m * n = Nat.succ m * n)) (↑(castAdd (m * n)) l))

case h.refine'_2
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
r : Fin (m * n)
⊢ repeat (Nat.succ m) a (↑(cast (_ : n + m * n = Nat.succ m * n)) (↑(natAdd n) r)) =
    (append a (repeat m a) ∘ ↑(cast h)) (↑(cast (_ : n + m * n = Nat.succ m * n)) (↑(natAdd n) r))
case h
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
⊢ ∀ (x : Fin (n + m * n)),
    repeat (Nat.succ m) a (↑(cast (_ : n + m * n = Nat.succ m * n)) x) =
      (append a (repeat m a) ∘ ↑(cast h)) (↑(cast (_ : n + m * n = Nat.succ m * n)) x)
refine' Fin.addCases (fun l => _) fun r => _
no goals
case h.refine'_1
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
l : Fin n
⊢ repeat (Nat.succ m) a (↑(cast (_ : n + m * n = Nat.succ m * n)) (↑(castAdd (m * n)) l)) =
    (append a (repeat m a) ∘ ↑(cast h)) (↑(cast (_ : n + m * n = Nat.succ m * n)) (↑(castAdd (m * n)) l))
simp [modNat, Nat.mod_eq_of_lt l.is_lt]
no goals
case h.refine'_2
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
r : Fin (m * n)
⊢ repeat (Nat.succ m) a (↑(cast (_ : n + m * n = Nat.succ m * n)) (↑(natAdd n) r)) =
    (append a (repeat m a) ∘ ↑(cast h)) (↑(cast (_ : n + m * n = Nat.succ m * n)) (↑(natAdd n) r))
simp [modNat]