awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
⊢ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∈ t'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')

Tactic:
have h := hsf'' ⟨x'', hx''⟩
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
h : f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∈ t'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
⊢ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∈ t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') : ι) ∧
    f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t

Tactic:
rw [mem_sdiff] at h

Premises used: Finset.mem_sdiff
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
h :
  f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∈ t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') : ι) ∧
    f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
⊢ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
h :
  f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∈ t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') : ι) ∧
    f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
⊢ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
⊢ ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t

Tactic:
have f''_notMem_biUnion : ∀ (x'') (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t := by
    intro x'' hx''
    have h := hsf'' ⟨x'', hx''⟩
    rw [mem_sdiff] at h
    exact h.2
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
⊢ ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')

Tactic:
grind
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
⊢ ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')

Tactic:
have im_disj :
      ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s), f' ⟨x', hx'⟩ ≠ f'' ⟨x'', hx''⟩ := by
    grind
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
⟨fun x => if h : x ∈ s then f' ⟨x, h⟩ else f'' ⟨x, h⟩, ?_, ?_⟩

Premises used: Membership.mem, dite, Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
refine_1 :
  Function.Injective.{u + 1, v + 1} (β := α) fun (x : ι) ↦
    if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
    else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h)
refine_2 :
  ∀ (x : ι),
    (fun (x : ι) ↦
          (if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
            else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h) :
            α))
        x ∈
      t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
refine ⟨fun x => if h : x ∈ s then f' ⟨x, h⟩ else f'' ⟨x, h⟩, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
⊢ Function.Injective.{u + 1, v + 1} (β := α) fun (x : ι) ↦
    if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
    else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h)

Tactic:
hf'.dite _ hf'' (@fun x x' => im_disj x x' _ _)

Premises used: Set.Mem, setOf, Function.Injective.dite, Not
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
⊢ Function.Injective.{u + 1, v + 1} (β := α) fun (x : ι) ↦
    if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
    else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h)

Tactic:
refine hf'.dite _ hf'' (@fun x x' => im_disj x x' _ _)

Premises used: Function.Injective.dite
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
x : ι
pos : ∀ (h : x ∈ s), f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h) ∈ t x
neg : ∀ (h : x ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h) ∈ t x
⊢ (if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
    else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h)) ∈
    t x

Tactic:
split_ifs with h
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
x : ι
h : x ∈ s
⊢ f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h) ∈ t x

Tactic:
hsf' ⟨x, h⟩

Premises used: Set.Mem, setOf, Subtype.mk
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
x : ι
h : x ∈ s
⊢ f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h) ∈ t x

Tactic:
exact hsf' ⟨x, h⟩

Premises used: Subtype.mk
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
x : ι
h : x ∉ s
⊢ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h) ∈ t x

Tactic:
sdiff_subset (hsf'' ⟨x, h⟩)

Premises used: Subtype.mk, Finset.sdiff_subset
-- Module: Mathlib.Combinatorics.Hall.Finite
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
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
x : ι
h : x ∉ s
⊢ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h) ∈ t x

Tactic:
exact sdiff_subset (hsf'' ⟨x, h⟩)

Premises used: Subtype.mk, Finset.sdiff_subset
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
intro : ∀ (val : Fintype ι), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
intro : ∀ (m : ℕ) (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
generalize hn : Fintype.card ι = m

Premises used: Fintype.card
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
hn : Fintype.card ι = n
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
_
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
m : ℕ
hn : Fintype.card ι = m
intro :
  ∀ (n : ℕ)
    (ih :
      ∀ m < n,
        ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
          (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x)
    {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
    (hn : Fintype.card ι = n), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
induction m using Nat.strongRecOn generalizing ι with | ind n ih => _