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₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ repeat (m₁ + m₂) a = append (repeat m₁ 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₁ m₂ : ℕ
⊢ repeat (m₁ + m₂) a = append (repeat m₁ a) (repeat m₂ a) ∘ ↑(cast (_ : (m₁ + m₂) * n = m₁ * 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₁ 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) ∘ ↑(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₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ repeat (m₁ + m₂) a = append (repeat m₁ 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₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin (m₁ * n + m₂ * n)),
    repeat (m₁ + m₂) a (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) x) =
      (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(cast h)) (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + 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₁ 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) ∘ ↑(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₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
l : Fin (m₁ * n)
⊢ repeat (m₁ + m₂) a (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (↑(castAdd (m₂ * n)) l)) =
    (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(cast h))
      (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + 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₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
r : Fin (m₂ * n)
⊢ repeat (m₁ + m₂) a (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (↑(natAdd (m₁ * n)) r)) =
    (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(cast h))
      (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (↑(natAdd (m₁ * 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₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin (m₁ * n + m₂ * n)),
    repeat (m₁ + m₂) a (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) x) =
      (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(cast h)) (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + 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₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
l : Fin (m₁ * n)
⊢ repeat (m₁ + m₂) a (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (↑(castAdd (m₂ * n)) l)) =
    (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(cast h))
      (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + 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₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
r : Fin (m₂ * n)
⊢ repeat (m₁ + m₂) a (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (↑(natAdd (m₁ * n)) r)) =
    (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(cast h))
      (↑(cast (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (↑(natAdd (m₁ * n)) r))
simp [modNat, Nat.add_mod]