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 + 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
refine_1 :
  Function.Injective.{u + 1, v + 1} (β := α) fun (z : ι) ↦
    if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h)
refine_2 :
  ∀ (x_1 : ι),
    (fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) x_1 ∈ t x_1
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
refine ⟨fun z => if h : z = x then y else f' ⟨z, h⟩, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x_1
ι' : Set ι := {x' : ι | x' ≠ x_1}
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₁ z₂ : ι
x : (↑ι' : Type u)
h : y = f' x
⊢ False

Tactic:
simpa [t', ← h] using hfr x
-- Module: Mathlib.Combinatorics.Hall.Finite
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₁ z₂ : ι
⊢ ∀ {x : (↑ι' : Type u)}, y ≠ f' x

Tactic:
have key : ∀ {x}, y ≠ f' x := by
      intro x h
      simpa [t', ← h] using hfr x
-- Module: Mathlib.Combinatorics.Hall.Finite
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₁ z₂ : ι
key : ∀ {x : (↑ι' : Type u)}, y ≠ f' x
pos :
  ∀ (h₁ : z₁ = x),
    Eq.{v + 1} (α := α)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
      z₁ = z₂
neg :
  ∀ (h₁ : ¬z₁ = x),
    Eq.{v + 1} (α := α)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
      z₁ = z₂
⊢ Eq.{v + 1} (α := α)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
    z₁ = z₂

Tactic:
by_cases h₁ : z₁ = x
-- Module: Mathlib.Combinatorics.Hall.Finite
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₁ z₂ : ι
key : ∀ {x : (↑ι' : Type u)}, y ≠ f' x
h₁ : z₁ = x
pos :
  ∀ (h₂ : z₂ = x),
    Eq.{v + 1} (α := α)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
      z₁ = z₂
neg :
  ∀ (h₂ : ¬z₂ = x),
    Eq.{v + 1} (α := α)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
      z₁ = z₂
⊢ Eq.{v + 1} (α := α)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
    z₁ = z₂

Tactic:
by_cases h₂ : z₂ = x
-- Module: Mathlib.Combinatorics.Hall.Finite
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₁ z₂ : ι
key : ∀ {x : (↑ι' : Type u)}, y ≠ f' x
h₁ : ¬z₁ = x
pos :
  ∀ (h₂ : z₂ = x),
    Eq.{v + 1} (α := α)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
      z₁ = z₂
neg :
  ∀ (h₂ : ¬z₂ = x),
    Eq.{v + 1} (α := α)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
        ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
      z₁ = z₂
⊢ Eq.{v + 1} (α := α)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
    z₁ = z₂

Tactic:
by_cases h₂ : z₂ = x
-- Module: Mathlib.Combinatorics.Hall.Finite
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₁ z₂ : ι
key : ∀ {x : (↑ι' : Type u)}, y ≠ f' x
h₁ : z₁ = x
h₂ : z₂ = x
⊢ Eq.{v + 1} (α := α)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
    z₁ = z₂

Tactic:
simp [h₁, h₂, hfinj.eq_iff, key, key.symm]

Premises used: Function.Injective.eq_iff, Ne.symm
-- Module: Mathlib.Combinatorics.Hall.Finite
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₁ z₂ : ι
key : ∀ {x : (↑ι' : Type u)}, y ≠ f' x
h₁ : z₁ = x
h₂ : ¬z₂ = x
⊢ Eq.{v + 1} (α := α)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
    z₁ = z₂

Tactic:
simp [h₁, h₂, hfinj.eq_iff, key, key.symm]

Premises used: Function.Injective.eq_iff, Ne.symm
-- Module: Mathlib.Combinatorics.Hall.Finite
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₁ z₂ : ι
key : ∀ {x : (↑ι' : Type u)}, y ≠ f' x
h₁ : ¬z₁ = x
h₂ : z₂ = x
⊢ Eq.{v + 1} (α := α)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
    z₁ = z₂

Tactic:
simp [h₁, h₂, hfinj.eq_iff, key, key.symm]

Premises used: Function.Injective.eq_iff, Ne.symm
-- Module: Mathlib.Combinatorics.Hall.Finite
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₁ z₂ : ι
key : ∀ {x : (↑ι' : Type u)}, y ≠ f' x
h₁ : ¬z₁ = x
h₂ : ¬z₂ = x
⊢ Eq.{v + 1} (α := α)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₁)
      ((fun (z : ι) ↦ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h) : α)) z₂) →
    z₁ = z₂

Tactic:
simp [h₁, h₂, hfinj.eq_iff, key, key.symm]

Premises used: Function.Injective.eq_iff, Ne.symm
-- Module: Mathlib.Combinatorics.Hall.Finite
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 : ι
pos : ∀ (hz : z = x), y ∈ t z
neg : ∀ (hz : ¬z = x), f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz) ∈ t z
⊢ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h)) ∈ t z

Tactic:
split_ifs with hz
-- Module: Mathlib.Combinatorics.Hall.Finite
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
pos pos₁ pos₂ pos₃ : y ∈ t x
⊢ y ∈ t z

Tactic:
rwa [hz]
-- Module: Mathlib.Combinatorics.Hall.Finite
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' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz)

Tactic:
specialize hfr ⟨z, hz⟩

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 + 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) ≠ 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

Premises used: Finset.mem_erase
-- Module: Mathlib.Combinatorics.Hall.Finite
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) ≠ y ∧
    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

Tactic:
hfr.2

Premises used: Set.Mem, setOf, And.right
-- Module: Mathlib.Combinatorics.Hall.Finite
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) ≠ y ∧
    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

Tactic:
exact hfr.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Hall.Finite
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 :
  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' : ι))

Tactic:
rw [← card_image_of_injective s' Subtype.coe_injective]

Premises used: Finset.card_image_of_injective, Subtype.coe_injective
-- Module: Mathlib.Combinatorics.Hall.Finite
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 (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') ≤
    #(Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t)

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

Premises used: Finset.image
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
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)
⊢ card (α := ι) (image (fun (a : { x : ι // x ∈ (↑s : Set ι) }) ↦ (↑a : ι)) s') ≤
    card.{v} (α := α) (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι))

Tactic:
convert! ht (s'.image fun z => z.1) using 1

Premises used: Finset.image
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
h :
  (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
    Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t
⊢ 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:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
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
⊢ (s'.biUnion fun (a' : (↑(↑s : Set ι) : Type u)) ↦ t (↑a' : ι)) =
    Finset.biUnion (image (fun (z : (↑(↑s : Set ι) : Type u)) ↦ (↑z : ι)) s') t

Tactic:
ext y
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι) : Type u)
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:
simp
-- Module: Mathlib.Combinatorics.Hall.Finite
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
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
⊢ #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

Premises used: congr_arg