[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
⊢ map valEmbedding univ = Iio n
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
n a✝ : ℕ
⊢ a✝ ∈ map valEmbedding univ ↔ a✝ ∈ Iio n
[PROOFSTEP]
simp [orderIsoSubtype.symm.surjective.exists, OrderIso.symm]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
⊢ Ioi 0 = map (succEmbedding n).toEmbedding univ
[PROOFSTEP]
ext i
[GOAL]
case a
α : Type u_1
β : Type u_2
n : ℕ
i : Fin (Nat.succ n)
⊢ i ∈ Ioi 0 ↔ i ∈ map (succEmbedding n).toEmbedding univ
[PROOFSTEP]
simp only [mem_Ioi, mem_map, mem_univ, Function.Embedding.coeFn_mk, exists_true_left]
[GOAL]
case a
α : Type u_1
β : Type u_2
n : ℕ
i : Fin (Nat.succ n)
⊢ 0 < i ↔ ∃ a, True ∧ ↑(succEmbedding n).toEmbedding a = i
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
β : Type u_2
n : ℕ
i : Fin (Nat.succ n)
⊢ 0 < i → ∃ a, True ∧ ↑(succEmbedding n).toEmbedding a = i
[PROOFSTEP]
refine' cases _ _ i
[GOAL]
case a.mp.refine'_1
α : Type u_1
β : Type u_2
n : ℕ
i : Fin (Nat.succ n)
⊢ 0 < 0 → ∃ a, True ∧ ↑(succEmbedding n).toEmbedding a = 0
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case a.mp.refine'_2
α : Type u_1
β : Type u_2
n : ℕ
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), 0 < succ i → ∃ a, True ∧ ↑(succEmbedding n).toEmbedding a = succ i
[PROOFSTEP]
intro j _
[GOAL]
case a.mp.refine'_2
α : Type u_1
β : Type u_2
n : ℕ
i : Fin (Nat.succ n)
j : Fin n
a✝ : 0 < succ j
⊢ ∃ a, True ∧ ↑(succEmbedding n).toEmbedding a = succ j
[PROOFSTEP]
use j
[GOAL]
case h
α : Type u_1
β : Type u_2
n : ℕ
i : Fin (Nat.succ n)
j : Fin n
a✝ : 0 < succ j
⊢ True ∧ ↑(succEmbedding n).toEmbedding j = succ j
[PROOFSTEP]
simp only [val_succEmbedding, and_self, RelEmbedding.coe_toEmbedding]
[GOAL]
case a.mpr
α : Type u_1
β : Type u_2
n : ℕ
i : Fin (Nat.succ n)
⊢ (∃ a, True ∧ ↑(succEmbedding n).toEmbedding a = i) → 0 < i
[PROOFSTEP]
rintro ⟨i, _, rfl⟩
[GOAL]
case a.mpr.intro.intro
α : Type u_1
β : Type u_2
n : ℕ
i : Fin n
left✝ : True
⊢ 0 < ↑(succEmbedding n).toEmbedding i
[PROOFSTEP]
exact succ_pos _
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
⊢ Iio (last n) = map castSuccEmb.toEmbedding univ
[PROOFSTEP]
apply Finset.map_injective Fin.valEmbedding
[GOAL]
case a
α : Type u_1
β : Type u_2
n : ℕ
⊢ map valEmbedding (Iio (last n)) = map valEmbedding (map castSuccEmb.toEmbedding univ)
[PROOFSTEP]
rw [Finset.map_map, Fin.map_valEmbedding_Iio, Fin.val_last]
[GOAL]
case a
α : Type u_1
β : Type u_2
n : ℕ
⊢ Iio n = map (Function.Embedding.trans castSuccEmb.toEmbedding valEmbedding) univ
[PROOFSTEP]
exact map_valEmbedding_univ.symm
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
i : Fin n
⊢ Ioi (succ i) = map (succEmbedding n).toEmbedding (Ioi i)
[PROOFSTEP]
ext i
[GOAL]
case a
α : Type u_1
β : Type u_2
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ i ∈ Ioi (succ i✝) ↔ i ∈ map (succEmbedding n).toEmbedding (Ioi i✝)
[PROOFSTEP]
simp only [mem_filter, mem_Ioi, mem_map, mem_univ, true_and_iff, Function.Embedding.coeFn_mk, exists_true_left]
[GOAL]
case a
α : Type u_1
β : Type u_2
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ succ i✝ < i ↔ ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = i
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
β : Type u_2
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ succ i✝ < i → ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = i
[PROOFSTEP]
refine' cases _ _ i
[GOAL]
case a.mp.refine'_1
α : Type u_1
β : Type u_2
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ succ i✝ < 0 → ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = 0
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case a.mp.refine'_2
α : Type u_1
β : Type u_2
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), succ i✝ < succ i → ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = succ i
[PROOFSTEP]
intro i hi
[GOAL]
case a.mp.refine'_2
α : Type u_1
β : Type u_2
n : ℕ
i✝¹ : Fin n
i✝ : Fin (Nat.succ n)
i : Fin n
hi : succ i✝¹ < succ i
⊢ ∃ a, i✝¹ < a ∧ ↑(succEmbedding n).toEmbedding a = succ i
[PROOFSTEP]
refine' ⟨i, succ_lt_succ_iff.mp hi, rfl⟩
[GOAL]
case a.mpr
α : Type u_1
β : Type u_2
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ (∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = i) → succ i✝ < i
[PROOFSTEP]
rintro ⟨i, hi, rfl⟩
[GOAL]
case a.mpr.intro.intro
α : Type u_1
β : Type u_2
n : ℕ
i✝ i : Fin n
hi : i✝ < i
⊢ succ i✝ < ↑(succEmbedding n).toEmbedding i
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
i : Fin n
⊢ Iio (castSucc i) = map castSuccEmb.toEmbedding (Iio i)
[PROOFSTEP]
apply Finset.map_injective Fin.valEmbedding
[GOAL]
case a
α : Type u_1
β : Type u_2
n : ℕ
i : Fin n
⊢ map valEmbedding (Iio (castSucc i)) = map valEmbedding (map castSuccEmb.toEmbedding (Iio i))
[PROOFSTEP]
rw [Finset.map_map, Fin.map_valEmbedding_Iio]
[GOAL]
case a
α : Type u_1
β : Type u_2
n : ℕ
i : Fin n
⊢ Iio ↑(castSucc i) = map (Function.Embedding.trans castSuccEmb.toEmbedding valEmbedding) (Iio i)
[PROOFSTEP]
exact (Fin.map_valEmbedding_Iio i).symm
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ Finset.card (filter p univ) = (if p 0 then 1 else 0) + Finset.card (filter (p ∘ succ) univ)
[PROOFSTEP]
rw [Fin.univ_succ, filter_cons, card_disjUnion, filter_map, card_map]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ Finset.card (if p 0 then {0} else ∅) +
      Finset.card (filter (p ∘ ↑{ toFun := succ, inj' := (_ : Function.Injective succ) }) univ) =
    (if p 0 then 1 else 0) + Finset.card (filter (p ∘ succ) univ)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : p 0
⊢ Finset.card {0} + Finset.card (filter (p ∘ ↑{ toFun := succ, inj' := (_ : Function.Injective succ) }) univ) =
    1 + Finset.card (filter (p ∘ succ) univ)
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : ¬p 0
⊢ Finset.card ∅ + Finset.card (filter (p ∘ ↑{ toFun := succ, inj' := (_ : Function.Injective succ) }) univ) =
    0 + Finset.card (filter (p ∘ succ) univ)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then 1 else 0) + Finset.card (filter (p ∘ succ) univ) =
    if p 0 then Finset.card (filter (p ∘ succ) univ) + 1 else Finset.card (filter (p ∘ succ) univ)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : p 0
⊢ 1 + Finset.card (filter (p ∘ succ) univ) = Finset.card (filter (p ∘ succ) univ) + 1
[PROOFSTEP]
simp [add_comm 1]
[GOAL]
case neg
α : Type u_1
β : Type u_2
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : ¬p 0
⊢ 0 + Finset.card (filter (p ∘ succ) univ) = Finset.card (filter (p ∘ succ) univ)
[PROOFSTEP]
simp [add_comm 1]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
inst✝ : DecidableEq α
a : α
v : Vector α n
⊢ Finset.card (filter (fun i => a = Vector.get v i) univ) = List.count a (Vector.toList v)
[PROOFSTEP]
induction' v using Vector.inductionOn with n x xs hxs
[GOAL]
case h_nil
α : Type u_1
β : Type u_2
n : ℕ
inst✝ : DecidableEq α
a : α
⊢ Finset.card (filter (fun i => a = Vector.get Vector.nil i) univ) = List.count a (Vector.toList Vector.nil)
[PROOFSTEP]
simp
[GOAL]
case h_cons
α : Type u_1
β : Type u_2
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : Vector α n
hxs : Finset.card (filter (fun i => a = Vector.get xs i) univ) = List.count a (Vector.toList xs)
⊢ Finset.card (filter (fun i => a = Vector.get (x ::ᵥ xs) i) univ) = List.count a (Vector.toList (x ::ᵥ xs))
[PROOFSTEP]
simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Function.comp, Vector.get_cons_succ, hxs,
  List.count_cons', add_comm (ite (a = x) 1 0)]
