-- Mathlib/Combinatorics/Hall/Basic.lean
theorem Fintype.all_card_le_rel_image_card_iff_exists_injective {α : Type u} {β : Type v}
    [DecidableEq β] (r : α → β → Prop) [∀ a : α, Fintype (Rel.image r {a})] :
    (∀ A : Finset α, #A ≤ Fintype.card (Rel.image r A)) ↔
      ∃ f : α → β, Function.Injective f ∧ ∀ x, r x (f x)

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = #(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✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = #(A.biUnion r')
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
simp only [h, h']

Result:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = #(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✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = #(A.biUnion r')
⊢ (∀ (A : Finset α), #A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

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

Result:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = #(A.biUnion r')
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
A : Finset α
⊢ card ↑(Rel.image r ↑A) = #(A.biUnion r')

Tactic:
rw [← Set.toFinset_card]

Result:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
A : Finset α
⊢ #(Rel.image r ↑A).toFinset = #(A.biUnion r')

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
⊢ (∀ (A : Finset α), #A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
have h : ∀ A : Finset α, Fintype.card (Rel.image r A) = #(A.biUnion r') := by
  intro A
  rw [← Set.toFinset_card]
  apply congr_arg
  ext b
  simp [r', Rel.image]

Result:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = #(A.biUnion r')
⊢ (∀ (A : Finset α), #A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
⊢ ∀ (A : Finset α), card ↑(Rel.image r ↑A) = #(A.biUnion r')

Tactic:
intro A

Result:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
A : Finset α
⊢ card ↑(Rel.image r ↑A) = #(A.biUnion r')

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
A : Finset α
⊢ #(Rel.image r ↑A).toFinset = #(A.biUnion r')

Tactic:
apply congr_arg

Result:
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
A : Finset α
⊢ (Rel.image r ↑A).toFinset = A.biUnion r'

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
⊢ (∀ (A : Finset α), #A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
let r' a := (Rel.image r {a}).toFinset

Result:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
⊢ (∀ (A : Finset α), #A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Proof state:
case h.h
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
A : Finset α
b : β
⊢ b ∈ (Rel.image r ↑A).toFinset ↔ b ∈ A.biUnion r'

Tactic:
simp [r', Rel.image]

Result:
no goals

Proof state:
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
A : Finset α
⊢ (Rel.image r ↑A).toFinset = A.biUnion r'

Tactic:
ext b

Result:
case h.h
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
A : Finset α
b : β
⊢ b ∈ (Rel.image r ↑A).toFinset ↔ b ∈ A.biUnion r'

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => (Rel.image r {a}).toFinset
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = #(A.biUnion r')
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x

Tactic:
simp [r', Rel.image]

Result:
no goals