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 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)

Tactic:
have step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 := by
      rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]
      on_goal 1 =>
        rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
        · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
          simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
          change pointCount P l • _ = lineCount L (f l) • _
          rw [hf2]
      all_goals simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]; exact fun p => Iff.rfl
-- 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
rwa :
  ∀ (step1 : HAdd.hAdd (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ sᶜ, lineCount L i.1) = ∑ i : P × L, pointCount P i.2)
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
rwa₁ :
  ∀
    (step1 :
      HAdd.hAdd (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ sᶜ, lineCount L i.1) =
        HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, pointCount P i.2))
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
rwa₂ :
  ∀
    (step1 :
      HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, lineCount L i.1) =
        HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, pointCount P i.2))
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (step1 : Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2))
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)

Tactic:
rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1

Premises used: add_left_cancel_iff, Finset.sum_add_sum_compl
-- 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)

Tactic:
have step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2 := by
      rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
-- 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
step3 : Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, lineCount L i.1)
    (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, pointCount P i.2)

Tactic:
rw [← Set.toFinset_compl] at step3

Premises used: Set.toFinset_compl
-- 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
step3 :
  Eq (α := ℕ) (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, lineCount L i.1)
    (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, pointCount P i.2)
i : P × L
hi : Membership.mem (γ := Finset (P × L)) (Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ) i
⊢ i.1 ∉ i.2

Tactic:
Set.mem_toFinset.mp hi

Premises used: Set.Mem, setOf, Iff.mp, Set.mem_toFinset, Not
-- 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
step3 :
  Eq (α := ℕ) (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, lineCount L i.1)
    (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, pointCount P i.2)
i : P × L
hi : Membership.mem (γ := Finset (P × L)) (Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ) i
⊢ i.1 ∉ i.2

Tactic:
exact Set.mem_toFinset.mp hi

Premises used: Iff.mp, Set.mem_toFinset
-- 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
step3 :
  Eq (α := ℕ) (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, lineCount L i.1)
    (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, pointCount P i.2)
⊢ lineCount L p = pointCount P l

Tactic:
exact
      ((Finset.sum_eq_sum_iff_of_le fun i hi =>
              HasLines.pointCount_le_lineCount (by exact Set.mem_toFinset.mp hi)).mp
          step3.symm (p, l) (Set.mem_toFinset.mpr hpl)).symm

Premises used: Iff.mpr, Finset.sum_eq_sum_iff_of_le, Prod.mk, Configuration.HasLines.pointCount_le_lineCount, Iff.mp, Set.mem_toFinset, Eq.symm
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasPoints P L
inst_2 : Fintype P
inst_3 : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
⊢ lineCount L p = pointCount P l

Tactic:
(@HasLines.lineCount_eq_pointCount (Dual L) (Dual P) _ _ _ _ hPL.symm l p hpl).symm

Premises used: Configuration.Dual, Configuration.lineCount, Configuration.HasLines.lineCount_eq_pointCount, Configuration.pointCount, Eq.symm
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
obtain : ∀ (f : L → P), Function.Bijective f → ∀ (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)), ∃ p ∈ l₁, p ∈ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
obtain ⟨f, _, hf2⟩ := HasLines.exists_bijective_of_card_eq h

Premises used: Configuration.HasLines.exists_bijective_of_card_eq
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
⊢ Nontrivial L

Tactic:
haveI : Nontrivial L := ⟨⟨l₁, l₂, hl⟩⟩
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this : Nontrivial L
⊢ Nontrivial P

Tactic:
haveI := Fintype.one_lt_card_iff_nontrivial.mp ((congr_arg _ h).mpr Fintype.one_lt_card)
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this_1 : Nontrivial L
this : Nontrivial P
⊢ ∀ (p : P), 0 < lineCount L p

Tactic:
have h₁ : ∀ p : P, 0 < lineCount L p := fun p =>
        Exists.elim (exists_ne p) fun q hq =>
          (congr_arg _ Nat.card_eq_fintype_card).mpr
            (Fintype.card_pos_iff.mpr ⟨⟨mkLine hq, (mkLine_ax hq).2⟩⟩)
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this_1 : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
⊢ ∀ (l : L), 0 < pointCount P l

