[GOAL]
α : Type u_1
s✝ t✝ s t : Finset α
⊢ s ∈ powerset t ↔ s ⊆ t
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
s t✝ t : Finset α
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ { val := val✝, nodup := nodup✝ } ∈ powerset t ↔ { val := val✝, nodup := nodup✝ } ⊆ t
[PROOFSTEP]
simp [powerset, mem_mk, mem_pmap, mk.injEq, mem_powerset, exists_prop, exists_eq_right, ← val_le_iff]
[GOAL]
α : Type u_1
s✝ t s : Finset α
⊢ ↑(powerset s) = toSet ⁻¹' 𝒫↑s
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
s✝ t s x✝ : Finset α
⊢ x✝ ∈ ↑(powerset s) ↔ x✝ ∈ toSet ⁻¹' 𝒫↑s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s t : Finset α
⊢ powerset s = {∅} ↔ s = ∅
[PROOFSTEP]
rw [← powerset_empty, powerset_inj]
[GOAL]
α : Type u_1
s✝ t✝ s t : Finset α
a : α
ht : t ∈ powerset s
h : ¬a ∈ s
⊢ ¬a ∈ t
[PROOFSTEP]
apply mt _ h
[GOAL]
α : Type u_1
s✝ t✝ s t : Finset α
a : α
ht : t ∈ powerset s
h : ¬a ∈ s
⊢ a ∈ t → a ∈ s
[PROOFSTEP]
apply mem_powerset.1 ht
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ powerset (insert a s) = powerset s ∪ image (insert a) (powerset s)
[PROOFSTEP]
ext t
[GOAL]
case a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t ∈ powerset (insert a s) ↔ t ∈ powerset s ∪ image (insert a) (powerset s)
[PROOFSTEP]
simp only [exists_prop, mem_powerset, mem_image, mem_union, subset_insert_iff]
[GOAL]
case a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ erase t a ⊆ s ↔ t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
[PROOFSTEP]
by_cases h : a ∈ t
[GOAL]
case pos
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ erase t a ⊆ s ↔ t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
[PROOFSTEP]
constructor
[GOAL]
case pos.mp
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ erase t a ⊆ s → t ⊆ s ∨ ∃ a_2, a_2 ⊆ s ∧ insert a a_2 = t
[PROOFSTEP]
exact fun H => Or.inr ⟨_, H, insert_erase h⟩
[GOAL]
case pos.mpr
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ (t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t) → erase t a ⊆ s
[PROOFSTEP]
intro H
[GOAL]
case pos.mpr
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
⊢ erase t a ⊆ s
[PROOFSTEP]
cases' H with H H
[GOAL]
case pos.mpr.inl
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : t ⊆ s
⊢ erase t a ⊆ s
[PROOFSTEP]
exact Subset.trans (erase_subset a t) H
[GOAL]
case pos.mpr.inr
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
⊢ erase t a ⊆ s
[PROOFSTEP]
rcases H with ⟨u, hu⟩
[GOAL]
case pos.mpr.inr.intro
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
u : Finset α
hu : u ⊆ s ∧ insert a u = t
⊢ erase t a ⊆ s
[PROOFSTEP]
rw [← hu.2]
[GOAL]
case pos.mpr.inr.intro
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
u : Finset α
hu : u ⊆ s ∧ insert a u = t
⊢ erase (insert a u) a ⊆ s
[PROOFSTEP]
exact Subset.trans (erase_insert_subset a u) hu.1
[GOAL]
case neg
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : ¬a ∈ t
⊢ erase t a ⊆ s ↔ t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
[PROOFSTEP]
have : ¬∃ u : Finset α, u ⊆ s ∧ insert a u = t := by simp [Ne.symm (ne_insert_of_not_mem _ _ h)]
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : ¬a ∈ t
⊢ ¬∃ u, u ⊆ s ∧ insert a u = t
[PROOFSTEP]
simp [Ne.symm (ne_insert_of_not_mem _ _ h)]
[GOAL]
case neg
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : ¬a ∈ t
this : ¬∃ u, u ⊆ s ∧ insert a u = t
⊢ erase t a ⊆ s ↔ t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
[PROOFSTEP]
simp [Finset.erase_eq_of_not_mem h, this]
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s t : Finset α
⊢ t ∈ ssubsets s ↔ t ⊂ s
[PROOFSTEP]
rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
s : Finset α
h : Finset.Nonempty s
⊢ ∅ ∈ ssubsets s
[PROOFSTEP]
rw [mem_ssubsets, ssubset_iff_subset_ne]
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
s : Finset α
h : Finset.Nonempty s
⊢ ∅ ⊆ s ∧ ∅ ≠ s
[PROOFSTEP]
exact ⟨empty_subset s, h.ne_empty.symm⟩
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
n : ℕ
s t : Finset α
⊢ s ∈ powersetLen n t ↔ s ⊆ t ∧ card s = n
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
s t✝ : Finset α
n : ℕ
t : Finset α
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ { val := val✝, nodup := nodup✝ } ∈ powersetLen n t ↔
    { val := val✝, nodup := nodup✝ } ⊆ t ∧ card { val := val✝, nodup := nodup✝ } = n
[PROOFSTEP]
simp [powersetLen, val_le_iff.symm]
[GOAL]
α : Type u_1
s✝ t s : Finset α
⊢ powersetLen 0 s = {∅}
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ∈ powersetLen 0 s ↔ a✝ ∈ {∅}
[PROOFSTEP]
rw [mem_powersetLen, mem_singleton, card_eq_zero]
[GOAL]
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ a✝ = ∅ ↔ a✝ = ∅
[PROOFSTEP]
refine'
  ⟨fun h => h.2, fun h => by
    rw [h]
    exact ⟨empty_subset s, rfl⟩⟩
