awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Configuration
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 P ≤ #(s.biUnion t) + (Fintype.card L - #s)
⊢ Fintype.card L ≤ #(s.biUnion t) + (Fintype.card L - #s)

Tactic:
replace := h.trans this
-- Module: Mathlib.Combinatorics.Configuration
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)
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : #s ≤ #(s.biUnion t)), #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

Premises used: add_tsub_assoc_of_le, le_tsub_iff_left, add_le_add_iff_right, Finset.card_le_univ, le_add_left
-- Module: Mathlib.Combinatorics.Configuration
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
neg : #(s.biUnion t)ᶜ ≤ #sᶜ
⊢ #s ≤ #(s.biUnion t)

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
-- Module: Mathlib.Combinatorics.Configuration
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

Tactic:
Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => ?_

Premises used: Iff.mpr, Finset.card_le_one_iff
-- Module: Mathlib.Combinatorics.Configuration
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
refine : ∀ (p₁ p₂ : P) (hp₁ : p₁ ∈ (s.biUnion t)ᶜ) (hp₂ : p₂ ∈ (s.biUnion t)ᶜ), p₁ = p₂
⊢ #(s.biUnion t)ᶜ ≤ 1

Tactic:
refine Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => ?_

Premises used: Iff.mpr, Finset.card_le_one_iff
-- Module: Mathlib.Combinatorics.Configuration
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)ᶜ
⊢ ∀ 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₂

Premises used: Classical.not_not, not_exists, Set.mem_setOf_eq, Finset.mem_compl, Set.mem_toFinset, not_and, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.Configuration
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
⊢ ∀ 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₂

Premises used: Classical.not_not, not_exists, Set.mem_setOf_eq, Finset.mem_compl, Set.mem_toFinset, not_and, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.Configuration
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
obtain : ∀ (l₁ l₂ : L) (hl₁ : l₁ ∈ s) (hl₂ : l₂ ∈ s) (hl₃ : l₁ ≠ l₂), p₁ = p₂
⊢ 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₁⟩)

Premises used: Iff.mpr, Finset.one_lt_card_iff, And.intro, Nat.one_lt_iff_ne_zero_and_ne_one, Iff.mp
-- Module: Mathlib.Combinatorics.Configuration
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
l₁ l₂ : L
hl₁ : l₁ ∈ s
hl₂ : l₂ ∈ s
hl₃ : l₁ ≠ l₂
⊢ p₁ = p₂

Tactic:
(eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃

Premises used: Configuration.Nondegenerate.eq_or_eq, Or.resolve_right
-- Module: Mathlib.Combinatorics.Configuration
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
l₁ l₂ : L
hl₁ : l₁ ∈ s
hl₂ : l₂ ∈ s
hl₃ : l₁ ≠ l₂
⊢ p₁ = p₂

Tactic:
exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃

Premises used: Configuration.Nondegenerate.eq_or_eq, Or.resolve_right
-- Module: Mathlib.Combinatorics.Configuration
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

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₃
-- Module: Mathlib.Combinatorics.Configuration
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ᶜ
neg : ∀ (hs₃ : ¬#sᶜ = 0), #(s.biUnion t)ᶜ ≤ #sᶜ
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ

Tactic:
by_cases hs₃ : #sᶜ = 0
-- Module: Mathlib.Combinatorics.Configuration
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
pos : #(s.biUnion t)ᶜ = 0
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ

Tactic:
rw [hs₃, Nat.le_zero]

Premises used: Nat.le_zero
-- Module: Mathlib.Combinatorics.Configuration
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
pos : ∀ (hs₃ : s = univ), s.biUnion t = univ
⊢ #(s.biUnion t)ᶜ = 0

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₃ ⊢

Premises used: Finset.card_eq_iff_eq_univ, Finset.card_compl, tsub_eq_zero_iff_le, eq_comm, LE.le.ge_iff_eq', Finset.card_le_univ
-- Module: Mathlib.Combinatorics.Configuration
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
pos : Finset.biUnion univ t = univ
⊢ s.biUnion t = univ

Tactic:
rw [hs₃]
-- Module: Mathlib.Combinatorics.Configuration
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
pos : ∀ (hs₃ : ∀ (x : L), x ∈ s) (x : P), x ∈ Finset.biUnion univ t
⊢ Finset.biUnion univ t = univ

Tactic:
rw [Finset.eq_univ_iff_forall] at hs₃ ⊢

Premises used: Finset.eq_univ_iff_forall
-- Module: Mathlib.Combinatorics.Configuration
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₃ : ∀ (x : L), x ∈ s
⊢ ∀ (x : P), x ∈ Finset.biUnion univ t

Tactic:
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⟩

Premises used: Iff.mpr, Finset.mem_univ, And.intro, Exists.intro, Set.mem_toFinset, Configuration.Nondegenerate.exists_line, Finset.mem_biUnion, Exists.elim
-- Module: Mathlib.Combinatorics.Configuration
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₃ : ∀ (x : L), x ∈ s
⊢ ∀ (x : P), x ∈ Finset.biUnion univ t

Tactic:
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⟩

Premises used: Iff.mpr, Finset.mem_univ, And.intro, Exists.intro, Set.mem_toFinset, Configuration.Nondegenerate.exists_line, Finset.mem_biUnion, Exists.elim
-- Module: Mathlib.Combinatorics.Configuration
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ᶜ

Tactic:
hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)

Premises used: Iff.mpr, Nat.one_le_iff_ne_zero, LE.le.trans
-- Module: Mathlib.Combinatorics.Configuration
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ᶜ

Tactic:
exact hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)

