m n : ℕ
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : ai = bi
h : { fst := ai, snd := a }.snd = { fst := bi, snd := b }.snd ∘ ↑(cast hi)
⊢ { fst := ai, snd := a } = { fst := bi, snd := b }
m n : ℕ
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : { fst := ai, snd := a }.fst = { fst := bi, snd := b }.fst
h : { fst := ai, snd := a }.snd = { fst := bi, snd := b }.snd ∘ ↑(cast hi)
⊢ { fst := ai, snd := a } = { fst := bi, snd := b }
dsimp only at hi
m n : ℕ
α : Type u_1
ai : ℕ
a b : Fin ai → α
h : { fst := ai, snd := a }.snd = { fst := ai, snd := b }.snd ∘ ↑(cast (_ : ai = ai))
⊢ { fst := ai, snd := a } = { fst := ai, snd := b }
m n : ℕ
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : ai = bi
h : { fst := ai, snd := a }.snd = { fst := bi, snd := b }.snd ∘ ↑(cast hi)
⊢ { fst := ai, snd := a } = { fst := bi, snd := b }
subst hi
no goals
m n : ℕ
α : Type u_1
ai : ℕ
a b : Fin ai → α
h : { fst := ai, snd := a }.snd = { fst := ai, snd := b }.snd ∘ ↑(cast (_ : ai = ai))
⊢ { fst := ai, snd := a } = { fst := ai, snd := b }
simpa using h