[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Icc a b) = Icc ↑a ↑b
[PROOFSTEP]
simp [Icc_eq_finset_subtype, Finset.fin, Finset.map_map, Icc_filter_lt_of_lt_right]
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ico a b) = Ico ↑a ↑b
[PROOFSTEP]
simp [Ico_eq_finset_subtype, Finset.fin, Finset.map_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioc a b) = Ioc ↑a ↑b
[PROOFSTEP]
simp [Ioc_eq_finset_subtype, Finset.fin, Finset.map_map, Ioc_filter_lt_of_lt_right]
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioo a b) = Ioo ↑a ↑b
[PROOFSTEP]
simp [Ioo_eq_finset_subtype, Finset.fin, Finset.map_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Icc a b) = ↑b + 1 - ↑a
[PROOFSTEP]
rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ico a b) = ↑b - ↑a
[PROOFSTEP]
rw [← Nat.card_Ico, ← map_valEmbedding_Ico, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ioc a b) = ↑b - ↑a
[PROOFSTEP]
rw [← Nat.card_Ioc, ← map_valEmbedding_Ioc, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ioo a b) = ↑b - ↑a - 1
[PROOFSTEP]
rw [← Nat.card_Ioo, ← map_valEmbedding_Ioo, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (uIcc a b) = Int.natAbs (↑↑b - ↑↑a) + 1
[PROOFSTEP]
rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
[PROOFSTEP]
rw [← card_Icc, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
[PROOFSTEP]
rw [← card_Ico, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
[PROOFSTEP]
rw [← card_Ioc, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
[PROOFSTEP]
rw [← card_Ioo, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.uIcc a b) = Int.natAbs (↑↑b - ↑↑a) + 1
[PROOFSTEP]
rw [← card_uIcc, Fintype.card_ofFinset]
[GOAL]
n : ℕ
a b : Fin n
⊢ Ici a = Finset.fin n (Icc (↑a) n)
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
a b a✝ : Fin n
⊢ a✝ ∈ Ici a ↔ a✝ ∈ Finset.fin n (Icc (↑a) n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
a b : Fin n
⊢ Ioi a = Finset.fin n (Ioc (↑a) n)
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
a b a✝ : Fin n
⊢ a✝ ∈ Ioi a ↔ a✝ ∈ Finset.fin n (Ioc (↑a) n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ici a) = Icc (↑a) (n - 1)
[PROOFSTEP]
clear b
[GOAL]
n : ℕ
a : Fin n
⊢ map valEmbedding (Ici a) = Icc (↑a) (n - 1)
[PROOFSTEP]
ext x
[GOAL]
case a
n : ℕ
a : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ici a) ↔ x ∈ Icc (↑a) (n - 1)
[PROOFSTEP]
simp only [exists_prop, Embedding.coe_subtype, mem_Ici, mem_map, mem_Icc]
[GOAL]
case a
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a ≤ a_1 ∧ ↑valEmbedding a_1 = x) ↔ ↑a ≤ x ∧ x ≤ n - 1
[PROOFSTEP]
constructor
[GOAL]
case a.mp
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a ≤ a_1 ∧ ↑valEmbedding a_1 = x) → ↑a ≤ x ∧ x ≤ n - 1
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case a.mp.intro.intro
n : ℕ
a x : Fin n
hx : a ≤ x
⊢ ↑a ≤ ↑valEmbedding x ∧ ↑valEmbedding x ≤ n - 1
[PROOFSTEP]
exact ⟨hx, le_tsub_of_add_le_right <| x.2⟩
[GOAL]
case a.mpr
n : ℕ
a : Fin n
x : ℕ
⊢ ↑a ≤ x ∧ x ≤ n - 1 → ∃ a_2, a ≤ a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
cases n
[GOAL]
case a.mpr.zero
x : ℕ
a : Fin Nat.zero
⊢ ↑a ≤ x ∧ x ≤ Nat.zero - 1 → ∃ a_2, a ≤ a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
exact Fin.elim0 a
[GOAL]
case a.mpr.succ
x n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ ↑a ≤ x ∧ x ≤ Nat.succ n✝ - 1 → ∃ a_2, a ≤ a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
exact fun hx => ⟨⟨x, Nat.lt_succ_iff.2 hx.2⟩, hx.1, rfl⟩
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioi a) = Ioc (↑a) (n - 1)
[PROOFSTEP]
clear b
[GOAL]
n : ℕ
a : Fin n
⊢ map valEmbedding (Ioi a) = Ioc (↑a) (n - 1)
[PROOFSTEP]
ext x
[GOAL]
case a
n : ℕ
a : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ioi a) ↔ x ∈ Ioc (↑a) (n - 1)
[PROOFSTEP]
simp only [exists_prop, Embedding.coe_subtype, mem_Ioi, mem_map, mem_Ioc]
[GOAL]
case a
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ ↑valEmbedding a_1 = x) ↔ ↑a < x ∧ x ≤ n - 1
[PROOFSTEP]
constructor
[GOAL]
case a.mp
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ ↑valEmbedding a_1 = x) → ↑a < x ∧ x ≤ n - 1
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case a.mp.intro.intro
n : ℕ
a x : Fin n
hx : a < x
⊢ ↑a < ↑valEmbedding x ∧ ↑valEmbedding x ≤ n - 1
[PROOFSTEP]
exact ⟨hx, le_tsub_of_add_le_right <| x.2⟩
[GOAL]
case a.mpr
n : ℕ
a : Fin n
x : ℕ
⊢ ↑a < x ∧ x ≤ n - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
cases n
[GOAL]
case a.mpr.zero
x : ℕ
a : Fin Nat.zero
⊢ ↑a < x ∧ x ≤ Nat.zero - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
exact Fin.elim0 a
[GOAL]
case a.mpr.succ
x n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ ↑a < x ∧ x ≤ Nat.succ n✝ - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
[PROOFSTEP]
exact fun hx => ⟨⟨x, Nat.lt_succ_iff.2 hx.2⟩, hx.1, rfl⟩
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Iic b) = Iic ↑b
[PROOFSTEP]
simp [Iic_eq_finset_subtype, Finset.fin, Finset.map_map, Iic_filter_lt_of_lt_right]
[GOAL]
n : ℕ
a b : Fin n
⊢ map valEmbedding (Iio b) = Iio ↑b
[PROOFSTEP]
simp [Iio_eq_finset_subtype, Finset.fin, Finset.map_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ici a) = n - ↑a
[PROOFSTEP]
clear b
[GOAL]
n : ℕ
a : Fin n
⊢ card (Ici a) = n - ↑a
[PROOFSTEP]
cases n with
| zero => exact Fin.elim0 a
| succ => rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
[GOAL]
n : ℕ
a : Fin n
⊢ card (Ici a) = n - ↑a
[PROOFSTEP]
cases n with
| zero => exact Fin.elim0 a
| succ => rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
[GOAL]
case zero
a : Fin Nat.zero
⊢ card (Ici a) = Nat.zero - ↑a
[PROOFSTEP]

| zero => exact Fin.elim0 a
[GOAL]
case zero
a : Fin Nat.zero
⊢ card (Ici a) = Nat.zero - ↑a
[PROOFSTEP]
exact Fin.elim0 a
[GOAL]
case succ
n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ card (Ici a) = Nat.succ n✝ - ↑a
[PROOFSTEP]

| succ => rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
[GOAL]
case succ
n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ card (Ici a) = Nat.succ n✝ - ↑a
[PROOFSTEP]
rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Ioi a) = n - 1 - ↑a
[PROOFSTEP]
rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioc]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Iic b) = ↑b + 1
[PROOFSTEP]
rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ card (Iio b) = ↑b
[PROOFSTEP]
rw [← Nat.card_Iio b, ← map_valEmbedding_Iio, card_map]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ici a) = n - ↑a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ici]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ioi a) = n - 1 - ↑a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ioi]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Iic b) = ↑b + 1
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Iic]
[GOAL]
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Iio b) = ↑b
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Iio]
