awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
ι : Type
w : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ)
    (fun (x : ι → Shrink.{0, u_7} η → α) ↦
      C fun (x_1 : ι × Shrink.{0, u_7} η) ↦
        match (motive := ι × Shrink.{0, u_7} η → α) x_1 with
        | (i, e) => x i e)
    l
h :
  ∀ (x : ι × Shrink.{0, u_7} η → α),
    x =
      (⇑(Equiv.refl α).symm : (a : α) → α) ∘
        x ∘ (⇑(Equiv.refl (ι × Shrink.{0, u_7} η)) : (a : ι × Shrink.{0, u_7} η) → ι × Shrink.{0, u_7} η)
⊢ IsMono C (l.toSubspace.reindex (Equiv.symm (equivShrink η)) (Equiv.refl α) (Equiv.refl (ι × Shrink.{0, u_7} η)))

Tactic:
convert! hl.toSubspace.reindex

Premises used: Combinatorics.Subspace.IsMono.reindex, Combinatorics.Line.IsMono.toSubspace
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
ι : Type
w : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ)
    (fun (x : ι → Shrink.{0, u_7} η → α) ↦
      C fun (x_1 : ι × Shrink.{0, u_7} η) ↦
        match (motive := ι × Shrink.{0, u_7} η → α) x_1 with
        | (i, e) => x i e)
    l
x : ι × Shrink.{0, u_7} η → α
⊢ x =
    (⇑(Equiv.refl α).symm : (a : α) → α) ∘
      x ∘ (⇑(Equiv.refl (ι × Shrink.{0, u_7} η)) : (a : ι × Shrink.{0, u_7} η) → ι × Shrink.{0, u_7} η)

Tactic:
simp
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
obtain :
  ∀ (ι : Type) (ιfin : Fintype ι) (hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l),
    ∃ (n : ℕ), ∀ (C : (Fin n → α) → κ), ∃ (l : Subspace η α (Fin n)), IsMono C l
⊢ ∃ (n : ℕ), ∀ (C : (Fin n → α) → κ), ∃ (l : Subspace η α (Fin n)), IsMono C l

Tactic:
obtain ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension α κ η

Premises used: Combinatorics.Subspace.exists_mono_in_high_dimension
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
⊢ ∃ (n : ℕ), ∀ (C : (Fin n → α) → κ), ∃ (l : Subspace η α (Fin n)), IsMono C l

Tactic:
⟨Fintype.card ι, fun C ↦ ?_⟩

Premises used: Fintype.card, Exists.intro
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
refine : ∀ (C : (Fin (Fintype.card ι) → α) → κ), ∃ (l : Subspace η α (Fin (Fintype.card ι))), IsMono C l
⊢ ∃ (n : ℕ), ∀ (C : (Fin n → α) → κ), ∃ (l : Subspace η α (Fin n)), IsMono C l

Tactic:
refine ⟨Fintype.card ι, fun C ↦ ?_⟩
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
obtain :
  ∀ (l : Subspace η α ι) (c : κ)
    (cl :
      ∀ (x : η → α),
        (fun (v : ι → α) ↦ C (v ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)))
            ((↑l : (x : η → α) → (i : ι) → α) x) =
          c),
    ∃ (l : Subspace η α (Fin (Fintype.card ι))), IsMono C l
⊢ ∃ (l : Subspace η α (Fin (Fintype.card ι))), IsMono C l

Tactic:
obtain ⟨l, c, cl⟩ := hι fun v ↦ C (v ∘ (Fintype.equivFin _).symm)

Premises used: Function.comp, Fintype.equivFin, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl :
  ∀ (x : η → α),
    (fun (v : ι → α) ↦ C (v ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)))
        ((↑l : (x : η → α) → (i : ι) → α) x) =
      c
⊢ ∃ (l : Subspace η α (Fin (Fintype.card ι))), IsMono C l

Tactic:
⟨⟨l.idxFun ∘ (Fintype.equivFin _).symm, fun e ↦ ?_⟩, c, cl⟩

