awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
M : Type u_5
κ : Type u_6
inst : AddCommMonoid M
S : Finset M
inst_1 : Finite κ
C : M → κ
obtain :
  ∀ (ι : Type) (_inst : Fintype ι) (hι : ∀ (C : (ι → ↥S) → κ), ∃ (l : Line (↥S) ι), Line.IsMono C l),
    ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
obtain₁ :
  ∀ (ι : Type) (_inst : Fintype ι)
    (hι : ∃ (l : Line (↥S) ι), Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ) (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) l),
    ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
obtain₂ :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
    (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
    ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
obtain₃ :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
    (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
    let s : Finset ι := {i : ι | l.idxFun i = none};
    ∀ (hs : s = {i : ι | l.idxFun i = none}), ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
refine_1 :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
    (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
    let s : Finset ι := {i : ι | l.idxFun i = none};
    ∀ (hs : s = {i : ι | l.idxFun i = none}), ⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none) ∈ s
refine_2 :
  (ι : Type) →
    (_inst : Fintype ι) →
      (l : Line (↥S) ι) →
        (c : κ) →
          (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c) →
            let s : Finset ι := {i : ι | l.idxFun i = none};
            (hs : s = {i : ι | l.idxFun i = none}) → (i : ι) → ↥S → M
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have refine_3 : ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
  (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
  let s : Finset ι := {i : ι | l.idxFun i = none};
  ∀ (hs : s = {i : ι | l.idxFun i = none}),
    ∀ s_1 ∈ S, C (#s • s_1 + ∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0) = c
Tactic: classical
  obtain ⟨ι, _inst, hι⟩ := Line.exists_mono_in_high_dimension S κ
  specialize hι fun v => C <| ∑ i, v i
  obtain ⟨l, c, hl⟩ := hι
  set s : Finset ι := {i | l.idxFun i = none} with hs
  refine ⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0,
    c, ?_⟩
  · rw [hs, Finset.mem_filter]
    exact ⟨Finset.mem_univ _, l.proper.choose_spec⟩
  · exact fun m => m
  intro x xs
  rw [← hl ⟨x, xs⟩]
  clear hl; congr
  rw [← Finset.sum_add_sum_compl s]
  congr 1
  · rw [← Finset.sum_const]
    apply Finset.sum_congr rfl
    intro i hi
    rw [hs, Finset.mem_filter] at hi
    rw [l.apply_none _ _ hi.right, Subtype.coe_mk]
  · apply Finset.sum_congr rfl
    intro i hi
    rw [hs, Finset.compl_filter, Finset.mem_filter] at hi
    obtain ⟨y, hy⟩ := Option.ne_none_iff_exists.mp hi.right
    simp [← hy, Option.map_some, Option.getD]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
have intro : ∀ (val : Fintype η), ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
Tactic: cases nonempty_fintype η
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
have intro : ∀ (ι : Type) (w : Fintype ι)
  (hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l),
  ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
Tactic: obtain ⟨ι, _, hι⟩ := Line.exists_mono_in_high_dimension (Shrink.{0} η → α) κ
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
have intro : ∀ (C : (ι × Shrink.{0, u_7} η → α) → κ), ∃ (l : Subspace η α (ι × Shrink.{0, u_7} η)), IsMono C l
Tactic: refine ⟨ι × Shrink η, inferInstance, fun C ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 : Subspace η α (ι × Shrink.{0, u_7} η)), IsMono C l
have intro : ∀ (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),
  ∃ (l : Subspace η α (ι × Shrink.{0, u_7} η)), IsMono C l
Tactic: obtain ⟨l, hl⟩ := hι fun x ↦ C fun (i, e) ↦ x i e
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ ∃ (l : Subspace η α (ι × Shrink.{0, u_7} η)), IsMono C l
have intro : IsMono C (l.toSubspace.reindex (Equiv.symm (equivShrink η)) (Equiv.refl α) (Equiv.refl (ι × Shrink.{0, u_7} η)))
Tactic: refine ⟨l.toSubspace.reindex (equivShrink.{0} η).symm (Equiv.refl _) (Equiv.refl _), ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ IsMono C (l.toSubspace.reindex (Equiv.symm (equivShrink η)) (Equiv.refl α) (Equiv.refl (ι × Shrink.{0, u_7} η)))
have 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} η)
Tactic: convert! hl.toSubspace.reindex
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
⊢ ∃ (n : ℕ), ∀ (C : (Fin n → α) → κ), ∃ (l : Subspace η α (Fin n)), IsMono C l
have obtain : ∀ (ι : Type) (ιfin : Fintype ι) (hι : ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l),
  ∃ (n : ℕ), ∀ (C : (Fin n → α) → κ), ∃ (l : Subspace η α (Fin n)), IsMono C l
Tactic: obtain ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension α κ η
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
have refine : ∀ (C : (Fin (Fintype.card ι) → α) → κ), ∃ (l : Subspace η α (Fin (Fintype.card ι))), IsMono C l
Tactic: refine ⟨Fintype.card ι, fun C ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 η α (Fin (Fintype.card ι))), IsMono C l
have 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
Tactic: obtain ⟨l, c, cl⟩ := hι fun v ↦ C (v ∘ (Fintype.equivFin _).symm)
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
have refine : ∀ (e : η),
  ∃ (i : Fin (Fintype.card ι)),
    (l.idxFun ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)) i = Sum.inr e
