α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
haveI := Classical.decEq β
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
let r' a := univ.filter fun b => r a b
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
have h : ∀ A : Finset α, (univ.filter fun b : β => ∃ a ∈ A, r a b) = A.biUnion r' := by
  intro A
  ext b
  simp
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (Finset.biUnion A fun a => filter (fun b => r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), f x ∈ filter (fun b => r x b) univ
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
simp_rw [h, h']
no goals
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (Finset.biUnion A fun a => filter (fun b => r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), f x ∈ filter (fun b => r x b) univ
apply Finset.all_card_le_biUnion_card_iff_exists_injective
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
A : Finset α
⊢ filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
⊢ ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
intro A
case a
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
A : Finset α
b : β
⊢ b ∈ filter (fun b => ∃ a, a ∈ A ∧ r a b) univ ↔ b ∈ Finset.biUnion A r'
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
A : Finset α
⊢ filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
ext b
no goals
case a
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
A : Finset α
b : β
⊢ b ∈ filter (fun b => ∃ a, a ∈ A ∧ r a b) univ ↔ b ∈ Finset.biUnion A r'
simp
no goals
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
simp