[GOAL]
α : Type u_1
s✝ t s a✝ : Finset α
h : a✝ = ∅
⊢ a✝ ⊆ s ∧ a✝ = ∅
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
s✝ t s a✝ : Finset α
h : a✝ = ∅
⊢ ∅ ⊆ s ∧ ∅ = ∅
[PROOFSTEP]
exact ⟨empty_subset s, rfl⟩
[GOAL]
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
h : card s < n
⊢ card (powersetLen n s) = 0
[PROOFSTEP]
rw [card_powersetLen, Nat.choose_eq_zero_of_lt h]
[GOAL]
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
⊢ powersetLen n s = filter (fun x => card x = n) (powerset s)
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
s✝ t : Finset α
n : ℕ
s a✝ : Finset α
⊢ a✝ ∈ powersetLen n s ↔ a✝ ∈ filter (fun x => card x = n) (powerset s)
[PROOFSTEP]
simp [mem_powersetLen]
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ powersetLen (Nat.succ n) (insert x s) = powersetLen (Nat.succ n) s ∪ image (insert x) (powersetLen n s)
[PROOFSTEP]
rw [powersetLen_eq_filter, powerset_insert, filter_union, ← powersetLen_eq_filter]
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ powersetLen (Nat.succ n) s ∪ filter (fun x => card x = Nat.succ n) (image (insert x) (powerset s)) =
    powersetLen (Nat.succ n) s ∪ image (insert x) (powersetLen n s)
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ filter (fun x => card x = Nat.succ n) (image (insert x) (powerset s)) = image (insert x) (powersetLen n s)
[PROOFSTEP]
rw [powersetLen_eq_filter, image_filter]
[GOAL]
case e_a
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ image (insert x) (filter ((fun x => card x = Nat.succ n) ∘ insert x) (powerset s)) =
    image (insert x) (filter (fun x => card x = n) (powerset s))
[PROOFSTEP]
congr 1
[GOAL]
case e_a.e_s
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ filter ((fun x => card x = Nat.succ n) ∘ insert x) (powerset s) = filter (fun x => card x = n) (powerset s)
[PROOFSTEP]
ext t
[GOAL]
case e_a.e_s.a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
t : Finset α
⊢ t ∈ filter ((fun x => card x = Nat.succ n) ∘ insert x) (powerset s) ↔ t ∈ filter (fun x => card x = n) (powerset s)
[PROOFSTEP]
simp only [mem_powerset, mem_filter, Function.comp_apply, and_congr_right_iff]
[GOAL]
case e_a.e_s.a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
t : Finset α
⊢ t ⊆ s → (card (insert x t) = Nat.succ n ↔ card t = n)
[PROOFSTEP]
intro ht
[GOAL]
case e_a.e_s.a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
t : Finset α
ht : t ⊆ s
⊢ card (insert x t) = Nat.succ n ↔ card t = n
[PROOFSTEP]
have : x ∉ t := fun H => h (ht H)
[GOAL]
case e_a.e_s.a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
t : Finset α
ht : t ⊆ s
this : ¬x ∈ t
⊢ card (insert x t) = Nat.succ n ↔ card t = n
[PROOFSTEP]
simp [card_insert_of_not_mem this, Nat.succ_inj']
[GOAL]
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
h : n ≤ card s
⊢ Finset.Nonempty (powersetLen n s)
[PROOFSTEP]
classical
induction' s using Finset.induction_on with x s hx IH generalizing n
· rw [card_empty, le_zero_iff] at h
  rw [h, powersetLen_zero]
  exact Finset.singleton_nonempty _
· cases n
  · simp
  · rw [card_insert_of_not_mem hx, Nat.succ_le_succ_iff] at h
    rw [powersetLen_succ_insert hx]
    refine' Nonempty.mono _ ((IH h).image (insert x))
    exact subset_union_right _ _
[GOAL]
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
h : n ≤ card s
⊢ Finset.Nonempty (powersetLen n s)
[PROOFSTEP]
induction' s using Finset.induction_on with x s hx IH generalizing n
[GOAL]
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n ≤ card ∅
⊢ Finset.Nonempty (powersetLen n ∅)
[PROOFSTEP]
rw [card_empty, le_zero_iff] at h
[GOAL]
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n = 0
⊢ Finset.Nonempty (powersetLen n ∅)
[PROOFSTEP]
rw [h, powersetLen_zero]
[GOAL]
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n = 0
⊢ Finset.Nonempty {∅}
[PROOFSTEP]
exact Finset.singleton_nonempty _
[GOAL]
case insert
α : Type u_1
s✝¹ t : Finset α
n✝ : ℕ
s✝ : Finset α
h✝ : n✝ ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n : ℕ
h : n ≤ card (insert x s)
⊢ Finset.Nonempty (powersetLen n (insert x s))
[PROOFSTEP]
cases n
[GOAL]
case insert.zero
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
h : Nat.zero ≤ card (insert x s)
⊢ Finset.Nonempty (powersetLen Nat.zero (insert x s))
[PROOFSTEP]
simp
[GOAL]
case insert.succ
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n✝ : ℕ
h : Nat.succ n✝ ≤ card (insert x s)
⊢ Finset.Nonempty (powersetLen (Nat.succ n✝) (insert x s))
[PROOFSTEP]
rw [card_insert_of_not_mem hx, Nat.succ_le_succ_iff] at h
[GOAL]
case insert.succ
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n✝ : ℕ
h : n✝ ≤ card s
⊢ Finset.Nonempty (powersetLen (Nat.succ n✝) (insert x s))
[PROOFSTEP]
rw [powersetLen_succ_insert hx]
[GOAL]
case insert.succ
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n✝ : ℕ
h : n✝ ≤ card s
⊢ Finset.Nonempty (powersetLen (Nat.succ n✝) s ∪ image (insert x) (powersetLen n✝ s))
[PROOFSTEP]
refine' Nonempty.mono _ ((IH h).image (insert x))
[GOAL]
case insert.succ
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n✝ : ℕ
h : n✝ ≤ card s
⊢ image (insert x) (powersetLen n✝ s) ⊆ powersetLen (Nat.succ n✝) s ∪ image (insert x) (powersetLen n✝ s)
[PROOFSTEP]
exact subset_union_right _ _
[GOAL]
α : Type u_1
s✝ t s : Finset α
⊢ powersetLen (card s) s = {s}
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ∈ powersetLen (card s) s ↔ a✝ ∈ {s}
[PROOFSTEP]
rw [mem_powersetLen, mem_singleton]
[GOAL]
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ card a✝ = card s ↔ a✝ = s
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ card a✝ = card s → a✝ = s
[PROOFSTEP]
exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge
[GOAL]
case a.mpr
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ card a✝ = card s
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mpr
α : Type u_1
s t a✝ : Finset α
⊢ a✝ ⊆ a✝ ∧ card a✝ = card a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s✝ t s : Finset α
⊢ powerset s =
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
[PROOFSTEP]
refine' ext fun a => ⟨fun ha => _, fun ha => _⟩
[GOAL]
case refine'_1
α : Type u_1
s✝ t s a : Finset α
ha : a ∈ powerset s
⊢ a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
[PROOFSTEP]
rw [mem_disjiUnion]
[GOAL]
case refine'_1
α : Type u_1
s✝ t s a : Finset α
ha : a ∈ powerset s
⊢ ∃ a_1, a_1 ∈ range (card s + 1) ∧ a ∈ powersetLen a_1 s
[PROOFSTEP]
exact
  ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_of_subset (mem_powerset.mp ha))),
    mem_powersetLen.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