Premises used: Iff.mpr, Nat.one_le_iff_ne_zero, LE.le.trans
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Fintype P
inst_2 : Fintype L
simp : Fintype.card ((i : P) × { l : L // i ∈ l }) = Fintype.card ((i : L) × { p : P // p ∈ i })
⊢ Eq (α := ℕ) (∑ p : P, lineCount L p) (∑ l : L, pointCount P l)

Tactic:
simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]

Premises used: Configuration.lineCount, Fintype.card_sigma, Configuration.pointCount, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Fintype P
inst_2 : Fintype L
f : (i : P) × { l : L // i ∈ l } ≃ (i : L) × { p : P // p ∈ i }
⊢ Fintype.card ((i : P) × { l : L // i ∈ l }) = Fintype.card ((i : L) × { p : P // p ∈ i })

Tactic:
apply Fintype.card_congr

Premises used: Fintype.card_congr
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Fintype P
inst_2 : Fintype L
⊢ (i : P) × { l : L // i ∈ l } ≃ (i : L) × { p : P // p ∈ i }

Tactic:
calc
      (Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } :=
        (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
      _ ≃ { x : L × P // x.2 ∈ x.1 } := (Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl
      _ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (p : P) => p ∈ l

Premises used: Equiv.prodComm, Iff.rfl, Equiv.subtypeProdEquivSigmaSubtype, Membership.mem, Equiv.subtypeEquiv, Subtype, Equiv.symm, Sigma
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Fintype P
inst_2 : Fintype L
simp : Fintype.card ((i : P) × { l : L // i ∈ l }) = Fintype.card ((i : L) × { p : P // p ∈ i })
f : (i : P) × { l : L // i ∈ l } ≃ (i : L) × { p : P // p ∈ i }
⊢ Eq (α := ℕ) (∑ p : P, lineCount L p) (∑ l : L, pointCount P l)

Tactic:
classical
    simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]
    apply Fintype.card_congr
    calc
      (Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } :=
        (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
      _ ≃ { x : L × P // x.2 ∈ x.1 } := (Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl
      _ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (p : P) => p ∈ l

Premises used: Fintype.card_congr, Equiv.prodComm, Iff.rfl, Equiv.subtypeProdEquivSigmaSubtype, Configuration.lineCount, Membership.mem, Equiv.subtypeEquiv, Fintype.card_sigma, Subtype, Configuration.pointCount, Equiv.symm, Sigma, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
pos : ∀ (hf : Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }), pointCount P l ≤ lineCount L p
neg : ∀ (hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }), pointCount P l ≤ lineCount L p
⊢ pointCount P l ≤ lineCount L p

Tactic:
by_cases hf : Infinite { p : P // p ∈ l }

Premises used: Membership.mem, Subtype, Infinite
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
simp [pointCount]

Premises used: Configuration.pointCount
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
neg : ∀ (this : Fintype { p : P // p ∈ l }), pointCount P l ≤ lineCount L p
⊢ pointCount P l ≤ lineCount L p

Tactic:
haveI := fintypeOfNotInfinite hf
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
this : Fintype { p : P // p ∈ l }
neg : ∀ (val : Fintype { l : L // p ∈ l }), pointCount P l ≤ lineCount L p
⊢ pointCount P l ≤ lineCount L p

Tactic:
cases nonempty_fintype { l : L // p ∈ l }

Premises used: Membership.mem, Subtype, nonempty_fintype
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
this : Fintype { p : P // p ∈ l }
val : Fintype { l : L // p ∈ l }
neg : Fintype.card.{u_1} { p : P // p ∈ l } ≤ Fintype.card.{u_2} { l : L // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
rw [lineCount, pointCount, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]

Premises used: Configuration.lineCount, Configuration.pointCount, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
this : Fintype { p : P // p ∈ l }
val : Fintype { l : L // p ∈ l }
⊢ ∀ (p' : { p : P // p ∈ l }), p ≠ (↑p' : P)

Tactic:
have : ∀ p' : { p // p ∈ l }, p ≠ p' := fun p' hp' => h ((congr_arg (· ∈ l) hp').mpr p'.2)
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
this_1 : Fintype { p : P // p ∈ l }
val : Fintype { l : L // p ∈ l }
this : ∀ (p' : { p : P // p ∈ l }), p ≠ (↑p' : P)
⊢ Fintype.card.{u_1} { p : P // p ∈ l } ≤ Fintype.card.{u_2} { l : L // p ∈ l }

Tactic:
Fintype.card_le_of_injective (fun p' => ⟨mkLine (this p'), (mkLine_ax (this p')).1⟩)
      fun p₁ p₂ hp =>
      Subtype.ext ((eq_or_eq p₁.2 p₂.2 (mkLine_ax (this p₁)).2
            ((congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hp)).mpr (mkLine_ax (this p₂)).2)).resolve_right
          fun h' => (congr_arg (p ∉ ·) h').mp h (mkLine_ax (this p₁)).1)

Premises used: Fintype.card_le_of_injective, Eq.mpr, Configuration.Nondegenerate.eq_or_eq, Membership.mem, Eq.mp, Configuration.HasLines.mkLine_ax, Configuration.HasLines.mkLine, Subtype.ext_iff, Subtype.mk, congr_arg, And.right, And.left, Iff.mp, Or.resolve_right, Subtype.val, Not, Subtype.property, Subtype.ext
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
this_1 : Fintype { p : P // p ∈ l }
val : Fintype { l : L // p ∈ l }
this : ∀ (p' : { p : P // p ∈ l }), p ≠ (↑p' : P)
⊢ Fintype.card.{u_1} { p : P // p ∈ l } ≤ Fintype.card.{u_2} { l : L // p ∈ l }

Tactic:
exact
    Fintype.card_le_of_injective (fun p' => ⟨mkLine (this p'), (mkLine_ax (this p')).1⟩)
      fun p₁ p₂ hp =>
      Subtype.ext ((eq_or_eq p₁.2 p₂.2 (mkLine_ax (this p₁)).2
            ((congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hp)).mpr (mkLine_ax (this p₂)).2)).resolve_right
          fun h' => (congr_arg (p ∉ ·) h').mp h (mkLine_ax (this p₁)).1)

Premises used: Fintype.card_le_of_injective, Configuration.Nondegenerate.eq_or_eq, Membership.mem, Eq.mp, Configuration.HasLines.mkLine_ax, congr_arg, And.right, And.left, Or.resolve_right, Not, Subtype.property, Subtype.ext
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasPoints P L
p : P
l : L
h : p ∉ l
hf : Finite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
⊢ lineCount L p ≤ pointCount P l

Tactic:
@HasLines.pointCount_le_lineCount (Dual L) (Dual P) _ _ l p h hf

Premises used: Configuration.Dual, Configuration.lineCount, Configuration.HasLines.pointCount_le_lineCount, Configuration.pointCount
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
by_contra : ∀ (hc₂ : ¬Fintype.card P ≤ Fintype.card L), False
⊢ Fintype.card P ≤ Fintype.card L

Tactic:
by_contra hc₂
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
obtain : ∀ (f : L → P) (hf₁ : Function.Injective f) (hf₂ : ∀ (l : L), f l ∉ l), False
⊢ False

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_ge hc₂)

Premises used: Configuration.Nondegenerate.exists_injective_of_card_le, le_of_not_ge
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
rw :
  Eq (α := ℕ) (∑ l : L, lineCount L (f l))
    (∑ x : L, lineCount.{u_1, u_2} (P := P) L (({ toFun := f, inj' := hf₁ : L ↪ P } : (a : L) → P) x : P))
⊢ Eq (α := ℕ) (∑ l : L, lineCount L (f l)) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p)

Tactic:
rw [sum_map]

Premises used: Finset.sum_map
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ Eq (α := ℕ) (∑ l : L, lineCount L (f l))
    (∑ x : L, lineCount.{u_1, u_2} (P := P) L (({ toFun := f, inj' := hf₁ : L ↪ P } : (a : L) → P) x : P))

Tactic:
dsimp
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
obtain :
  ∀ (p : P) (hp : ¬∃ (a : L), f a = p),
    LT.lt (α := ℕ) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p) (∑ p : P, lineCount L p)
⊢ LT.lt (α := ℕ) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p) (∑ p : P, lineCount L p)

Tactic:
obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)

Premises used: mt, Iff.mp, Classical.not_forall, Fintype.card_le_of_surjective
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ (a : L), f a = p
⊢ LT.lt (α := ℕ) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p) (∑ p : P, lineCount L p)

Tactic:
sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le

Premises used: zero_le, Finset.mem_univ, Finset.sum_lt_sum_of_subset, Finset.subset_univ
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ (a : L), f a = p
refine_1 : p ∉ map { toFun := f, inj' := hf₁ : L ↪ P } univ
refine_2 : 0 < lineCount L p
⊢ LT.lt (α := ℕ) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p) (∑ p : P, lineCount L p)

Tactic:
refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le

Premises used: zero_le, Finset.mem_univ, Finset.sum_lt_sum_of_subset, Finset.subset_univ
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ (a : L), f a = p
⊢ p ∉ map { toFun := f, inj' := hf₁ : L ↪ P } univ

Tactic:
simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]

Premises used: Finset.mem_univ, exists_prop, Finset.mem_map, true_and