awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
⊢ ι → α

Tactic:
exact fun i =>
          (u (Opposite.op ({i} : Finset ι))).val ⟨i, by simp only [mem_singleton]⟩

Premises used: Subtype.mk, Opposite.op, Singleton.singleton, Subtype.val
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
⊢ Subset (α := Finset ι) {i} {i, i'}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
⊢ Subset (α := Finset ι) {i} {i, i'}

Tactic:
have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : Subset (α := Finset ι) {i} {i, i'}
⊢ Subset (α := Finset ι) {i'} {i, i'}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : Subset (α := Finset ι) {i} {i, i'}
⊢ Subset (α := Finset ι) {i'} {i, i'}

Tactic:
have subi' : ({i'} : Finset ι) ⊆ {i, i'} := by simp
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : Subset (α := Finset ι) {i} {i, i'}
subi' : Subset (α := Finset ι) {i'} {i, i'}
⊢ LE.le (α := Finset ι) {i} {i, i'}

Tactic:
rw [← Finset.le_iff_subset] at subi subi'

Premises used: Finset.le_iff_subset
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : Subset (α := Finset ι) {i} {i, i'}
subi' : Subset (α := Finset ι) {i'} {i, i'}
subi₁ : LE.le (α := Finset ι) {i} {i, i'}
⊢ LE.le (α := Finset ι) {i'} {i, i'}

Tactic:
rw [← Finset.le_iff_subset] at subi subi'

Premises used: Finset.le_iff_subset
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : LE.le (α := Finset ι) {i} {i, i'}
subi' : LE.le (α := Finset ι) {i'} {i, i'}
mp :
  Eq.{v + 1} (α := α)
      ((↑(u (Opposite.op {i})) : ↥{i} → α) (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        α)
      ((↑(u (Opposite.op {i'})) : ↥{i'} → α)
          (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i'} x) i' ⋯) :
        α) →
    i = i'
⊢ Eq.{v + 1} (α := α)
      ((fun (i : ι) ↦
          ((↑(u (Opposite.op {i})) : ↥(Opposite.unop (Opposite.op {i})) → α)
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {i})) x) i ⋯) :
            α))
        i)
      ((fun (i : ι) ↦
          ((↑(u (Opposite.op {i})) : ↥(Opposite.unop (Opposite.op {i})) → α)
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {i})) x) i ⋯) :
            α))
        i') →
    i = i'

Tactic:
simp only
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : LE.le (α := Finset ι) {i} {i, i'}
subi' : LE.le (α := Finset ι) {i'} {i, i'}
mp :
  Eq.{v + 1} (α := α)
      ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((hallMatchingsFunctor t).map (homOfLE subi).op) :
                (a : (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i, i'}))) →
                  (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i})))
              (u (Opposite.op {i, i'}))) :
          ↥{i} → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((hallMatchingsFunctor t).map (homOfLE subi').op) :
                (a : (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i, i'}))) →
                  (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i'})))
              (u (Opposite.op {i, i'}))) :
          ↥{i'} → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i'} x) i' ⋯)) →
    i = i'
⊢ Eq.{v + 1} (α := α)
      ((↑(u (Opposite.op {i})) : ↥{i} → α) (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        α)
      ((↑(u (Opposite.op {i'})) : ↥{i'} → α)
          (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i'} x) i' ⋯) :
        α) →
    i = i'

Tactic:
rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]

Premises used: Quiver.Hom.op, CategoryTheory.homOfLE
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : LE.le (α := Finset ι) {i} {i, i'}
subi' : LE.le (α := Finset ι) {i'} {i, i'}
uii' : (hallMatchingsFunctor t).obj (Opposite.op {i, i'}) := u (Opposite.op {i, i'})
⊢ Eq.{v + 1} (α := α)
      ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((hallMatchingsFunctor t).map (homOfLE subi).op) :
                (a : (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i, i'}))) →
                  (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i})))
              (u (Opposite.op {i, i'}))) :
          ↥{i} → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((hallMatchingsFunctor t).map (homOfLE subi').op) :
                (a : (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i, i'}))) →
                  (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i'})))
              (u (Opposite.op {i, i'}))) :
          ↥{i'} → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i'} x) i' ⋯)) →
    i = i'

Tactic:
fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)

Premises used: And.left, Subtype.mk_eq_mk, Iff.mp, Subtype.property
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : LE.le (α := Finset ι) {i} {i, i'}
subi' : LE.le (α := Finset ι) {i'} {i, i'}
uii' : (hallMatchingsFunctor t).obj (Opposite.op {i, i'}) := u (Opposite.op {i, i'})
⊢ Eq.{v + 1} (α := α)
      ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((hallMatchingsFunctor t).map (homOfLE subi).op) :
                (a : (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i, i'}))) →
                  (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i})))
              (u (Opposite.op {i, i'}))) :
          ↥{i} → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((hallMatchingsFunctor t).map (homOfLE subi').op) :
                (a : (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i, i'}))) →
                  (fun (X : Type (max v u)) ↦ X) ((hallMatchingsFunctor t).obj (Opposite.op {i'})))
              (u (Opposite.op {i, i'}))) :
          ↥{i'} → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i'} x) i' ⋯)) →
    i = i'

Tactic:
exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)

Premises used: And.left, Subtype.mk_eq_mk, Iff.mp, Subtype.property
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this_1 : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i : ι
⊢ Membership.mem (α := α) (t i)
    ((↑(u (Opposite.op {i})) : ↥(Opposite.unop (Opposite.op {i})) → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {i})) x) i ⋯) :
      α)

Tactic:
apply (u (Opposite.op ({i} : Finset ι))).property.2

Premises used: And.right, Opposite.op, Singleton.singleton, Subtype.property
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
mpr : #(image f s) ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)

Tactic:
rw [← Finset.card_image_of_injective s hf₁]

Premises used: Finset.card_image_of_injective
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
mpr : image f s ⊆ s.biUnion t
⊢ #(image f s) ≤ #(s.biUnion t)

Tactic:
apply Finset.card_le_card

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ image f s ⊆ s.biUnion t

Tactic:
grind
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
A : Finset α
h : ∀ (x : β), x ∈ R.image (↑A : Set α) ↔ x ∈ (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)
⊢ R.image (↑A : Set α) = (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)

Tactic:
ext
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
A : Finset α
x : β
⊢ x ∈ R.image (↑A : Set α) ↔ x ∈ (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)

Tactic:
simp [SetRel.image]

Premises used: SetRel.image
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
A : Finset α
⊢ R.image (↑A : Set α) = (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)

Tactic:
have h : R.image A = (A.biUnion fun a => (R.image {a}).toFinset : Set β) := by
    ext
    simp [SetRel.image]
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
A : Finset α
h : R.image (↑A : Set α) = (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)
rw : Fintype (↑(↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β) : Type v)
⊢ Fintype (↑(R.image (↑A : Set α)) : Type v)

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
A : Finset α
h : R.image (↑A : Set α) = (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)
⊢ Fintype (↑(↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β) : Type v)

Tactic:
apply FinsetCoe.fintype

Premises used: FinsetCoe.fintype
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
A : Finset α
rw : #(R.image (↑A : Set α)).toFinset = #(A.biUnion r')
⊢ card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')

Tactic:
rw [← Set.toFinset_card]

Premises used: Set.toFinset_card
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
A : Finset α
h : (R.image (↑A : Set α)).toFinset = A.biUnion r'
⊢ #(R.image (↑A : Set α)).toFinset = #(A.biUnion r')

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
A : Finset α
h : ∀ (b : β), b ∈ (R.image (↑A : Set α)).toFinset ↔ b ∈ A.biUnion r'
⊢ (R.image (↑A : Set α)).toFinset = A.biUnion r'

Tactic:
ext b
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
A : Finset α
b : β
⊢ b ∈ (R.image (↑A : Set α)).toFinset ↔ b ∈ A.biUnion r'

Tactic:
simp [r', SetRel.image]

Premises used: SetRel.image
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
⊢ ∀ (A : Finset α), card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')

Tactic:
have h : ∀ A : Finset α, Fintype.card (R.image A) = #(A.biUnion r') := by
    intro A
    rw [← Set.toFinset_card]
    apply congr_arg
    ext b
    simp [r', SetRel.image]
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
h : ∀ (A : Finset α), card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')
⊢ ∀ (f : α → β) (x : α), (x, f x) ∈ R ↔ f x ∈ r' x

Tactic:
simp [r', SetRel.image]

Premises used: SetRel.image
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
h : ∀ (A : Finset α), card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')
⊢ ∀ (f : α → β) (x : α), (x, f x) ∈ R ↔ f x ∈ r' x

Tactic:
have h' : ∀ (f : α → β) (x), x ~[R] f x ↔ f x ∈ r' x := by simp [r', SetRel.image]
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
h : ∀ (A : Finset α), card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')
h' : ∀ (f : α → β) (x : α), (x, f x) ∈ R ↔ f x ∈ r' x
simp : (∀ (A : Finset α), #A ≤ #(A.biUnion r')) ↔ ∃ (f : α → β), Injective f ∧ ∀ (x : α), f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ card.{v} (↑(R.image (↑A : Set α)) : Type v)) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), (x, f x) ∈ R

Tactic:
simp only [h, h']
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
h : ∀ (A : Finset α), card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')
h' : ∀ (f : α → β) (x : α), (x, f x) ∈ R ↔ 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

Premises used: Finset.all_card_le_biUnion_card_iff_exists_injective
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
haveI :
  ∀ (this : DecidableEq β),
    (∀ (A : Finset α), #A ≤ Finset.card.{v} (α := β) {b : β | ∃ a ∈ A, r a b}) ↔
      ∃ (f : α → β), Injective f ∧ ∀ (x : α), r x (f x)
⊢ (∀ (A : Finset α), #A ≤ Finset.card.{v} (α := β) {b : β | ∃ a ∈ A, r a b}) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
haveI := Classical.decEq β
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
A : Finset α
h : ∀ (b : β), Membership.mem (γ := Finset β) {b : β | ∃ a ∈ A, r a b} b ↔ b ∈ A.biUnion r'
⊢ {b : β | ∃ a ∈ A, r a b} = A.biUnion r'

Tactic:
ext b
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
A : Finset α
b : β
⊢ Membership.mem (γ := Finset β) {b : β | ∃ a ∈ A, r a b} b ↔ b ∈ A.biUnion r'

Tactic:
simp [r']
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
⊢ ∀ (A : Finset α), {b : β | ∃ a ∈ A, r a b} = A.biUnion r'

Tactic:
have h : ∀ A : Finset α, ({b | ∃ a ∈ A, r a b} : Finset _) = A.biUnion r' := by
    intro A
    ext b
    simp [r']
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
h : ∀ (A : Finset α), {b : β | ∃ a ∈ A, r a b} = A.biUnion r'
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x

Tactic:
simp [r']
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
h : ∀ (A : Finset α), {b : β | ∃ a ∈ A, r a b} = A.biUnion r'
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x

Tactic:
have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp [r']
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
h : ∀ (A : Finset α), {b : β | ∃ a ∈ A, r a b} = A.biUnion r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
simp_rw : (∀ (A : Finset α), #A ≤ #(A.biUnion r')) ↔ ∃ (f : α → β), Injective f ∧ ∀ (x : α), f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ Finset.card.{v} (α := β) {b : β | ∃ a ∈ A, r a b}) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
simp_rw [h, h']
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
h : ∀ (A : Finset α), {b : β | ∃ a ∈ A, r a b} = 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

Premises used: Finset.all_card_le_biUnion_card_iff_exists_injective
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
haveI :
  ∀ (this : DecidableEq ι),
    #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)

Tactic:
haveI := Classical.decEq ι
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
⊢ Finset.Nonempty (α := ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      card (α := ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') <
        #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)

Tactic:
specialize ha (s'.image fun z => z.1)

Premises used: Finset.image
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  Finset.Nonempty (α := ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      card (α := ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') <
        #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
⊢ s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)

Tactic:
rw [image_nonempty, Finset.card_image_of_injective s' Subtype.coe_injective] at ha

Premises used: Finset.image_nonempty, Finset.card_image_of_injective, Subtype.coe_injective