[GOAL]
case refine'_2
α : Type u_1
s✝ t s a : Finset α
ha :
  a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
⊢ a ∈ powerset s
[PROOFSTEP]
rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
s✝ t s a : Finset α
ha✝ :
  a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
i : ℕ
_hi : i ∈ range (card s + 1)
ha : a ∈ powersetLen i s
⊢ a ∈ powerset s
[PROOFSTEP]
exact mem_powerset.mpr (mem_powersetLen.mp ha).1
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq (Finset α)
s : Finset α
⊢ powerset s = Finset.biUnion (range (card s + 1)) fun i => powersetLen i s
[PROOFSTEP]
simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s
[GOAL]
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ sup (powersetLen (Nat.succ n) u) id = u
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ sup (powersetLen (Nat.succ n) u) id ≤ u
[PROOFSTEP]
simp_rw [Finset.sup_le_iff, mem_powersetLen]
[GOAL]
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ ∀ (b : Finset α), b ⊆ u ∧ card b = Nat.succ n → id b ≤ u
[PROOFSTEP]
rintro x ⟨h, -⟩
[GOAL]
case a.intro
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
x : Finset α
h : x ⊆ u
⊢ id x ≤ u
[PROOFSTEP]
exact h
[GOAL]
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ u ≤ sup (powersetLen (Nat.succ n) u) id
[PROOFSTEP]
rw [sup_eq_biUnion, le_iff_subset, subset_iff]
[GOAL]
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
[PROOFSTEP]
cases' (Nat.succ_le_of_lt hn).eq_or_lt with h' h'
[GOAL]
case a.inl
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n = card u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
[PROOFSTEP]
simp [h']
[GOAL]
case a.inr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
[PROOFSTEP]
intro x hx
[GOAL]
case a.inr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
⊢ x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
[PROOFSTEP]
simp only [mem_biUnion, exists_prop, id.def]
[GOAL]
case a.inr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
⊢ ∃ a, a ∈ powersetLen (Nat.succ n) u ∧ x ∈ a
[PROOFSTEP]
obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetLen n (u.erase x) :=
  powersetLen_nonempty (le_trans (Nat.le_pred_of_lt hn) pred_card_le_card_erase)
[GOAL]
case a.inr.intro
α : Type u_1
s t✝ : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetLen n (erase u x)
⊢ ∃ a, a ∈ powersetLen (Nat.succ n) u ∧ x ∈ a
[PROOFSTEP]
refine' ⟨insert x t, _, mem_insert_self _ _⟩
[GOAL]
case a.inr.intro
α : Type u_1
s t✝ : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetLen n (erase u x)
⊢ insert x t ∈ powersetLen (Nat.succ n) u
[PROOFSTEP]
rw [← insert_erase hx, powersetLen_succ_insert (not_mem_erase _ _)]
[GOAL]
case a.inr.intro
α : Type u_1
s t✝ : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetLen n (erase u x)
⊢ insert x t ∈ powersetLen (Nat.succ n) (erase u x) ∪ image (insert x) (powersetLen n (erase u x))
[PROOFSTEP]
exact mem_union_right _ (mem_image_of_mem _ ht)
[GOAL]
α : Type u_1
s✝ t s : Finset α
i : ℕ
⊢ Multiset.map val (powersetLen i s).val = Multiset.powersetLen i s.val
[PROOFSTEP]
simp [Finset.powersetLen, map_pmap, pmap_eq_map, map_id']
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ∈ powersetLen n (map f s) ↔ t ∈ map (mapEmbedding f).toEmbedding (powersetLen n s)
[PROOFSTEP]
simp only [card_map, mem_powersetLen, le_eq_subset, gt_iff_lt, mem_map, mapEmbedding_apply]
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n ↔ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n → ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
classical
intro h
have : map f (filter (fun x => (f x ∈ t)) s) = t := by
  ext x
  simp only [mem_map, mem_filter, decide_eq_true_eq]
  exact
    ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂, fun hx =>
      let ⟨y, hy⟩ := mem_map.1 (h.1 hx);
      ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
refine' ⟨_, _, this⟩
rw [← card_map f, this, h.2]; simp
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n → ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
⊢ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
have : map f (filter (fun x => (f x ∈ t)) s) = t := by
  ext x
  simp only [mem_map, mem_filter, decide_eq_true_eq]
  exact
    ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂, fun hx =>
      let ⟨y, hy⟩ := mem_map.1 (h.1 hx);
      ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
⊢ map f (filter (fun x => ↑f x ∈ t) s) = t
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
x : β
⊢ x ∈ map f (filter (fun x => ↑f x ∈ t) s) ↔ x ∈ t
[PROOFSTEP]
simp only [mem_map, mem_filter, decide_eq_true_eq]
[GOAL]
case a
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
x : β
⊢ (∃ a, (a ∈ s ∧ ↑f a ∈ t) ∧ ↑f a = x) ↔ x ∈ t
[PROOFSTEP]
exact
  ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂, fun hx =>
    let ⟨y, hy⟩ := mem_map.1 (h.1 hx);
    ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
refine' ⟨_, _, this⟩
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ filter (fun x => ↑f x ∈ t) s ⊆ s ∧ card (filter (fun x => ↑f x ∈ t) s) = n
[PROOFSTEP]
rw [← card_map f, this, h.2]
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ filter (fun x => ↑f x ∈ t) s ⊆ s ∧ n = n
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ card t = n
[PROOFSTEP]
rintro ⟨a, ⟨has, rfl⟩, rfl⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
s✝ t : Finset α
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ ↑(mapEmbedding f).toEmbedding a ⊆ map f s ∧ card (↑(mapEmbedding f).toEmbedding a) = card a
[PROOFSTEP]
dsimp [RelEmbedding.coe_toEmbedding]
  --Porting note: Why is `rw` required here and not `simp`?
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
s✝ t : Finset α
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ ↑(mapEmbedding f) a ⊆ map f s ∧ card (↑(mapEmbedding f) a) = card a
[PROOFSTEP]
rw [mapEmbedding_apply]
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
s✝ t : Finset α
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ map f a ⊆ map f s ∧ card (map f a) = card a
[PROOFSTEP]
simp [has]


[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Finset.Nonempty (Icc a b) ↔ a ≤ b
[PROOFSTEP]
rw [← coe_nonempty, coe_Icc, Set.nonempty_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Finset.Nonempty (Ico a b) ↔ a < b
[PROOFSTEP]
rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Finset.Nonempty (Ioc a b) ↔ a < b
[PROOFSTEP]
rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DenselyOrdered α
⊢ Finset.Nonempty (Ioo a b) ↔ a < b
[PROOFSTEP]
rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Icc a b = ∅ ↔ ¬a ≤ b
[PROOFSTEP]
rw [← coe_eq_empty, coe_Icc, Set.Icc_eq_empty_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ico a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← coe_eq_empty, coe_Ico, Set.Ico_eq_empty_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioc a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Icc a b ↔ a ≤ b
[PROOFSTEP]
simp only [mem_Icc, true_and_iff, le_rfl]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ico a b ↔ a < b
[PROOFSTEP]
simp only [mem_Ico, true_and_iff, le_refl]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Icc a b ↔ a ≤ b
[PROOFSTEP]
simp only [mem_Icc, and_true_iff, le_rfl]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ioc a b ↔ a < b
[PROOFSTEP]
simp only [mem_Ioc, and_true_iff, le_rfl]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂
[PROOFSTEP]
simpa [← coe_subset] using Set.Icc_subset_Icc ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂
[PROOFSTEP]
simpa [← coe_subset] using Set.Ico_subset_Ico ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioc_subset_Ioc ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ⊆ Ioo a₂ b₂
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioo_subset_Ioo ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : a₁ < a₂
⊢ Ico a₂ b ⊆ Ioo a₁ b
[PROOFSTEP]
rw [← coe_subset, coe_Ico, coe_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b
[PROOFSTEP]
exact Set.Ico_subset_Ioo_left h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b₁ < b₂
⊢ Ioc a b₁ ⊆ Ioo a b₂
[PROOFSTEP]
rw [← coe_subset, coe_Ioc, coe_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b₁ < b₂
⊢ Set.Ioc a b₁ ⊆ Set.Ioo a b₂
[PROOFSTEP]
exact Set.Ioc_subset_Ioo_right h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b₁ < b₂
⊢ Icc a b₁ ⊆ Ico a b₂
[PROOFSTEP]
rw [← coe_subset, coe_Icc, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ Set.Ico a b₂
[PROOFSTEP]
exact Set.Icc_subset_Ico_right h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioo a b ⊆ Ico a b
[PROOFSTEP]
rw [← coe_subset, coe_Ioo, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ioo a b ⊆ Set.Ico a b
[PROOFSTEP]
exact Set.Ioo_subset_Ico_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioo a b ⊆ Ioc a b
[PROOFSTEP]
rw [← coe_subset, coe_Ioo, coe_Ioc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ioo a b ⊆ Set.Ioc a b
[PROOFSTEP]
exact Set.Ioo_subset_Ioc_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ico a b ⊆ Icc a b
[PROOFSTEP]
rw [← coe_subset, coe_Ico, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ico a b ⊆ Set.Icc a b
[PROOFSTEP]
exact Set.Ico_subset_Icc_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioc a b ⊆ Icc a b
[PROOFSTEP]
rw [← coe_subset, coe_Ioc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ioc a b ⊆ Set.Icc a b
[PROOFSTEP]
exact Set.Ioc_subset_Icc_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
[PROOFSTEP]
rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
[PROOFSTEP]
rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
[PROOFSTEP]
rw [← coe_subset, coe_Icc, coe_Ico, Set.Icc_subset_Ico_iff h₁]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂
[PROOFSTEP]
rw [← coe_ssubset, coe_Icc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
[PROOFSTEP]
exact Set.Icc_ssubset_Icc_left hI ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂
[PROOFSTEP]
rw [← coe_ssubset, coe_Icc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
[PROOFSTEP]
exact Set.Icc_ssubset_Icc_right hI ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
s : Set α
h₀ : BddBelow s
h₁ : BddAbove s
⊢ Set.Finite s
[PROOFSTEP]
let ⟨a, ha⟩ := h₀
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b b₁ b₂ c x : α
s : Set α
h₀ : BddBelow s
h₁ : BddAbove s
a : α
ha : a ∈ lowerBounds s
⊢ Set.Finite s
[PROOFSTEP]
let ⟨b, hb⟩ := h₁
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
s : Set α
h₀ : BddBelow s
h₁ : BddAbove s
a : α
ha : a ∈ lowerBounds s
b : α
hb : b ∈ upperBounds s
⊢ Set.Finite s
[PROOFSTEP]
classical exact ⟨Set.fintypeOfMemBounds ha hb⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
s : Set α
h₀ : BddBelow s
h₁ : BddAbove s
a : α
ha : a ∈ lowerBounds s
b : α
hb : b ∈ upperBounds s
⊢ Set.Finite s
[PROOFSTEP]
exact ⟨Set.fintypeOfMemBounds ha hb⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a c
[PROOFSTEP]
ext x
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x✝ : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
x : α
⊢ x ∈ filter (fun x => x < c) (Ico a b) ↔ x ∈ Ico a c
[PROOFSTEP]
rw [mem_filter, mem_Ico, mem_Ico, and_right_comm]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x✝ : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
x : α
⊢ (a ≤ x ∧ x < c) ∧ x < b ↔ a ≤ x ∧ x < c
[PROOFSTEP]
exact and_iff_left_of_imp fun h => h.2.trans_le hcb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
⊢ filter ((fun x x_1 => x ≤ x_1) c) (Ico a b) = Ico c b
[PROOFSTEP]
ext x
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x✝ a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
x : α
⊢ x ∈ filter ((fun x x_1 => x ≤ x_1) c) (Ico a b) ↔ x ∈ Ico c b
[PROOFSTEP]
rw [mem_filter, mem_Ico, mem_Ico, and_comm, and_left_comm]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x✝ a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
x : α
⊢ a ≤ x ∧ (fun x x_1 => x ≤ x_1) c x ∧ x < b ↔ c ≤ x ∧ x < b
[PROOFSTEP]
exact and_iff_right_of_imp fun h => hac.trans h.1
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j < b
⊢ filter (fun j => a < j ∧ j < b) univ = Ioo a b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j < b
a✝ : α
⊢ a✝ ∈ filter (fun j => a < j ∧ j < b) univ ↔ a✝ ∈ Ioo a b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j ≤ b
⊢ filter (fun j => a < j ∧ j ≤ b) univ = Ioc a b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ filter (fun j => a < j ∧ j ≤ b) univ ↔ a✝ ∈ Ioc a b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j < b
⊢ filter (fun j => a ≤ j ∧ j < b) univ = Ico a b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j < b
a✝ : α
⊢ a✝ ∈ filter (fun j => a ≤ j ∧ j < b) univ ↔ a✝ ∈ Ico a b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j ≤ b
⊢ filter (fun j => a ≤ j ∧ j ≤ b) univ = Icc a b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ filter (fun j => a ≤ j ∧ j ≤ b) univ ↔ a✝ ∈ Icc a b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderTop α
⊢ Icc a b ⊆ Ici a
[PROOFSTEP]
simpa [← coe_subset] using Set.Icc_subset_Ici_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderTop α
⊢ Ico a b ⊆ Ici a
[PROOFSTEP]
simpa [← coe_subset] using Set.Ico_subset_Ici_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioc a b ⊆ Ioi a
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioc_subset_Ioi_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioo a b ⊆ Ioi a
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioo_subset_Ioi_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderBot α
⊢ Icc a b ⊆ Iic b
[PROOFSTEP]
simpa [← coe_subset] using Set.Icc_subset_Iic_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderBot α
⊢ Ioc a b ⊆ Iic b
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioc_subset_Iic_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderBot α
⊢ Ico a b ⊆ Iio b
[PROOFSTEP]
simpa [← coe_subset] using Set.Ico_subset_Iio_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderBot α
⊢ Ioo a b ⊆ Iio b
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioo_subset_Iio_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ioi a ⊆ Ici a
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioi_subset_Ici_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred ((fun x x_1 => x < x_1) a)
⊢ filter ((fun x x_1 => x < x_1) a) univ = Ioi a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred ((fun x x_1 => x < x_1) a)
a✝ : α
⊢ a✝ ∈ filter ((fun x x_1 => x < x_1) a) univ ↔ a✝ ∈ Ioi a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) a)
⊢ filter ((fun x x_1 => x ≤ x_1) a) univ = Ici a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) a)
a✝ : α
⊢ a✝ ∈ filter ((fun x x_1 => x ≤ x_1) a) univ ↔ a✝ ∈ Ici a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ Iio a ⊆ Iic a
[PROOFSTEP]
simpa [← coe_subset] using Set.Iio_subset_Iic_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x < a
⊢ filter (fun x => x < a) univ = Iio a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x < a
a✝ : α
⊢ a✝ ∈ filter (fun x => x < a) univ ↔ a✝ ∈ Iio a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x ≤ a
⊢ filter (fun x => x ≤ a) univ = Iic a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x ≤ a
a✝ : α
⊢ a✝ ∈ filter (fun x => x ≤ a) univ ↔ a✝ ∈ Iic a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b c a : α
⊢ Icc a a = {a}
[PROOFSTEP]
rw [← coe_eq_singleton, coe_Icc, Set.Icc_self]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c
[PROOFSTEP]
rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ erase (Icc a b) a = Ioc a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ erase (Icc a b) b = Ico a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ erase (Ico a b) a = Ioo a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ erase (Ioc a b) b = Ioo a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b
[PROOFSTEP]
rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert a (Ioc a b) = Icc a b
[PROOFSTEP]
rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a (Ioo a b) = Ico a b
[PROOFSTEP]
rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b
[PROOFSTEP]
rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ico a b = {b}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ioc a b = {a}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a < b
⊢ Ico a b \ Ioo a b = {a}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a < b
⊢ Ioc a b \ Ioo a b = {b}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) (_ : ¬b ∈ Ico a b)
[PROOFSTEP]
classical rw [cons_eq_insert, Ico_insert_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) (_ : ¬b ∈ Ico a b)
[PROOFSTEP]
rw [cons_eq_insert, Ico_insert_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) (_ : ¬a ∈ Ioc a b)
[PROOFSTEP]
classical rw [cons_eq_insert, Ioc_insert_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) (_ : ¬a ∈ Ioc a b)
[PROOFSTEP]
rw [cons_eq_insert, Ioc_insert_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) (_ : ¬b ∈ Ioo a b)
[PROOFSTEP]
classical rw [cons_eq_insert, Ioo_insert_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) (_ : ¬b ∈ Ioo a b)
[PROOFSTEP]
rw [cons_eq_insert, Ioo_insert_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) (_ : ¬a ∈ Ioo a b)
[PROOFSTEP]
classical rw [cons_eq_insert, Ioo_insert_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) (_ : ¬a ∈ Ioo a b)
[PROOFSTEP]
rw [cons_eq_insert, Ioo_insert_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ filter (fun x => x ≤ a) (Ico a b) = {a}
[PROOFSTEP]
ext x
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x ∈ filter (fun x => x ≤ a) (Ico a b) ↔ x ∈ {a}
[PROOFSTEP]
rw [mem_filter, mem_Ico, mem_singleton, and_right_comm, ← le_antisymm_iff, eq_comm]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x = a ∧ x < b ↔ x = a
[PROOFSTEP]
exact and_iff_left_of_imp fun h => h.le.trans_lt hab
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ico a b) = card (Icc a b) - 1
[PROOFSTEP]
classical
by_cases h : a ≤ b
· rw [Icc_eq_cons_Ico h, card_cons]
  exact (Nat.add_sub_cancel _ _).symm
· rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, zero_tsub]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ico a b) = card (Icc a b) - 1
[PROOFSTEP]
by_cases h : a ≤ b
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a ≤ b
⊢ card (Ico a b) = card (Icc a b) - 1
[PROOFSTEP]
rw [Icc_eq_cons_Ico h, card_cons]
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a ≤ b
⊢ card (Ico a b) = card (Ico a b) + 1 - 1
[PROOFSTEP]
exact (Nat.add_sub_cancel _ _).symm
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : ¬a ≤ b
⊢ card (Ico a b) = card (Icc a b) - 1
[PROOFSTEP]
rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, zero_tsub]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ioo a b) = card (Ico a b) - 1
[PROOFSTEP]
classical
by_cases h : a < b
· rw [Ico_eq_cons_Ioo h, card_cons]
  exact (Nat.add_sub_cancel _ _).symm
· rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, zero_tsub]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ioo a b) = card (Ico a b) - 1
[PROOFSTEP]
by_cases h : a < b
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a < b
⊢ card (Ioo a b) = card (Ico a b) - 1
[PROOFSTEP]
rw [Ico_eq_cons_Ioo h, card_cons]
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a < b
⊢ card (Ioo a b) = card (Ioo a b) + 1 - 1
[PROOFSTEP]
exact (Nat.add_sub_cancel _ _).symm
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : ¬a < b
⊢ card (Ioo a b) = card (Ico a b) - 1
[PROOFSTEP]
rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, zero_tsub]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ioo a b) = card (Icc a b) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Icc a b) - 1 - 1 = card (Icc a b) - 2
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ erase (Ici a) a = Ioi a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ erase (Ici a) a ↔ a✝ ∈ Ioi a
[PROOFSTEP]
simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ insert a (Ioi a) = Ici a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a
[PROOFSTEP]
simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) (_ : ¬a ∈ Ioi a)
[PROOFSTEP]
classical rw [cons_eq_insert, Ioi_insert]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) (_ : ¬a ∈ Ioi a)
[PROOFSTEP]
rw [cons_eq_insert, Ioi_insert]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ card (Ioi a) = card (Ici a) - 1
[PROOFSTEP]
rw [Ici_eq_cons_Ioi, card_cons, add_tsub_cancel_right]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ erase (Iic b) b = Iio b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ erase (Iic b) b ↔ a✝ ∈ Iio b
[PROOFSTEP]
simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ insert b (Iio b) = Iic b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ insert b (Iio b) ↔ a✝ ∈ Iic b
[PROOFSTEP]
simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) (_ : ¬b ∈ Iio b)
[PROOFSTEP]
classical rw [cons_eq_insert, Iio_insert]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) (_ : ¬b ∈ Iio b)
[PROOFSTEP]
rw [cons_eq_insert, Iio_insert]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ card (Iio a) = card (Iic a) - 1
[PROOFSTEP]
rw [Iic_eq_cons_Iio, card_cons, add_tsub_cancel_right]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
[PROOFSTEP]
rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b ∪ Ico b c = Ico a c
[PROOFSTEP]
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ioc a b ∪ Ioc b c = Ioc a c
[PROOFSTEP]
rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c
[PROOFSTEP]
rw [← coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
[PROOFSTEP]
exact Set.Ico_subset_Ico_union_Ico
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
[PROOFSTEP]
rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, ← inf_eq_min, ← sup_eq_max, Set.Ico_inter_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
cases le_total b c with
| inl h => rw [Ico_filter_lt_of_right_le h, min_eq_left h]
| inr h => rw [Ico_filter_lt_of_le_right h, min_eq_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
x✝ : b ≤ c ∨ c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
cases le_total b c with
| inl h => rw [Ico_filter_lt_of_right_le h, min_eq_left h]
| inr h => rw [Ico_filter_lt_of_le_right h, min_eq_right h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]

| inl h => rw [Ico_filter_lt_of_right_le h, min_eq_left h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
rw [Ico_filter_lt_of_right_le h, min_eq_left h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]

| inr h => rw [Ico_filter_lt_of_le_right h, min_eq_right h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
rw [Ico_filter_lt_of_le_right h, min_eq_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
cases le_total a c with
| inl h => rw [Ico_filter_le_of_left_le h, max_eq_right h]
| inr h => rw [Ico_filter_le_of_le_left h, max_eq_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
x✝ : a ≤ c ∨ c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
cases le_total a c with
| inl h => rw [Ico_filter_le_of_left_le h, max_eq_right h]
| inr h => rw [Ico_filter_le_of_le_left h, max_eq_left h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]

| inl h => rw [Ico_filter_le_of_left_le h, max_eq_right h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
rw [Ico_filter_le_of_left_le h, max_eq_right h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]

| inr h => rw [Ico_filter_le_of_le_left h, max_eq_left h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
rw [Ico_filter_le_of_le_left h, max_eq_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ filter (fun x => x < c) (Ioo a b) = Ioo a (min b c)
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝¹ b✝ a b c a✝ : α
⊢ a✝ ∈ filter (fun x => x < c) (Ioo a b) ↔ a✝ ∈ Ioo a (min b c)
[PROOFSTEP]
simp [and_assoc]
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝³ : LinearOrder α✝
inst✝² : LocallyFiniteOrder α✝
a✝ b✝ : α✝
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ filter (fun x => x < b) (Iio a) = Iio (min a b)
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α✝ : Type u_2
inst✝³ : LinearOrder α✝
inst✝² : LocallyFiniteOrder α✝
a✝¹ b✝ : α✝
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b a✝ : α
⊢ a✝ ∈ filter (fun x => x < b) (Iio a) ↔ a✝ ∈ Iio (min a b)
[PROOFSTEP]
simp [and_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]
cases le_total a c with
| inl h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
  exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
| inr h => rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
x✝ : a ≤ c ∨ c ≤ a
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]
cases le_total a c with
| inl h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
  exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
| inr h => rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]

| inl h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
  exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]
ext x
[GOAL]
case inl.a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
x : α
⊢ x ∈ Ico a b \ Ico a c ↔ x ∈ Ico (max a c) b
[PROOFSTEP]
rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
[GOAL]
case inl.a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
x : α
⊢ (a ≤ x ∧ (a ≤ x → c ≤ x)) ∧ x < b ↔ c ≤ x ∧ x < b
[PROOFSTEP]
exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ a
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]

| inr h => rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ a
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]
rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]
cases le_total b c with
| inl h => rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
| inr h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
  exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
x✝ : b ≤ c ∨ c ≤ b
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]
cases le_total b c with
| inl h => rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
| inr h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
  exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : b ≤ c
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]

| inl h => rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : b ≤ c
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]
rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]