Premises used: Combinatorics.Subspace.idxFun, Function.comp, Combinatorics.Subspace.mk, Fintype.equivFin, Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl :
  ∀ (x : η → α),
    (fun (v : ι → α) ↦ C (v ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)))
        ((↑l : (x : η → α) → (i : ι) → α) x) =
      c
refine :
  ∀ (e : η),
    ∃ (i : Fin (Fintype.card ι)),
      (l.idxFun ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)) i = Sum.inr e
⊢ ∃ (l : Subspace η α (Fin (Fintype.card ι))), IsMono C l

Tactic:
refine ⟨⟨l.idxFun ∘ (Fintype.equivFin _).symm, fun e ↦ ?_⟩, c, cl⟩
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl :
  ∀ (x : η → α),
    (fun (v : ι → α) ↦ C (v ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)))
        ((↑l : (x : η → α) → (i : ι) → α) x) =
      c
e : η
obtain :
  ∀ (i : ι) (hi : l.idxFun i = Sum.inr e),
    ∃ (i : Fin (Fintype.card ι)),
      (l.idxFun ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)) i = Sum.inr e
⊢ ∃ (i : Fin (Fintype.card ι)),
    (l.idxFun ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)) i = Sum.inr e

Tactic:
obtain ⟨i, hi⟩ := l.proper e

Premises used: Combinatorics.Subspace.proper
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl :
  ∀ (x : η → α),
    (fun (v : ι → α) ↦ C (v ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)))
        ((↑l : (x : η → α) → (i : ι) → α) x) =
      c
e : η
i : ι
hi : l.idxFun i = Sum.inr e
h :
  comp (α := Fin (Fintype.card ι)) l.idxFun
      ((⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι) : (a : Fin (Fintype.card ι)) → ι)
      ((Fintype.equivFin ι : (a : ι) → Fin (Fintype.card ι)) i : Fin (Fintype.card ι)) =
    Sum.inr e
⊢ ∃ (i : Fin (Fintype.card ι)),
    (l.idxFun ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)) i = Sum.inr e

Tactic:
use Fintype.equivFin _ i

Premises used: Fintype.equivFin, DFunLike.coe
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl :
  ∀ (x : η → α),
    (fun (v : ι → α) ↦ C (v ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)))
        ((↑l : (x : η → α) → (i : ι) → α) x) =
      c
e : η
i : ι
hi : l.idxFun i = Sum.inr e
⊢ comp (α := Fin (Fintype.card ι)) l.idxFun
      ((⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι) : (a : Fin (Fintype.card ι)) → ι)
      ((Fintype.equivFin ι : (a : ι) → Fin (Fintype.card ι)) i : Fin (Fintype.card ι)) =
    Sum.inr e

Tactic:
simpa using hi
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : (↑(hallMatchingsOn t ι'') : Type (max u v))
refine : (fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) ⋯)) ∈ hallMatchingsOn t ι'
⊢ (↑(hallMatchingsOn t ι') : Type (max u v))

Tactic:
refine ⟨fun i => f.val ⟨i, h i.property⟩, ?_⟩
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : (↑(hallMatchingsOn t ι'') : Type (max u v))
⊢ Injective (↑f : ↥ι'' → α)

Tactic:
obtain ⟨hinj, hc⟩ := f.property

Premises used: Subtype.property
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : (↑(hallMatchingsOn t ι'') : Type (max u v))
hinj : Injective (↑f : ↥ι'' → α)
⊢ ∀ (x : ↥ι''), (↑f : ↥ι'' → α) x ∈ t (↑x : ι)

Tactic:
obtain ⟨hinj, hc⟩ := f.property

Premises used: Subtype.property
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : (↑(hallMatchingsOn t ι'') : Type (max u v))
hinj : Injective (↑f : ↥ι'' → α)
hc : ∀ (x : ↥ι''), (↑f : ↥ι'' → α) x ∈ t (↑x : ι)
⊢ (fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) ⋯)) ∈ hallMatchingsOn t ι'

Tactic:
⟨?_, fun i => hc ⟨i, h i.property⟩⟩

