awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' : ι | x' ≠ x}
t' : (↑ι' : Type u) → Finset α := fun (x' : (↑ι' : Type u)) ↦ (t (↑x' : ι)).erase y
card_ι' : Fintype.card.{u} (↑ι' : Type u) = n
f' : (↑ι' : Type u) → α
hfinj : Function.Injective f'
hfr : ∀ (x : (↑ι' : Type u)), f' x ∈ t' x
z : ι
hz : ¬z = x
⊢ f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz) ∈ t z
have hfr₁ : f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz) ∈ t' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz)
Tactic: specialize hfr ⟨z, hz⟩
Cleared hypotheses: hfr
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' : ι | x' ≠ x}
t' : (↑ι' : Type u) → Finset α := fun (x' : (↑ι' : Type u)) ↦ (t (↑x' : ι)).erase y
card_ι' : Fintype.card.{u} (↑ι' : Type u) = n
f' : (↑ι' : Type u) → α
hfinj : Function.Injective f'
z : ι
hz : ¬z = x
hfr : f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz) ∈ t' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz)
⊢ f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz) ∈ t z
have hfr₁ : f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz) ≠ y ∧
  f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz) ∈ t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz) : ι)
Tactic: rw [mem_erase] at hfr
Cleared hypotheses: hfr
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
have rw : card (α := ι) (image (fun (a : { x : ι // x ∈ (↑s : Set ι) }) ↦ (↑a : ι)) s') ≤
  card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
Tactic: rw [← card_image_of_injective s' Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
⊢ card (α := ι) (image (fun (a : { x : ι // x ∈ (↑s : Set ι) }) ↦ (↑a : ι)) s') ≤
    card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
have h : card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
  #(Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t)
Tactic: convert! ht (s'.image fun z => z.1) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
⊢ card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
    #(Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t)
have h : (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
  Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
⊢ (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
    Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t
have h : ∀ (y : α),
  Membership.mem (γ := Finset α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) y ↔
    y ∈ Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t
Tactic: ext y
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
have rw : card (α := ι) (image (fun (a : { x : ι // x ∈ (↑s : Set ι) }) ↦ (↑a : ι)) s') ≤
  card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
Tactic: classical
    rw [← card_image_of_injective s' Subtype.coe_injective]
    convert! ht (s'.image fun z => z.1) using 1
    apply congr_arg
    ext y
    simp
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
rw rw₁ rw₂ :
  card (α := ι) (image (fun (a : { x : ι // x ∈ (↑s : Set ι) }) ↦ (↑a : ι)) s') ≤
    card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
have h : card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
  #(Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t)
Tactic: classical
    rw [← card_image_of_injective s' Subtype.coe_injective]
    convert! ht (s'.image fun z => z.1) using 1
    apply congr_arg
    ext y
    simp
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
rw rw₁ rw₂ :
  card (α := ι) (image (fun (a : { x : ι // x ∈ (↑s : Set ι) }) ↦ (↑a : ι)) s') ≤
    card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
h :
  card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
    #(Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
have h₁ : (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
  Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t
Tactic: classical
    rw [← card_image_of_injective s' Subtype.coe_injective]
    convert! ht (s'.image fun z => z.1) using 1
    apply congr_arg
    ext y
    simp
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
rw rw₁ rw₂ :
  card (α := ι) (image (fun (a : { x : ι // x ∈ (↑s : Set ι) }) ↦ (↑a : ι)) s') ≤
    card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
h :
  card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
    #(Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t)
h₁ :
  (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
    Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))
have h₂ : ∀ (y : α),
  Membership.mem (γ := Finset α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) y ↔
    y ∈ Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t
Tactic: classical
    rw [← card_image_of_injective s' Subtype.coe_injective]
    convert! ht (s'.image fun z => z.1) using 1
    apply congr_arg
    ext y
    simp
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
have haveI : ∀ (this : DecidableEq ι),
  #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
Tactic: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
⊢ Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
have simp : ∀ ⦃a : ι⦄, a ∈ s → ∀ (x : a ∈ (↑s : Set ι)ᶜ), Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)ᶜ) a sorry ∉ s'
Tactic: simp only [disjoint_left, not_exists, mem_image, SetCoe.exists, exists_and_right,
      exists_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
have disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
Tactic: have disj : Disjoint s (s'.image fun z => z.1) := by
    simp only [disjoint_left, not_exists, mem_image, SetCoe.exists, exists_and_right,
      exists_eq_right]
    intro x hx hc _
    exact absurd hx hc
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
have this₁ : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
Tactic: have : #s' = #(s ∪ s'.image fun z => z.1) - #s := by
    simp [disj, card_image_of_injective _ Subtype.coe_injective, Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
have rw : #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #(s.biUnion t) ≤
  card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
Tactic: rw [this, hus]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
⊢ #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #(s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
have refine : #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t) - #(s.biUnion t) ≤
  card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
Tactic: refine (Nat.sub_le_sub_right (ht _) _).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
⊢ #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t) - #(s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
have rw : #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t \ s.biUnion t) ≤
  card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
Tactic: rw [← card_sdiff_of_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
rw :
  #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t \ s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
⊢ #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t) - #(s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
have rw₁ : s.biUnion t ⊆ (s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t
Tactic: rw [← card_sdiff_of_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
⊢ #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t \ s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
have a : (s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t \ s.biUnion t ⊆
  s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t_1 : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t_1)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t_1)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
t : α
⊢ t ∈ (s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t_1 \ s.biUnion t_1 →
    Membership.mem (γ := Finset α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t_1 (↑x' : ι) \ s.biUnion t_1) t
have a : ∀ (x : ι),
  (x ∈ s ∨ ∃ a ∈ s', (↑a : ι) = x) →
    t ∈ t_1 x → (∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)) → ∃ a ∈ s', t ∈ t_1 (↑a : ι) ∧ ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)
Tactic: simp only [mem_biUnion, mem_sdiff, not_exists, mem_image, and_imp, mem_union,
      exists_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
⊢ s.biUnion t ⊆ (s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t
have h : s ⊆ s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s'
Tactic: apply biUnion_subset_biUnion_of_subset_left
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have haveI : ∀ (this : DecidableEq ι), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have rw : ∀ (hn : Fintype.card ι = n.succ) (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t))
  (ih :
    ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
      Fintype.card ι' ≤ n →
        (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x)
  (s : Finset ι) (hs : s.Nonempty) (hns : s ≠ univ) (hus : #s = #(s.biUnion t)) (this : DecidableEq ι),
  ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: rw [Nat.add_one] at hn
Cleared hypotheses: hn, ht, ih, s, hs, hns, hus, this
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ Fintype.card.{u} ↥s ≤ n
have a : Fintype.card.{u} ↥s < n.succ
Tactic: apply Nat.le_of_lt_succ
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have card_ι'_le : Fintype.card.{u} ↥s ≤ n
Tactic: have card_ι'_le : Fintype.card s ≤ n := by
    apply Nat.le_of_lt_succ
    calc
      Fintype.card s = #s := Fintype.card_coe _
      _ < Fintype.card ι := (card_lt_iff_ne_univ _).mpr hns
      _ = n.succ := hn
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have rcases : ∀ (f' : ↥s → α) (hf' : Function.Injective f') (hsf' : ∀ (x : ↥s), f' x ∈ t' x),
  ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: rcases ih t' card_ι'_le (hall_cond_of_restrict ht) with ⟨f', hf', hsf'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
⊢ Fintype.card.{u} (↑ι'' : Type u) ≤ n
have simp_rw : Fintype.card.{u} ↥sᶜ < Fintype.card ι
Tactic: simp_rw [ι'', ← Nat.lt_succ_iff, ← hn, ← Finset.coe_compl, coe_sort_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
⊢ Fintype.card.{u} ↥sᶜ < Fintype.card ι
have rwa : #sᶜ < Fintype.card ι
Tactic: rwa [Fintype.card_coe, card_compl_lt_iff_nonempty]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
Tactic: have card_ι''_le : Fintype.card ι'' ≤ n := by
    simp_rw [ι'', ← Nat.lt_succ_iff, ← hn, ← Finset.coe_compl, coe_sort_coe]
    rwa [Fintype.card_coe, card_compl_lt_iff_nonempty]