awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
this : Fintype.card L ≤ #(s.biUnion t) + (Fintype.card L - #s)
⊢ #s ≤ #(s.biUnion t)
have rwa : ∀ (this : Fintype.card L ≤ #(s.biUnion t) + Fintype.card L - #s), #s ≤ #(s.biUnion t)
Tactic: rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
this : Fintype.card L ≤ #(s.biUnion t) + (Fintype.card L - #s)
rwa : ∀ (this : Fintype.card L ≤ #(s.biUnion t) + Fintype.card L - #s), #s ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)
have rwa₁ : ∀ (this : #s + Fintype.card L ≤ #(s.biUnion t) + Fintype.card L), #s ≤ #(s.biUnion t)
Tactic: rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
this : Fintype.card L ≤ #(s.biUnion t) + (Fintype.card L - #s)
rwa : ∀ (this : Fintype.card L ≤ #(s.biUnion t) + Fintype.card L - #s), #s ≤ #(s.biUnion t)
rwa₁ : ∀ (this : #s + Fintype.card L ≤ #(s.biUnion t) + Fintype.card L), #s ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)
have rwa₂ : ∀ (this : #s ≤ #(s.biUnion t)), #s ≤ #(s.biUnion t)
Tactic: rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
⊢ #s ≤ #(s.biUnion t)
have neg : #(s.biUnion t)ᶜ ≤ #sᶜ
Tactic: suffices #(s.biUnion t)ᶜ ≤ #sᶜ by
      -- Rephrase in terms of complements (uses `h`)
      rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
      replace := h.trans this
      rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
⊢ #(s.biUnion t)ᶜ ≤ 1
have refine : ∀ (p₁ p₂ : P) (hp₁ : p₁ ∈ (s.biUnion t)ᶜ) (hp₂ : p₂ ∈ (s.biUnion t)ᶜ), p₁ = p₂
Tactic: refine Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : p₁ ∈ (s.biUnion t)ᶜ
hp₂ : p₂ ∈ (s.biUnion t)ᶜ
⊢ p₁ = p₂
have hp₃ : ∀ x ∈ s, p₁ ∈ x
Tactic: simp_rw [t, Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and,
        Set.mem_toFinset, Set.mem_setOf_eq, Classical.not_not] at hp₁ hp₂
Cleared hypotheses: hp₁, hp₂
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : p₁ ∈ (s.biUnion t)ᶜ
hp₂ : p₂ ∈ (s.biUnion t)ᶜ
hp₃ : ∀ x ∈ s, p₁ ∈ x
⊢ p₁ = p₂
have hp₄ : ∀ x ∈ s, p₂ ∈ x
Tactic: simp_rw [t, Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and,
        Set.mem_toFinset, Set.mem_setOf_eq, Classical.not_not] at hp₁ hp₂
Cleared hypotheses: hp₁, hp₂
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : ∀ x ∈ s, p₁ ∈ x
hp₂ : ∀ x ∈ s, p₂ ∈ x
⊢ p₁ = p₂
have obtain : ∀ (l₁ l₂ : L) (hl₁ : l₁ ∈ s) (hl₂ : l₂ ∈ s) (hl₃ : l₁ ≠ l₂), p₁ = p₂
Tactic: obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ :=
        Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ
have hs₂ : #(s.biUnion t)ᶜ ≤ 1
Tactic: have hs₂ : #(s.biUnion t)ᶜ ≤ 1 := by
      -- At most one line through two points of `s`
      refine Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => ?_
      simp_rw [t, Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and,
        Set.mem_toFinset, Set.mem_setOf_eq, Classical.not_not] at hp₁ hp₂
      obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ :=
        Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
      exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ
have pos : ∀ (hs₃ : #sᶜ = 0), #(s.biUnion t)ᶜ ≤ #sᶜ
Tactic: by_cases hs₃ : #sᶜ = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
pos : ∀ (hs₃ : #sᶜ = 0), #(s.biUnion t)ᶜ ≤ #sᶜ
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ
have neg : ∀ (hs₃ : ¬#sᶜ = 0), #(s.biUnion t)ᶜ ≤ #sᶜ
Tactic: by_cases hs₃ : #sᶜ = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : #sᶜ = 0
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ
have pos : #(s.biUnion t)ᶜ = 0
Tactic: rw [hs₃, Nat.le_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : #sᶜ = 0
⊢ #(s.biUnion t)ᶜ = 0
have pos : ∀ (hs₃ : s = univ), s.biUnion t = univ
Tactic: rw [Finset.card_compl, tsub_eq_zero_iff_le, (Finset.card_le_univ _).ge_iff_eq', eq_comm,
        Finset.card_eq_iff_eq_univ] at hs₃ ⊢
Cleared hypotheses: hs₃
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : s = univ
⊢ s.biUnion t = univ
have pos : Finset.biUnion univ t = univ
Tactic: rw [hs₃]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : s = univ
⊢ Finset.biUnion univ t = univ
have pos : ∀ (hs₃ : ∀ (x : L), x ∈ s) (x : P), x ∈ Finset.biUnion univ t
Tactic: rw [Finset.eq_univ_iff_forall] at hs₃ ⊢
Cleared hypotheses: hs₃
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
let let₁ let₂ : ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
have let₃ : let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
∀ (s : Finset L), #s ≤ #(s.biUnion t)
Tactic: classical
    let t : L → Finset P := fun l => Set.toFinset { p | p ∉ l }
    suffices ∀ s : Finset L, #s ≤ (s.biUnion t).card by
      -- Hall's marriage theorem
      obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
      exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
    intro s
    by_cases hs₀ : #s = 0
    -- If `s = ∅`, then `#s = 0 ≤ #(s.bUnion t)`
    · simp_rw [hs₀, zero_le]
    by_cases hs₁ : #s = 1
    -- If `s = {l}`, then pick a point `p ∉ l`
    · obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
      obtain ⟨p, hl⟩ := exists_point (P := P) l
      rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
      exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)
    suffices #(s.biUnion t)ᶜ ≤ #sᶜ by
      -- Rephrase in terms of complements (uses `h`)
      rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
      replace := h.trans this
      rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this
    have hs₂ : #(s.biUnion t)ᶜ ≤ 1 := by
      -- At most one line through two points of `s`
      refine Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => ?_
      simp_rw [t, Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and,
        Set.mem_toFinset, Set.mem_setOf_eq, Classical.not_not] at hp₁ hp₂
      obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ :=
        Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
      exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃
    by_cases hs₃ : #sᶜ = 0
    · rw [hs₃, Nat.le_zero]
      rw [Finset.card_compl, tsub_eq_zero_iff_le, (Finset.card_le_univ _).ge_iff_eq', eq_comm,
        Finset.card_eq_iff_eq_univ] at hs₃ ⊢
      rw [hs₃]
      rw [Finset.eq_univ_iff_forall] at hs₃ ⊢
      exact fun p =>
        Exists.elim (exists_line p) -- If `s = univ`, then show `s.bUnion t = univ`
        fun l hl => Finset.mem_biUnion.mpr ⟨l, Finset.mem_univ l, Set.mem_toFinset.mpr hl⟩
    · exact hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
let let₁ let₂ : ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
let₃ let₄ :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L), #s ≤ #(s.biUnion t)
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
have pos : let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
∀ (s : Finset L) (hs₀ : #s = 0), #s ≤ #(s.biUnion t)
Tactic: classical
    let t : L → Finset P := fun l => Set.toFinset { p | p ∉ l }
    suffices ∀ s : Finset L, #s ≤ (s.biUnion t).card by
      -- Hall's marriage theorem
      obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
      exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
    intro s
    by_cases hs₀ : #s = 0
    -- If `s = ∅`, then `#s = 0 ≤ #(s.bUnion t)`
    · simp_rw [hs₀, zero_le]
    by_cases hs₁ : #s = 1
    -- If `s = {l}`, then pick a point `p ∉ l`
    · obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
      obtain ⟨p, hl⟩ := exists_point (P := P) l
      rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
      exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)
    suffices #(s.biUnion t)ᶜ ≤ #sᶜ by
      -- Rephrase in terms of complements (uses `h`)
      rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
      replace := h.trans this
      rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this
    have hs₂ : #(s.biUnion t)ᶜ ≤ 1 := by
      -- At most one line through two points of `s`
      refine Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => ?_
      simp_rw [t, Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and,
        Set.mem_toFinset, Set.mem_setOf_eq, Classical.not_not] at hp₁ hp₂
      obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ :=
        Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
      exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃
    by_cases hs₃ : #sᶜ = 0
    · rw [hs₃, Nat.le_zero]
      rw [Finset.card_compl, tsub_eq_zero_iff_le, (Finset.card_le_univ _).ge_iff_eq', eq_comm,
        Finset.card_eq_iff_eq_univ] at hs₃ ⊢
      rw [hs₃]
      rw [Finset.eq_univ_iff_forall] at hs₃ ⊢
      exact fun p =>
        Exists.elim (exists_line p) -- If `s = univ`, then show `s.bUnion t = univ`
        fun l hl => Finset.mem_biUnion.mpr ⟨l, Finset.mem_univ l, Set.mem_toFinset.mpr hl⟩
    · exact hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
let let₁ let₂ : ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
let₃ let₄ :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L), #s ≤ #(s.biUnion t)
pos :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L) (hs₀ : #s = 0), #s ≤ #(s.biUnion t)
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
have neg : let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
∀ (s : Finset L) (hs₀ : ¬#s = 0), #s ≤ #(s.biUnion t)
Tactic: classical
    let t : L → Finset P := fun l => Set.toFinset { p | p ∉ l }
    suffices ∀ s : Finset L, #s ≤ (s.biUnion t).card by
      -- Hall's marriage theorem
      obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
      exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
    intro s
    by_cases hs₀ : #s = 0
    -- If `s = ∅`, then `#s = 0 ≤ #(s.bUnion t)`
    · simp_rw [hs₀, zero_le]
    by_cases hs₁ : #s = 1
    -- If `s = {l}`, then pick a point `p ∉ l`
    · obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
      obtain ⟨p, hl⟩ := exists_point (P := P) l
      rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
      exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)
    suffices #(s.biUnion t)ᶜ ≤ #sᶜ by
      -- Rephrase in terms of complements (uses `h`)
      rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
      replace := h.trans this
      rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this
    have hs₂ : #(s.biUnion t)ᶜ ≤ 1 := by
      -- At most one line through two points of `s`
      refine Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => ?_
      simp_rw [t, Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and,
        Set.mem_toFinset, Set.mem_setOf_eq, Classical.not_not] at hp₁ hp₂
      obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ :=
        Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
      exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃
    by_cases hs₃ : #sᶜ = 0
    · rw [hs₃, Nat.le_zero]
      rw [Finset.card_compl, tsub_eq_zero_iff_le, (Finset.card_le_univ _).ge_iff_eq', eq_comm,
        Finset.card_eq_iff_eq_univ] at hs₃ ⊢
      rw [hs₃]
      rw [Finset.eq_univ_iff_forall] at hs₃ ⊢
      exact fun p =>
        Exists.elim (exists_line p) -- If `s = univ`, then show `s.bUnion t = univ`
        fun l hl => Finset.mem_biUnion.mpr ⟨l, Finset.mem_univ l, Set.mem_toFinset.mpr hl⟩
    · exact hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
let let₁ let₂ : ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
let₃ let₄ :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L), #s ≤ #(s.biUnion t)
pos :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L) (hs₀ : #s = 0), #s ≤ #(s.biUnion t)
neg neg₁ :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L) (hs₀ : ¬#s = 0), #s ≤ #(s.biUnion t)
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
have pos₁ : let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
∀ (s : Finset L) (hs₀ : ¬#s = 0) (hs₁ : #s = 1), #s ≤ #(s.biUnion t)
Tactic: classical
    let t : L → Finset P := fun l => Set.toFinset { p | p ∉ l }
    suffices ∀ s : Finset L, #s ≤ (s.biUnion t).card by
      -- Hall's marriage theorem
      obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
      exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
    intro s
    by_cases hs₀ : #s = 0
    -- If `s = ∅`, then `#s = 0 ≤ #(s.bUnion t)`
    · simp_rw [hs₀, zero_le]
    by_cases hs₁ : #s = 1
    -- If `s = {l}`, then pick a point `p ∉ l`
    · obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
      obtain ⟨p, hl⟩ := exists_point (P := P) l
      rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
      exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)
    suffices #(s.biUnion t)ᶜ ≤ #sᶜ by
      -- Rephrase in terms of complements (uses `h`)
      rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
      replace := h.trans this
      rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this
    have hs₂ : #(s.biUnion t)ᶜ ≤ 1 := by
      -- At most one line through two points of `s`
      refine Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => ?_
      simp_rw [t, Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and,
        Set.mem_toFinset, Set.mem_setOf_eq, Classical.not_not] at hp₁ hp₂
      obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ :=
        Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
      exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃
    by_cases hs₃ : #sᶜ = 0
    · rw [hs₃, Nat.le_zero]
      rw [Finset.card_compl, tsub_eq_zero_iff_le, (Finset.card_le_univ _).ge_iff_eq', eq_comm,
        Finset.card_eq_iff_eq_univ] at hs₃ ⊢
      rw [hs₃]
      rw [Finset.eq_univ_iff_forall] at hs₃ ⊢
      exact fun p =>
        Exists.elim (exists_line p) -- If `s = univ`, then show `s.bUnion t = univ`
        fun l hl => Finset.mem_biUnion.mpr ⟨l, Finset.mem_univ l, Set.mem_toFinset.mpr hl⟩
    · exact hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
let let₁ let₂ : ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
let₃ let₄ :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L), #s ≤ #(s.biUnion t)
pos :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L) (hs₀ : #s = 0), #s ≤ #(s.biUnion t)
neg neg₁ :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L) (hs₀ : ¬#s = 0), #s ≤ #(s.biUnion t)
pos₁ :
  let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
  ∀ (s : Finset L) (hs₀ : ¬#s = 0) (hs₁ : #s = 1), #s ≤ #(s.biUnion t)
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
have neg₂ : let t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l};
∀ (s : Finset L) (hs₀ : ¬#s = 0) (hs₁ : ¬#s = 1), #s ≤ #(s.biUnion t)
Tactic: classical
    let t : L → Finset P := fun l => Set.toFinset { p | p ∉ l }
    suffices ∀ s : Finset L, #s ≤ (s.biUnion t).card by
      -- Hall's marriage theorem
      obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
      exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
    intro s
    by_cases hs₀ : #s = 0
    -- If `s = ∅`, then `#s = 0 ≤ #(s.bUnion t)`
    · simp_rw [hs₀, zero_le]
    by_cases hs₁ : #s = 1
    -- If `s = {l}`, then pick a point `p ∉ l`
    · obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
      obtain ⟨p, hl⟩ := exists_point (P := P) l
      rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
      exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)
    suffices #(s.biUnion t)ᶜ ≤ #sᶜ by
      -- Rephrase in terms of complements (uses `h`)
      rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
      replace := h.trans this
      rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this
    have hs₂ : #(s.biUnion t)ᶜ ≤ 1 := by
      -- At most one line through two points of `s`
      refine Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => ?_
      simp_rw [t, Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and,
        Set.mem_toFinset, Set.mem_setOf_eq, Classical.not_not] at hp₁ hp₂
      obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ :=
        Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
      exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃
    by_cases hs₃ : #sᶜ = 0
    · rw [hs₃, Nat.le_zero]
      rw [Finset.card_compl, tsub_eq_zero_iff_le, (Finset.card_le_univ _).ge_iff_eq', eq_comm,
        Finset.card_eq_iff_eq_univ] at hs₃ ⊢
      rw [hs₃]
      rw [Finset.eq_univ_iff_forall] at hs₃ ⊢
      exact fun p =>
        Exists.elim (exists_line p) -- If `s = univ`, then show `s.bUnion t = univ`
        fun l hl => Finset.mem_biUnion.mpr ⟨l, Finset.mem_univ l, Set.mem_toFinset.mpr hl⟩
    · exact hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Fintype P
inst_2 : Fintype L
⊢ Eq (α := ℕ) (∑ p : P, lineCount L p) (∑ l : L, pointCount P l)
have simp : Fintype.card ((i : P) × { l : L // i ∈ l }) = Fintype.card ((i : L) × { p : P // p ∈ i })
Tactic: simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Fintype P
inst_2 : Fintype L
⊢ Fintype.card ((i : P) × { l : L // i ∈ l }) = Fintype.card ((i : L) × { p : P // p ∈ i })
have f : (i : P) × { l : L // i ∈ l } ≃ (i : L) × { p : P // p ∈ i }
Tactic: apply Fintype.card_congr