Premises used: Set.Mem, hallMatchingsOn, setOf, Subtype.mk, And.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : (↑(hallMatchingsOn t ι'') : Type (max u v))
hinj : Injective (↑f : ↥ι'' → α)
hc : ∀ (x : ↥ι''), (↑f : ↥ι'' → α) x ∈ t (↑x : ι)
refine :
  Injective.{u + 1, v + 1} (β := α) fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) ⋯)
⊢ (fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) ⋯)) ∈ hallMatchingsOn t ι'

Tactic:
refine ⟨?_, fun i => hc ⟨i, h i.property⟩⟩
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : (↑(hallMatchingsOn t ι'') : Type (max u v))
hinj : Injective (↑f : ↥ι'' → α)
hc : ∀ (x : ↥ι''), (↑f : ↥ι'' → α) x ∈ t (↑x : ι)
i : ι
hi : i ∈ ι'
j : ι
hj : j ∈ ι'
hh :
  Eq.{v + 1} (α := α)
    ((fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) ⋯))
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') i hi))
    ((fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) ⋯))
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') j hj))
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') i hi = Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') j hj

Tactic:
simpa only [Subtype.mk_eq_mk] using hinj hh

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
⊢ Nonempty (↑(hallMatchingsOn t ι') : Type (max u v))

Tactic:
⟨Classical.indefiniteDescription _ ?_⟩

Premises used: Classical.indefiniteDescription, Nonempty.intro
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
refine : ∃ (x : ↥ι' → α), x ∈ hallMatchingsOn t ι'
⊢ Nonempty (↑(hallMatchingsOn t ι') : Type (max u v))

Tactic:
refine ⟨Classical.indefiniteDescription _ ?_⟩
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
apply : ∀ (s : Finset ↥ι'), #s ≤ card.{v} (α := α) (s.biUnion fun (i : ↥ι') ↦ t (↑i : ι))
⊢ ∃ (x : ↥ι' → α), x ∈ hallMatchingsOn t ι'

Tactic:
apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp

Premises used: Finset.all_card_le_biUnion_card_iff_existsInjective', Iff.mp, Subtype.val
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
⊢ #(image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s') ≤
    #((image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s').biUnion t)

Tactic:
h (s'.image (↑))

Premises used: Finset.image
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
h₁ : #s' = #(image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s')
h₂ :
  card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι)) =
    #((image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s').biUnion t)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι))

Tactic:
convert! h (s'.image (↑)) using 1

Premises used: Finset.image
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
⊢ #s' = #(image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s')

Tactic:
simp only [card_image_of_injective s' Subtype.coe_injective]

Premises used: Finset.card_image_of_injective, Subtype.coe_injective
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
h₁ h₂ :
  card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι)) = card.{v} (α := α) (s'.biUnion fun (a : ↥ι') ↦ t (↑a : ι))
⊢ card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι)) =
    #((image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s').biUnion t)

Tactic:
rw [image_biUnion]

Premises used: Finset.image_biUnion
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
refine : ∃ (x : ↥ι' → α), x ∈ hallMatchingsOn t ι'
refine₁ refine₂ : ∀ (s' : Finset ↥ι'), #s' ≤ card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι))
h₁ : ∀ (s' : Finset ↥ι'), #s' = #(image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s')
h₂ h₃ :
  ∀ (s' : Finset ↥ι'),
    card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι)) =
      #((image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s').biUnion t)
