-- Mathlib/Combinatorics/Hall/Basic.lean
theorem Fintype.all_card_le_filter_rel_iff_exists_injective {α : Type u} {β : Type v} [Fintype β]
    (r : α → β → Prop) [∀ a, DecidablePred (r a)] :
    (∀ A : Finset α, #A ≤ #{b | ∃ a ∈ A, r a b}) ↔ ∃ f : α → β, Injective f ∧ ∀ x, r x (f x)

Proof state:
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
⊢ (∀ (A : Finset α), #A ≤ #(filter (fun b => ∃ a ∈ A, r a b) univ)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
let r' a : Finset β := {b | r a b}

Result:
α : 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 α), #A ≤ #(filter (fun b => ∃ a ∈ A, r a b) univ)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Proof state:
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
⊢ (∀ (A : Finset α), #A ≤ #(filter (fun b => ∃ a ∈ A, r a b) univ)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
haveI := Classical.decEq β

Result:
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
⊢ (∀ (A : Finset α), #A ≤ #(filter (fun b => ∃ a ∈ A, r a b) univ)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Proof state:
α : 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, r a b) univ = A.biUnion r'

Tactic:
ext b

Result:
case h
α : 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, r a b) univ ↔ b ∈ A.biUnion r'

Proof state:
case h
α : 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, r a b) univ ↔ b ∈ A.biUnion r'

Tactic:
simp [r']

Result:
no goals

Proof state:
α : 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, r a b) univ = A.biUnion r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ #(A.biUnion r')) ↔ ∃ f, Injective f ∧ ∀ (x : α), f x ∈ r' x

Tactic:
apply Finset.all_card_le_biUnion_card_iff_exists_injective

Result:
no goals

Proof state:
α : 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 α), #A ≤ #(filter (fun b => ∃ a ∈ A, r a b) univ)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
have h : ∀ A : Finset α, ({b | ∃ a ∈ A, r a b} : Finset _) = A.biUnion r' := by
  intro A
  ext b
  simp [r']

Result:
α : 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, r a b) univ = A.biUnion r'
⊢ (∀ (A : Finset α), #A ≤ #(filter (fun b => ∃ a ∈ A, r a b) univ)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Proof state:
α : 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, r a b) univ = A.biUnion r'
⊢ (∀ (A : Finset α), #A ≤ #(filter (fun b => ∃ a ∈ A, r a b) univ)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp [r']

Result:
α : 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, r a b) univ = A.biUnion r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ #(filter (fun b => ∃ a ∈ A, r a b) univ)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Proof state:
α : 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, r a b) univ = A.biUnion r'

Tactic:
intro A

Result:
α : 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, r a b) univ = A.biUnion r'

Proof state:
α : 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, r a b) univ = A.biUnion r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ #(filter (fun b => ∃ a ∈ A, r a b) univ)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
simp_rw [h, h']

Result:
α : 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, r a b) univ = A.biUnion r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ #(A.biUnion r')) ↔ ∃ f, Injective f ∧ ∀ (x : α), f x ∈ r' x

Proof state:
α : 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, r a b) univ = A.biUnion r'
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x

Tactic:
simp [r']

Result:
no goals