| inr h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
  exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]
ext x
[GOAL]
case inr.a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
x : α
⊢ x ∈ Ico a b \ Ico c b ↔ x ∈ Ico a (min b c)
[PROOFSTEP]
rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
[GOAL]
case inr.a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
x : α
⊢ a ≤ x ∧ x < b ∧ (x < b → x < c) ↔ a ≤ x ∧ x < c
[PROOFSTEP]
exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ disjUnion (Ioi a) (Iio a) (_ : Disjoint (Ioi a) (Iio a)) = {a}ᶜ
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a a✝ : α
⊢ a✝ ∈ disjUnion (Ioi a) (Iio a) (_ : Disjoint (Ioi a) (Iio a)) ↔ a✝ ∈ {a}ᶜ
[PROOFSTEP]
simp [eq_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : a ≤ b
⊢ [[a, b]] = Icc a b
[PROOFSTEP]
rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b ≤ a
⊢ [[a, b]] = Icc b a
[PROOFSTEP]
rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c x a b : α
⊢ [[a, b]] = [[b, a]]
[PROOFSTEP]
rw [uIcc, uIcc, inf_comm, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ [[a, a]] = {a}
[PROOFSTEP]
simp [uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]
[PROOFSTEP]
rw [mem_uIcc] at h₁ h₂
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
h₂ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]
[PROOFSTEP]
exact Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂
[PROOFSTEP]
rw [mem_Icc] at ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂
[PROOFSTEP]
exact Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ [[b, c]] → b ∈ [[a, c]] → a = b
[PROOFSTEP]
simp_rw [mem_uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b
[PROOFSTEP]
exact Set.eq_of_mem_uIcc_of_mem_uIcc
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c
[PROOFSTEP]
simp_rw [mem_uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c
[PROOFSTEP]
exact Set.eq_of_mem_uIcc_of_mem_uIcc'
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : (fun b => [[b, a]]) b = (fun b => [[b, a]]) c
⊢ b = c
[PROOFSTEP]
rw [ext_iff] at h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (a_1 : α), a_1 ∈ (fun b => [[b, a]]) b ↔ a_1 ∈ (fun b => [[b, a]]) c
⊢ b = c
[PROOFSTEP]
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b b₁ b₂ c x a : α
⊢ Injective (uIcc a)
[PROOFSTEP]
simpa only [uIcc_comm] using uIcc_injective_right a
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ↑[[a, b]] = ↑(Icc a b ∪ Icc b a)
[PROOFSTEP]
push_cast
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
[PROOFSTEP]
exact Set.uIcc_eq_union
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
[PROOFSTEP]
simp [uIcc_eq_union]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ c < a → c < b → ¬c ∈ [[a, b]]
[PROOFSTEP]
rw [mem_uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ c < a → c < b → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)
[PROOFSTEP]
exact Set.not_mem_uIcc_of_lt
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a < c → b < c → ¬c ∈ [[a, b]]
[PROOFSTEP]
rw [mem_uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a < c → b < c → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)
[PROOFSTEP]
exact Set.not_mem_uIcc_of_gt
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ↑[[a, c]] ⊆ ↑([[a, b]] ∪ [[b, c]])
[PROOFSTEP]
push_cast
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c
[PROOFSTEP]
exact Set.uIcc_subset_uIcc_union_uIcc
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Icc a b = Set.Icc (c + a) (c + b)
[PROOFSTEP]
exact Set.image_const_add_Icc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Icc a b) = Icc (a + c) (b + c)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Icc a b = Set.Icc (a + c) (b + c)
[PROOFSTEP]
exact Set.image_add_const_Icc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Ico a b = Set.Ico (c + a) (c + b)
[PROOFSTEP]
exact Set.image_const_add_Ico _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ico a b) = Ico (a + c) (b + c)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Ico a b = Set.Ico (a + c) (b + c)
[PROOFSTEP]
exact Set.image_add_const_Ico _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)
[PROOFSTEP]
exact Set.image_const_add_Ioc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
[PROOFSTEP]
exact Set.image_add_const_Ioc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Ioo a b = Set.Ioo (c + a) (c + b)
[PROOFSTEP]
exact Set.image_const_add_Ioo _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ioo a b) = Ioo (a + c) (b + c)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)
[PROOFSTEP]
exact Set.image_add_const_Ioo _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
rw [← map_add_left_Icc, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Icc a b) = image (↑(addLeftEmbedding c)) (Icc a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
rw [← map_add_left_Ico, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ico a b) = image (↑(addLeftEmbedding c)) (Ico a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
rw [← map_add_left_Ioc, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioc a b) = image (↑(addLeftEmbedding c)) (Ioc a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
rw [← map_add_left_Ioo, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioo a b) = image (↑(addLeftEmbedding c)) (Ioo a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Icc a b) = Icc (a + c) (b + c)
[PROOFSTEP]
rw [← map_add_right_Icc, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Icc a b) = image (↑(addRightEmbedding c)) (Icc a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ico a b) = Ico (a + c) (b + c)
[PROOFSTEP]
rw [← map_add_right_Ico, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ico a b) = image (↑(addRightEmbedding c)) (Ico a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioc a b) = Ioc (a + c) (b + c)
[PROOFSTEP]
rw [← map_add_right_Ioc, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioc a b) = image (↑(addRightEmbedding c)) (Ioc a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioo a b) = Ioo (a + c) (b + c)
[PROOFSTEP]
rw [← map_add_right_Ioo, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioo a b) = image (↑(addRightEmbedding c)) (Ioo a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∏ i : ι, ∏ j in Ioi i, f j i * f i j = ∏ i : ι, ∏ j in {i}ᶜ, f j i
[PROOFSTEP]
simp_rw [← Ioi_disjUnion_Iio, prod_disjUnion, prod_mul_distrib]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ (∏ x : ι, ∏ x_1 in Ioi x, f x_1 x) * ∏ x : ι, ∏ x_1 in Ioi x, f x x_1 =
    (∏ x : ι, ∏ x_1 in Ioi x, f x_1 x) * ∏ x : ι, ∏ x_1 in Iio x, f x_1 x
[PROOFSTEP]
congr 1
[GOAL]
case e_a
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∏ x : ι, ∏ x_1 in Ioi x, f x x_1 = ∏ x : ι, ∏ x_1 in Iio x, f x_1 x
[PROOFSTEP]
rw [prod_sigma', prod_sigma']
[GOAL]
case e_a
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∏ x in Finset.sigma univ fun x => Ioi x, f x.fst x.snd = ∏ x in Finset.sigma univ fun x => Iio x, f x.snd x.fst
[PROOFSTEP]
refine' prod_bij' (fun i _ => ⟨i.2, i.1⟩) _ _ (fun i _ => ⟨i.2, i.1⟩) _ _ _
[GOAL]
case e_a.refine'_1
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Ioi x),
    (fun i x => { fst := i.snd, snd := i.fst }) a ha ∈ Finset.sigma univ fun x => Iio x
[PROOFSTEP]
simp
[GOAL]
case e_a.refine'_2
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Ioi x),
    f a.fst a.snd =
      f ((fun i x => { fst := i.snd, snd := i.fst }) a ha).snd ((fun i x => { fst := i.snd, snd := i.fst }) a ha).fst
[PROOFSTEP]
simp
[GOAL]
case e_a.refine'_3
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Iio x),
    (fun i x => { fst := i.snd, snd := i.fst }) a ha ∈ Finset.sigma univ fun x => Ioi x
[PROOFSTEP]
simp
[GOAL]
case e_a.refine'_4
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Ioi x),
    (fun i x => { fst := i.snd, snd := i.fst }) ((fun i x => { fst := i.snd, snd := i.fst }) a ha)
        (_ : { fst := a.snd, snd := a.fst } ∈ Finset.sigma univ fun x => Iio x) =
      a
[PROOFSTEP]
simp
[GOAL]
case e_a.refine'_5
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Iio x),
    (fun i x => { fst := i.snd, snd := i.fst }) ((fun i x => { fst := i.snd, snd := i.fst }) a ha)
        (_ : { fst := a.snd, snd := a.fst } ∈ Finset.sigma univ fun x => Ioi x) =
      a
[PROOFSTEP]
simp