⊢ Nonempty (↑(hallMatchingsOn t ι') : Type (max u v))

Tactic:
classical
    refine ⟨Classical.indefiniteDescription _ ?_⟩
    apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp
    intro s'
    convert! h (s'.image (↑)) using 1
    · simp only [card_image_of_injective s' Subtype.coe_injective]
    · rw [image_biUnion]

Premises used: Finset.all_card_le_biUnion_card_iff_existsInjective', Finset.image_biUnion, Iff.mp, Subtype.val
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : (↑(hallMatchingsOn t ι') : Type (max u v))
i : ↥ι'
refine : (↑f : ↥ι' → α) i ∈ ι'.biUnion t
⊢ ↥(ι'.biUnion t)

Tactic:
refine ⟨f.val i, ?_⟩
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : (↑(hallMatchingsOn t ι') : Type (max u v))
i : ↥ι'
rw : ∃ a ∈ ι', (↑f : ↥ι' → α) i ∈ t a
⊢ (↑f : ↥ι' → α) i ∈ ι'.biUnion t

Tactic:
rw [mem_biUnion]

Premises used: Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : (↑(hallMatchingsOn t ι') : Type (max u v))
i : ↥ι'
⊢ ∃ a ∈ ι', (↑f : ↥ι' → α) i ∈ t a

Tactic:
⟨i, i.property, f.property.2 i⟩

Premises used: And.right, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : (↑(hallMatchingsOn t ι') : Type (max u v))
i : ↥ι'
⊢ ∃ a ∈ ι', (↑f : ↥ι' → α) i ∈ t a

Tactic:
exact ⟨i, i.property, f.property.2 i⟩
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : (↑(hallMatchingsOn t ι') : Type (max u v)) → ↥ι' → ↥(ι'.biUnion t) :=
  fun (f : (↑(hallMatchingsOn t ι') : Type (max u v))) (i : ↥ι') ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ ι'.biUnion t) ((↑f : ↥ι' → α) i) ⋯
apply : Injective g
⊢ Finite (↑{f : ↥ι' → α | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t (↑x : ι)} : Type (max u v))

Tactic:
apply Finite.of_injective g

Premises used: Finite.of_injective
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : (↑(hallMatchingsOn t ι') : Type (max u v)) → ↥ι' → ↥(ι'.biUnion t) :=
  fun (f : (↑(hallMatchingsOn t ι') : Type (max u v))) (i : ↥ι') ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ ι'.biUnion t) ((↑f : ↥ι' → α) i) ⋯
f f' : (↑(hallMatchingsOn t ι') : Type (max u v))
h : g f = g f'
a : ∀ (a : ↥ι'), (↑f : ↥ι' → α) a = (↑f' : ↥ι' → α) a
⊢ f = f'

Tactic:
ext a
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : (↑(hallMatchingsOn t ι') : Type (max u v)) → ↥ι' → ↥(ι'.biUnion t) :=
  fun (f : (↑(hallMatchingsOn t ι') : Type (max u v))) (i : ↥ι') ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ ι'.biUnion t) ((↑f : ↥ι' → α) i) ⋯
f f' : (↑(hallMatchingsOn t ι') : Type (max u v))
h : g f = g f'
a : ↥ι'
a₁ : ∀ (h : ∀ (x : ↥ι'), g f x = g f' x) (a : ↥ι'), (↑f : ↥ι' → α) a = (↑f' : ↥ι' → α) a
⊢ (↑f : ↥ι' → α) a = (↑f' : ↥ι' → α) a

Tactic:
rw [funext_iff] at h

Premises used: funext_iff
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : (↑(hallMatchingsOn t ι') : Type (max u v)) → ↥ι' → ↥(ι'.biUnion t) :=
  fun (f : (↑(hallMatchingsOn t ι') : Type (max u v))) (i : ↥ι') ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ ι'.biUnion t) ((↑f : ↥ι' → α) i) ⋯
f f' : (↑(hallMatchingsOn t ι') : Type (max u v))
h : ∀ (x : ↥ι'), g f x = g f' x
a : ↥ι'
⊢ (↑f : ↥ι' → α) a = (↑f' : ↥ι' → α) a

Tactic:
simpa [g] using h a
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
rw rw₁ rw₂ : Finite (↑{f : ↥ι' → α | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t (↑x : ι)} : Type (max u v))
rw₃ : Finite (↑{f : ↥ι' → α | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t (↑x : ι)} : Type (max u v))
rw₄ :
  let g : (↑(hallMatchingsOn t ι') : Type (max u v)) → ↥ι' → ↥(ι'.biUnion t) :=
    fun (f : (↑(hallMatchingsOn t ι') : Type (max u v))) (i : ↥ι') ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ ι'.biUnion t) ((↑f : ↥ι' → α) i) ⋯;
  Injective g
rw₅ :
  let g : (↑(hallMatchingsOn t ι') : Type (max u v)) → ↥ι' → ↥(ι'.biUnion t) :=
    fun (f : (↑(hallMatchingsOn t ι') : Type (max u v))) (i : ↥ι') ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ ι'.biUnion t) ((↑f : ↥ι' → α) i) ⋯;
  ∀ ⦃f f' : (↑(hallMatchingsOn t ι') : Type (max u v))⦄ (h : g f = g f'), f = f'
a :
  let g : (↑(hallMatchingsOn t ι') : Type (max u v)) → ↥ι' → ↥(ι'.biUnion t) :=
    fun (f : (↑(hallMatchingsOn t ι') : Type (max u v))) (i : ↥ι') ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ ι'.biUnion t) ((↑f : ↥ι' → α) i) ⋯;
  ∀ ⦃f f' : (↑(hallMatchingsOn t ι') : Type (max u v))⦄ (h : g f = g f') (a : ↥ι'), (↑f : ↥ι' → α) a = (↑f' : ↥ι' → α) a
a₁ :
  let g : (↑(hallMatchingsOn t ι') : Type (max u v)) → ↥ι' → ↥(ι'.biUnion t) :=
    fun (f : (↑(hallMatchingsOn t ι') : Type (max u v))) (i : ↥ι') ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ ι'.biUnion t) ((↑f : ↥ι' → α) i) ⋯;
  ∀ ⦃f f' : (↑(hallMatchingsOn t ι') : Type (max u v))⦄ (h : ∀ (x : ↥ι'), g f x = g f' x) (a : ↥ι'),
    (↑f : ↥ι' → α) a = (↑f' : ↥ι' → α) a
⊢ Finite (↑(hallMatchingsOn t ι') : Type (max u v))

Tactic:
classical
    rw [hallMatchingsOn]
    let g : hallMatchingsOn t ι' → ι' → ι'.biUnion t := by
      rintro f i
      refine ⟨f.val i, ?_⟩
      rw [mem_biUnion]
      exact ⟨i, i.property, f.property.2 i⟩
    apply Finite.of_injective g
    intro f f' h
    ext a
    rw [funext_iff] at h
    simpa [g] using h a

Premises used: hallMatchingsOn, funext_iff
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
mp : (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) → ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x
mpr : (∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
⊢ (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) ↔ ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
⊢ ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')

Tactic:
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Nonempty ((hallMatchingsFunctor t).obj ι') := fun ι' =>
      hallMatchingsOn.nonempty t h ι'.unop
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite
    (Functor.obj
      { obj := fun (ι' : (Finset ι)ᵒᵖ) ↦ (↑(hallMatchingsOn t (Opposite.unop ι')) : Type (max u v)),
        map := fun {x x_1 : (Finset ι)ᵒᵖ} (g : x ⟶ x_1) ↦ ↾hallMatchingsOn.restrict t ⋯, map_id := ⋯, map_comp := ⋯ }
      ι')

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
⊢ ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')

Tactic:
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') := by
        intro ι'
        rw [hallMatchingsFunctor]
        infer_instance
-- 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 ι')
mp :
  ∀ (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) (hu : u ∈ (hallMatchingsFunctor t).sections),
    ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (hallMatchingsFunctor t)

Premises used: hallMatchingsFunctor, nonempty_sections_of_finite_inverse_system
-- 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
⊢ ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
⟨?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
mp : ι → α
mp₁ :
  Injective.{u + 1, 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 ⋯)
mp₂ :
  ∀ (x : ι),
    Membership.mem (α := α) (t x)
      ((↑(u (Opposite.op {x})) : ↥(Opposite.unop (Opposite.op {x})) → α)
          (Subtype.mk (p := fun (x_1 : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {x})) x_1) x ⋯) :
        α)
⊢ ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
refine ⟨?_, ?_, ?_⟩
-- 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 (γ := Finset ι) (Opposite.unop (Opposite.op {i})) i

Tactic:
simp only [mem_singleton]

Premises used: Finset.mem_singleton