Tactic:
have h₂ : ∀ l : L, 0 < pointCount P l := fun l => (congr_arg _ (hf2 l)).mpr (h₁ (f l))
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this_1 : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
obtain : ∀ (p : P) (hl₁ : p ∈ l₁), ∃ p ∈ l₁, p ∈ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
obtain ⟨p, hl₁⟩ := Fintype.card_pos_iff.mp ((congr_arg _ Nat.card_eq_fintype_card).mp (h₂ l₁))

Premises used: Eq.mp, congr_arg, Iff.mp, Fintype.card_pos_iff, 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
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this_1 : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
pos : ∀ (hl₂ : p ∈ l₂), ∃ p ∈ l₁, p ∈ l₂
neg : ∀ (hl₂ : p ∉ l₂), ∃ p ∈ l₁, p ∈ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
by_cases hl₂ : p ∈ l₂
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this_1 : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∈ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
⟨p, hl₁, hl₂⟩

Premises used: And.intro, Exists.intro
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this_1 : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∈ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
exact ⟨p, hl₁, hl₂⟩
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this_1 : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
⊢ Fintype.card.{u_1} { q : P // q ∈ l₂ } = Fintype.card.{u_2} { l : L // p ∈ l }

Tactic:
have key' : Fintype.card { q : P // q ∈ l₂ } = Fintype.card { l : L // p ∈ l } :=
        ((HasLines.lineCount_eq_pointCount h hl₂).trans Nat.card_eq_fintype_card).symm.trans
          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
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this_1 : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key' : Fintype.card.{u_1} { q : P // q ∈ l₂ } = Fintype.card.{u_2} { l : L // p ∈ l }
⊢ ∀ (q : { q : P // q ∈ l₂ }), p ≠ (↑q : P)

Tactic:
have : ∀ q : { q // q ∈ l₂ }, p ≠ q := fun q hq => hl₂ ((congr_arg (· ∈ l₂) hq).mpr q.2)
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f_1 : L → P
left : Function.Bijective f_1
hf2 : ∀ (l : L), pointCount P l = lineCount L (f_1 l)
this_1 : Nontrivial L
this_2 : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key' : Fintype.card.{u_1} { q : P // q ∈ l₂ } = Fintype.card.{u_2} { l : L // p ∈ l }
this : ∀ (q : { q : P // q ∈ l₂ }), p ≠ (↑q : P)
f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } :=
  fun (q : { q : P // q ∈ l₂ }) ↦ Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯
⊢ Function.Injective f

Tactic:
have hf : Function.Injective f := fun q₁ q₂ hq =>
        Subtype.ext ((eq_or_eq q₁.2 q₂.2 (mkLine_ax (this q₁)).2
            ((congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hq)).mpr (mkLine_ax (this q₂)).2)).resolve_right
            fun h => (congr_arg (p ∉ ·) h).mp hl₂ (mkLine_ax (this q₁)).1)
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f_1 : L → P
left : Function.Bijective f_1
hf2 : ∀ (l : L), pointCount P l = lineCount L (f_1 l)
this_1 : Nontrivial L
this_2 : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key' : Fintype.card.{u_1} { q : P // q ∈ l₂ } = Fintype.card.{u_2} { l : L // p ∈ l }
this : ∀ (q : { q : P // q ∈ l₂ }), p ≠ (↑q : P)
f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } :=
  fun (q : { q : P // q ∈ l₂ }) ↦ Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯
hf : Function.Injective f
⊢ Function.Surjective f

Tactic:
have key' := ((Fintype.bijective_iff_injective_and_card f).mpr ⟨hf, key'⟩).2
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f_1 : L → P
left : Function.Bijective f_1
hf2 : ∀ (l : L), pointCount P l = lineCount L (f_1 l)
this_1 : Nontrivial L
this_2 : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key'_1 : Fintype.card.{u_1} { q : P // q ∈ l₂ } = Fintype.card.{u_2} { l : L // p ∈ l }
this : ∀ (q : { q : P // q ∈ l₂ }), p ≠ (↑q : P)
f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } :=
  fun (q : { q : P // q ∈ l₂ }) ↦ Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯
hf : Function.Injective f
key' : Function.Surjective f
neg : ∀ (q : { q : P // q ∈ l₂ }) (hq : f q = Subtype.mk (p := fun (l : L) ↦ p ∈ l) l₁ hl₁), ∃ p ∈ l₁, p ∈ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
obtain ⟨q, hq⟩ := key' ⟨l₁, hl₁⟩

Premises used: Subtype.mk
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f_1 : L → P
left : Function.Bijective f_1
hf2 : ∀ (l : L), pointCount P l = lineCount L (f_1 l)
this_1 : Nontrivial L
this_2 : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key'_1 : Fintype.card.{u_1} { q : P // q ∈ l₂ } = Fintype.card.{u_2} { l : L // p ∈ l }
this : ∀ (q : { q : P // q ∈ l₂ }), p ≠ (↑q : P)
f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } :=
  fun (q : { q : P // q ∈ l₂ }) ↦ Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯
hf : Function.Injective f
key' : Function.Surjective f
q : { q : P // q ∈ l₂ }
hq : f q = Subtype.mk (p := fun (l : L) ↦ p ∈ l) l₁ hl₁
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
⟨q, (congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hq)).mp (mkLine_ax (this q)).2, q.2⟩

Premises used: Membership.mem, Eq.mp, Configuration.HasLines.mkLine_ax, Subtype.ext_iff, congr_arg, And.right, And.intro, Exists.intro, Iff.mp, Subtype.val, Subtype.property
-- 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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f_1 : L → P
left : Function.Bijective f_1
hf2 : ∀ (l : L), pointCount P l = lineCount L (f_1 l)
this_1 : Nontrivial L
this_2 : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key'_1 : Fintype.card.{u_1} { q : P // q ∈ l₂ } = Fintype.card.{u_2} { l : L // p ∈ l }
this : ∀ (q : { q : P // q ∈ l₂ }), p ≠ (↑q : P)
f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } :=
  fun (q : { q : P // q ∈ l₂ }) ↦ Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯
hf : Function.Injective f
key' : Function.Surjective f
q : { q : P // q ∈ l₂ }
hq : f q = Subtype.mk (p := fun (l : L) ↦ p ∈ l) l₁ hl₁
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
exact ⟨q, (congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hq)).mp (mkLine_ax (this q)).2, q.2⟩
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Fintype P
inst_3 : Fintype L
⊢ Fintype.card P = Fintype.card L

Tactic:
le_antisymm (HasLines.card_le P L) (HasPoints.card_le P L)

Premises used: le_antisymm, Configuration.HasPoints.card_le, Configuration.HasLines.card_le
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
intro : ∀ (val : Fintype P), lineCount L p = lineCount L q
⊢ lineCount L p = lineCount L q

Tactic:
cases nonempty_fintype P

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
val : Fintype P
intro : ∀ (val : Fintype L), lineCount L p = lineCount L q
⊢ lineCount L p = lineCount L q

Tactic:
cases nonempty_fintype L

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
val : Fintype P
val_1 : Fintype L
intro :
  ∀ (p₁ p₂ p₃ : P) (l₁ l₂ l₃ : L) (h₁₂ : p₁ ∉ l₂) (h₁₃ : p₁ ∉ l₃) (h₂₁ : p₂ ∉ l₁) (h₂₂ : p₂ ∈ l₂) (h₂₃ : p₂ ∈ l₃)
    (h₃₁ : p₃ ∉ l₁) (h₃₂ : p₃ ∈ l₂) (h₃₃ : p₃ ∉ l₃), lineCount L p = lineCount L q
⊢ lineCount L p = lineCount L q

Tactic:
obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _

Premises used: Configuration.ProjectivePlane.exists_config
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
val : Fintype P
val_1 : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
⊢ Fintype.card P = Fintype.card L

Tactic:
have h := card_points_eq_card_lines P L
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
val : Fintype P
val_1 : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
⊢ lineCount L p₂ = n

Tactic:
have hp₂ : lineCount L p₂ = n := rfl
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
val : Fintype P
val_1 : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
⊢ pointCount P l₁ = n

Tactic:
have hl₁ : pointCount P l₁ = n := (HasLines.lineCount_eq_pointCount h h₂₁).symm.trans hp₂
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
val : Fintype P
val_1 : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
⊢ lineCount L p₃ = n

Tactic:
have hp₃ : lineCount L p₃ = n := (HasLines.lineCount_eq_pointCount h h₃₁).trans hl₁
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
val : Fintype P
val_1 : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
⊢ pointCount P l₃ = n

Tactic:
have hl₃ : pointCount P l₃ = n := (HasLines.lineCount_eq_pointCount h h₃₃).symm.trans hp₃
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
val : Fintype P
val_1 : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
⊢ lineCount L p₁ = n

Tactic:
have hp₁ : lineCount L p₁ = n := (HasLines.lineCount_eq_pointCount h h₁₃).trans hl₃