awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
⊢ (t x).Nonempty
have rw : 0 < #(t x)
Tactic: rw [← Finset.card_pos]
-- 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
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
⊢ #(Finset.biUnion {x} t) = #(t x)
have rw : #(t x) = #(t x)
Tactic: rw [Finset.singleton_biUnion]
-- 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
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
⊢ 0 < #(t x)
have _ : #(Finset.biUnion {x} t) = #(t x)
Tactic: calc
      0 < 1 := Nat.one_pos
      _ ≤ #(.biUnion {x} t) := ht {x}
      _ = (t x).card := by rw [Finset.singleton_biUnion]
-- 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 ι
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have tx_ne : (t x).Nonempty
Tactic: have tx_ne : (t x).Nonempty := by
    rw [← Finset.card_pos]
    calc
      0 < 1 := Nat.one_pos
      _ ≤ #(.biUnion {x} t) := ht {x}
      _ = (t x).card := by rw [Finset.singleton_biUnion]
-- 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
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
tx_ne : (t x).Nonempty
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have choose : ∀ (y : α) (hy : y ∈ t x), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: choose y hy using tx_ne
Cleared hypotheses: tx_ne
-- 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
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
⊢ Fintype.card ι - 1 = n
have rw : n + 1 - 1 = n
Tactic: rw [hn, Nat.add_succ_sub_one, add_zero]
-- 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
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
rw : n + 1 - 1 = n
⊢ Fintype.card ι - 1 = n
have rw₁ : n + 0 = n
Tactic: rw [hn, Nat.add_succ_sub_one, add_zero]
-- 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
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
rw : n + 1 - 1 = n
rw₁ : n + 0 = n
⊢ Fintype.card ι - 1 = n
have rw₂ : n = n
Tactic: rw [hn, Nat.add_succ_sub_one, add_zero]
-- 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
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have card_ι' : Fintype.card.{u} (↑ι' : Type u) = n
Tactic: have card_ι' : Fintype.card ι' = n :=
    calc
      Fintype.card ι' = Fintype.card ι - 1 := Set.card_ne_eq _
      _ = n := by rw [hn, Nat.add_succ_sub_one, add_zero]
-- 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
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 : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have rcases : ∀ (f' : (↑ι' : Type u) → α) (hfinj : Function.Injective f') (hfr : ∀ (x : (↑ι' : Type u)), f' x ∈ t' x),
  ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: rcases ih t' card_ι'.le (hall_cond_of_erase y ha) with ⟨f', hfinj, hfr⟩
-- 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
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
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have 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)
Tactic: refine ⟨fun z => if h : z = x then y else f' ⟨z, h⟩, ?_, ?_⟩
-- 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
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)
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have 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
Tactic: refine ⟨fun z => if h : z = x then y else f' ⟨z, h⟩, ?_, ?_⟩
-- 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₁ 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₂
have key : ∀ {x : (↑ι' : Type u)}, y ≠ f' x
Tactic: have key : ∀ {x}, y ≠ f' x := by
      intro x h
      simpa [t', ← h] using hfr x
-- 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
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
⊢ 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₂
have 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₂
Tactic: by_cases h₁ : z₁ = x
-- 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
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₂
⊢ 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₂
have 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₂
Tactic: by_cases h₁ : z₁ = x
-- 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
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
⊢ 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₂
have 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₂
Tactic: by_cases h₂ : z₂ = x
-- 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
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₂
⊢ 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₂
have 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₂
Tactic: by_cases h₂ : z₂ = x
-- 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
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
⊢ 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₂
have 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₂
Tactic: by_cases h₂ : z₂ = x
-- 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
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₂
⊢ 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₂
have 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₂
Tactic: by_cases h₂ : z₂ = x
-- 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
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 : ι
⊢ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h)) ∈ t z
have pos : ∀ (hz : z = x), y ∈ t z
Tactic: split_ifs with hz
-- 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
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
⊢ (if h : z = x then y else f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z h)) ∈ t z
have neg : ∀ (hz : ¬z = x), f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι') z hz) ∈ t z
Tactic: split_ifs with hz