ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), Finset.Nonempty s → s ≠ univ → card s < card (Finset.biUnion s t)
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), Finset.Nonempty s → s ≠ univ → card s < card (Finset.biUnion s t)
s' : Finset ↑{x' | x' ≠ x}
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
haveI := Classical.decEq ι
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha :
  Finset.Nonempty (image (fun z => ↑z) s') →
    image (fun z => ↑z) s' ≠ univ → card (image (fun z => ↑z) s') < card (Finset.biUnion (image (fun z => ↑z) s') t)
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), Finset.Nonempty s → s ≠ univ → card s < card (Finset.biUnion s t)
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
specialize ha (s'.image fun z => z.1)
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha :
  Finset.Nonempty (image (fun z => ↑z) s') →
    image (fun z => ↑z) s' ≠ univ → card (image (fun z => ↑z) s') < card (Finset.biUnion (image (fun z => ↑z) s') t)
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
rw [Nonempty.image_iff, Finset.card_image_of_injective s' Subtype.coe_injective] at ha
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)

case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : ¬Finset.Nonempty s'
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
by_cases he : s'.Nonempty
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
have ha' : s'.card < (s'.biUnion fun x => t x).card := by
  convert ha he fun h => by simpa [← h] using mem_univ x using 2
  ext x
  simp only [mem_image, mem_biUnion, exists_prop, SetCoe.exists, exists_and_right,
    exists_eq_right, Subtype.coe_mk]
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
⊢ card s' ≤ card (erase (Finset.biUnion s' fun x' => t ↑x') a)
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
rw [← erase_biUnion]
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
hb : a ∈ Finset.biUnion s' fun x_1 => t ↑x_1
⊢ card s' ≤ card (erase (Finset.biUnion s' fun x' => t ↑x') a)

case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
hb : ¬a ∈ Finset.biUnion s' fun x_1 => t ↑x_1
⊢ card s' ≤ card (erase (Finset.biUnion s' fun x' => t ↑x') a)
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
⊢ card s' ≤ card (erase (Finset.biUnion s' fun x' => t ↑x') a)
by_cases hb : a ∈ s'.biUnion fun x => t x
case h.e'_4.h.e'_2
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
⊢ (Finset.biUnion s' fun x_1 => t ↑x_1) = Finset.biUnion (image (fun z => ↑z) s') t
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
⊢ card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
convert ha he fun h => by simpa [← h] using mem_univ x using 2
case h.e'_4.h.e'_2.a
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x✝ : ι
a : α
s' : Finset ↑{x' | x' ≠ x✝}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
x : α
⊢ (x ∈ Finset.biUnion s' fun x => t ↑x) ↔ x ∈ Finset.biUnion (image (fun z => ↑z) s') t
case h.e'_4.h.e'_2
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
⊢ (Finset.biUnion s' fun x_1 => t ↑x_1) = Finset.biUnion (image (fun z => ↑z) s') t
ext x
no goals
case h.e'_4.h.e'_2.a
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x✝ : ι
a : α
s' : Finset ↑{x' | x' ≠ x✝}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
x : α
⊢ (x ∈ Finset.biUnion s' fun x => t ↑x) ↔ x ∈ Finset.biUnion (image (fun z => ↑z) s') t
simp only [mem_image, mem_biUnion, exists_prop, SetCoe.exists, exists_and_right,
  exists_eq_right, Subtype.coe_mk]
no goals
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
h : image (fun z => ↑z) s' = univ
⊢ False
simpa [← h] using mem_univ x
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
hb : a ∈ Finset.biUnion s' fun x_1 => t ↑x_1
⊢ card s' ≤ card (Finset.biUnion s' fun x_1 => t ↑x_1) - 1
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
hb : a ∈ Finset.biUnion s' fun x_1 => t ↑x_1
⊢ card s' ≤ card (erase (Finset.biUnion s' fun x' => t ↑x') a)
rw [card_erase_of_mem hb]
no goals
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
hb : a ∈ Finset.biUnion s' fun x_1 => t ↑x_1
⊢ card s' ≤ card (Finset.biUnion s' fun x_1 => t ↑x_1) - 1
exact Nat.le_pred_of_lt ha'
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
hb : ¬a ∈ Finset.biUnion s' fun x_1 => t ↑x_1
⊢ card s' ≤ card (Finset.biUnion s' fun x_1 => t ↑x_1)
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
hb : ¬a ∈ Finset.biUnion s' fun x_1 => t ↑x_1
⊢ card s' ≤ card (erase (Finset.biUnion s' fun x' => t ↑x') a)
rw [erase_eq_of_not_mem hb]
no goals
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : Finset.Nonempty s'
ha' : card s' < card (Finset.biUnion s' fun x_1 => t ↑x_1)
hb : ¬a ∈ Finset.biUnion s' fun x_1 => t ↑x_1
⊢ card s' ≤ card (Finset.biUnion s' fun x_1 => t ↑x_1)
exact Nat.le_of_lt ha'
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : s' = ∅
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : ¬Finset.Nonempty s'
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
rw [nonempty_iff_ne_empty, not_not] at he
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
this : DecidableEq ι
ha : Finset.Nonempty ∅ → image (fun z => ↑z) ∅ ≠ univ → card ∅ < card (Finset.biUnion (image (fun z => ↑z) ∅) t)
⊢ card ∅ ≤ card (Finset.biUnion ∅ fun x' => erase (t ↑x') a)
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : Finset.Nonempty s' → image (fun z => ↑z) s' ≠ univ → card s' < card (Finset.biUnion (image (fun z => ↑z) s') t)
he : s' = ∅
⊢ card s' ≤ card (Finset.biUnion s' fun x' => erase (t ↑x') a)
subst s'
no goals
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
this : DecidableEq ι
ha : Finset.Nonempty ∅ → image (fun z => ↑z) ∅ ≠ univ → card ∅ < card (Finset.biUnion (image (fun z => ↑z) ∅) t)
⊢ card ∅ ≤ card (Finset.biUnion ∅ fun x' => erase (t ↑x') a)
simp