Tactic: refine ⟨⟨l.idxFun ∘ (Fintype.equivFin _).symm, fun e ↦ ?_⟩, c, cl⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 : Fin (Fintype.card ι)),
    (l.idxFun ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)) i = Sum.inr e
have 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
Tactic: obtain ⟨i, hi⟩ := l.proper e
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ ∃ (i : Fin (Fintype.card ι)),
    (l.idxFun ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)) i = Sum.inr e
have 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
Tactic: use Fintype.equivFin _ i
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : (↑(hallMatchingsOn t ι'') : Type (max u v))
⊢ (↑(hallMatchingsOn t ι') : Type (max u v))
have refine : (fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) sorry)) ∈ hallMatchingsOn t ι'
Tactic: refine ⟨fun i => f.val ⟨i, h i.property⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (hypothesis)
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : (↑(hallMatchingsOn t ι'') : Type (max u v))
⊢ (fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) ⋯)) ∈ hallMatchingsOn t ι'
have hinj : Injective (↑f : ↥ι'' → α)
Tactic: obtain ⟨hinj, hc⟩ := f.property
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (hypothesis)
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : (↑(hallMatchingsOn t ι'') : Type (max u v))
hinj : Injective (↑f : ↥ι'' → α)
⊢ (fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) ⋯)) ∈ hallMatchingsOn t ι'
have hc : ∀ (x : ↥ι''), (↑f : ↥ι'' → α) x ∈ t (↑x : ι)
Tactic: obtain ⟨hinj, hc⟩ := f.property
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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 ι'
have refine : Injective.{u + 1, v + 1} (β := α) fun (i : ↥ι') ↦ (↑f : ↥ι'' → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') (↑i : ι) sorry)
Tactic: refine ⟨?_, fun i => hc ⟨i, h i.property⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
⊢ Nonempty (↑(hallMatchingsOn t ι') : Type (max u v))
have refine : ∃ (x : ↥ι' → α), x ∈ hallMatchingsOn t ι'
Tactic: refine ⟨Classical.indefiniteDescription _ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
⊢ ∃ (x : ↥ι' → α), x ∈ hallMatchingsOn t ι'
have apply : ∀ (s : Finset ↥ι'), #s ≤ card.{v} (α := α) (s.biUnion fun (i : ↥ι') ↦ t (↑i : ι))
Tactic: apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι))
have h₁ : #s' = #(image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s')
Tactic: convert! h (s'.image (↑)) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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')
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι))
have h₂ : card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι)) =
  #((image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s').biUnion t)
Tactic: convert! h (s'.image (↑)) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
⊢ card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι)) =
    #((image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s').biUnion t)
have h₁ : card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι)) = card.{v} (α := α) (s'.biUnion fun (a : ↥ι') ↦ t (↑a : ι))
Tactic: rw [image_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
⊢ Nonempty (↑(hallMatchingsOn t ι') : Type (max u v))
have refine : ∃ (x : ↥ι' → α), x ∈ hallMatchingsOn t ι'
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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))
have refine₁ : ∀ (s : Finset ↥ι'), #s ≤ card.{v} (α := α) (s.biUnion fun (i : ↥ι') ↦ t (↑i : ι))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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 : ι))
⊢ Nonempty (↑(hallMatchingsOn t ι') : Type (max u v))
have h₁ : ∀ (s' : Finset ↥ι'), #s' = #(image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s')
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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')
⊢ Nonempty (↑(hallMatchingsOn t ι') : Type (max u v))
have h₂ : ∀ (s' : Finset ↥ι'),
  card.{v} (α := α) (s'.biUnion fun (i : ↥ι') ↦ t (↑i : ι)) =
    #((image (Subtype.val (p := fun (x : ι) ↦ x ∈ ι')) s').biUnion t)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : (↑(hallMatchingsOn t ι') : Type (max u v))
i : ↥ι'
⊢ ↥(ι'.biUnion t)
have refine : (↑f : ↥ι' → α) i ∈ ι'.biUnion t
Tactic: refine ⟨f.val i, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : (↑(hallMatchingsOn t ι') : Type (max u v))
i : ↥ι'
⊢ (↑f : ↥ι' → α) i ∈ ι'.biUnion t
have rw : ∃ a ∈ ι', (↑f : ↥ι' → α) i ∈ t a
Tactic: rw [mem_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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) ⋯
⊢ Finite (↑{f : ↥ι' → α | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t (↑x : ι)} : Type (max u v))
have apply : Injective g
Tactic: apply Finite.of_injective g
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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'
⊢ f = f'
have a : ∀ (a : ↥ι'), (↑f : ↥ι' → α) a = (↑f' : ↥ι' → α) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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 : ↥ι'
⊢ (↑f : ↥ι' → α) a = (↑f' : ↥ι' → α) a
have a₁ : ∀ (h : ∀ (x : ↥ι'), g f x = g f' x) (a : ↥ι'), (↑f : ↥ι' → α) a = (↑f' : ↥ι' → α) a
Tactic: rw [funext_iff] at h
Cleared hypotheses: h, a
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite (↑(hallMatchingsOn t ι') : Type (max u v))
have rw : Finite (↑{f : ↥ι' → α | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t (↑x : ι)} : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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))
⊢ Finite (↑(hallMatchingsOn t ι') : Type (max u v))
have 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) sorry;
Injective g
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
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
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
⊢ Finite (↑(hallMatchingsOn t ι') : Type (max u v))
have 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) sorry;
∀ ⦃f f' : (↑(hallMatchingsOn t ι') : Type (max u v))⦄ (h : g f = g f'), f = f'
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