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 : 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
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
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
this : ∀ (p : P), lineCount L p = n
⊢ lineCount L p = lineCount L q

Tactic:
(this p).trans (this q).symm

Premises used: Eq.symm, Eq.trans
-- 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
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
this : ∀ (p : P), lineCount L p = n
⊢ lineCount L p = lineCount L q

Tactic:
exact (this p).trans (this q).symm

Premises used: Eq.symm, Eq.trans
-- 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
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
intro : ∀ (p : P), lineCount L p = n
⊢ lineCount L p = lineCount L q

Tactic:
suffices ∀ p : P, lineCount L p = n by exact (this p).trans (this q).symm
-- 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
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
⊢ ∀ (p : P), lineCount L p = n

Tactic:
fun p =>
    or_not.elim (fun h₂ => ?_) fun h₂ => (HasLines.lineCount_eq_pointCount h h₂).trans hl₂

Premises used: or_not, Configuration.HasLines.lineCount_eq_pointCount, Or.elim, Eq.trans
-- 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
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
intro : ∀ (p : P) (h₂ : p ∈ l₂), lineCount L p = n
⊢ ∀ (p : P), lineCount L p = n

Tactic:
refine fun p =>
    or_not.elim (fun h₂ => ?_) fun h₂ => (HasLines.lineCount_eq_pointCount h h₂).trans hl₂

Premises used: or_not, Configuration.HasLines.lineCount_eq_pointCount, Or.elim, Eq.trans
-- 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_1 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
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
p : P
h₂ : p ∈ l₂
⊢ lineCount L p = n

Tactic:
or_not.elim (fun h₃ => ?_) fun h₃ => (HasLines.lineCount_eq_pointCount h h₃).trans hl₃

Premises used: or_not, Configuration.HasLines.lineCount_eq_pointCount, Or.elim, Eq.trans
-- 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_1 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
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
p : P
h₂ : p ∈ l₂
⊢ p ∈ l₃

Tactic:
refine or_not.elim (fun h₃ => ?_) fun h₃ => (HasLines.lineCount_eq_pointCount h h₃).trans hl₃

Premises used: or_not, Configuration.HasLines.lineCount_eq_pointCount, Or.elim, Eq.trans
-- 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_1 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
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
p : P
h₂ : p ∈ l₂
h₃ : p ∈ l₃
intro intro₁ : lineCount L p₂ = n
⊢ lineCount L p = n

Tactic:
rw [(eq_or_eq h₂ h₂₂ h₃ h₂₃).resolve_right fun h =>
      h₃₃ ((congr_arg (p₃ ∈ ·) h).mp h₃₂)]

Premises used: Configuration.Nondegenerate.eq_or_eq, Membership.mem, Eq.mp, congr_arg, Or.resolve_right
-- 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
l m : L
⊢ pointCount P l = pointCount P m

Tactic:
apply lineCount_eq_lineCount (Dual P)

Premises used: Configuration.ProjectivePlane.lineCount_eq_lineCount, Configuration.Dual
-- 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 : P
l : L
q : P
hq : q ∉ l
intro : ∀ (val : Fintype P), lineCount L q = pointCount P l
⊢ lineCount L q = pointCount P l

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 : P
l : L
q : P
hq : q ∉ l
val : Fintype P
intro : ∀ (val : Fintype L), lineCount L q = pointCount P l
⊢ lineCount L q = pointCount P l

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 : P
l : L
q : P
hq : q ∉ l
val : Fintype P
val_1 : Fintype L
⊢ lineCount L q = pointCount P l

Tactic:
HasLines.lineCount_eq_pointCount (card_points_eq_card_lines P L) hq

Premises used: Configuration.HasLines.lineCount_eq_pointCount, Configuration.ProjectivePlane.card_points_eq_card_lines
-- 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 : P
l : L
q : P
hq : q ∉ l
val : Fintype P
val_1 : Fintype L
⊢ lineCount L q = pointCount P l

Tactic:
exact HasLines.lineCount_eq_pointCount (card_points_eq_card_lines P L) hq

Premises used: Configuration.HasLines.lineCount_eq_pointCount, Configuration.ProjectivePlane.card_points_eq_card_lines
-- 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
⊢ ProjectivePlane.order.{u_2, u_1} (Dual L) (Dual P) = ProjectivePlane.order P L

Tactic:
congr_arg (fun n => n - 1) (lineCount_eq_pointCount _ _)

Premises used: HSub.hSub, congr_arg, Configuration.ProjectivePlane.lineCount_eq_pointCount, OfNat.ofNat, Configuration.ProjectivePlane.order
-- 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 : P
obtain : ∀ (q : P) (l : L) (h : q ∈ l), lineCount L p = order P L + 1
⊢ lineCount L p = order P L + 1

Tactic:
obtain ⟨q, -, -, l, -, -, -, -, h, -⟩ := Classical.choose_spec (@exists_config P L _ _)

Premises used: Configuration.ProjectivePlane.exists_config, Classical.choose_spec
-- 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
l : L
h : q ∈ l
intro : ∀ (val : Fintype { l : L // q ∈ l }), lineCount L p = order P L + 1
⊢ lineCount L p = order P L + 1

Tactic:
cases nonempty_fintype { l : L // q ∈ 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 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p q : P
l : L
h : q ∈ l
val : Fintype { l : L // q ∈ l }
intro : 1 ≤ Fintype.card.{u_2} { l : L // q ∈ l }
⊢ lineCount L p = order P L + 1

Tactic:
rw [order, lineCount_eq_lineCount L p q, lineCount_eq_lineCount L (Classical.choose _) q,
      lineCount, Nat.card_eq_fintype_card, Nat.sub_add_cancel]

Premises used: Configuration.ProjectivePlane.lineCount_eq_lineCount, Configuration.lineCount, Nat.sub_add_cancel, Classical.choose, Configuration.ProjectivePlane.order, Nat.card_eq_fintype_card
-- 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
l : L
h : q ∈ l
val : Fintype { l : L // q ∈ l }
⊢ 1 ≤ Fintype.card.{u_2} { l : L // q ∈ l }

Tactic:
Fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩

Premises used: Iff.mpr, Nonempty.intro, Subtype.mk, Fintype.card_pos_iff, Nat.lt
-- 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
l : L
h : q ∈ l
val : Fintype { l : L // q ∈ l }
⊢ 1 ≤ Fintype.card.{u_2} { l : L // q ∈ l }

Tactic:
exact Fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩

Premises used: Iff.mpr, Nonempty.intro, Fintype.card_pos_iff
-- 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 : P
obtain : ∀ (q : P) (l : L) (h : q ∈ l), lineCount L p = order P L + 1
intro : ∀ (q : P) (l : L) (h : q ∈ l) (val : Fintype { l : L // q ∈ l }), lineCount L p = order P L + 1
intro₁ : ∀ (q : P) (l : L) (h : q ∈ l) (val : Fintype { l : L // q ∈ l }), 1 ≤ Fintype.card.{u_2} { l : L // q ∈ l }
⊢ lineCount L p = order P L + 1

Tactic:
classical
    obtain ⟨q, -, -, l, -, -, -, -, h, -⟩ := Classical.choose_spec (@exists_config P L _ _)
    cases nonempty_fintype { l : L // q ∈ l }
    rw [order, lineCount_eq_lineCount L p q, lineCount_eq_lineCount L (Classical.choose _) q,
      lineCount, Nat.card_eq_fintype_card, Nat.sub_add_cancel]
    exact Fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩

Premises used: Iff.mpr, Configuration.lineCount, Configuration.ProjectivePlane.exists_config, Nonempty.intro, Classical.choose_spec, Nat.sub_add_cancel, Configuration.ProjectivePlane.order, 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 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
l : L
⊢ pointCount P l = order P L + 1

Tactic:
(lineCount_eq (Dual P) _).trans (congr_arg (fun n => n + 1) (Dual.order P L))

Premises used: Configuration.Dual, Configuration.ProjectivePlane.lineCount_eq, congr_arg, HAdd.hAdd, Configuration.pointCount, Configuration.ProjectivePlane.Dual.order, OfNat.ofNat, Eq.trans
-- 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
obtain :
  ∀ (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₃), 1 < order P L
⊢ 1 < order P L

Tactic:
obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, -, -, 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₁ 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₃
intro : ∀ (val : Fintype { p : P // p ∈ l₂ }), 1 < order P L
⊢ 1 < order P L

Tactic:
cases nonempty_fintype { p : P // 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 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite 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₃
val : Fintype { p : P // p ∈ l₂ }
intro : ∃ (a : { p : P // p ∈ l₂ }) (b : { p : P // p ∈ l₂ }) (c : { p : P // p ∈ l₂ }), a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ 1 < order P L

Tactic:
rw [← add_lt_add_iff_right 1, ← pointCount_eq _ l₂, pointCount, Nat.card_eq_fintype_card,
    Fintype.two_lt_card_iff]

Premises used: Fintype.two_lt_card_iff, Configuration.pointCount, Configuration.ProjectivePlane.pointCount_eq, OfNat.ofNat, add_lt_add_iff_right, Nat.card_eq_fintype_card
-- 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₁ 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₃
val : Fintype { p : P // p ∈ l₂ }
intro :
  ∃ (a : { p : P // p ∈ l₂ }) (b : { p : P // p ∈ l₂ }) (c : { p : P // p ∈ l₂ }),
    ¬(↑a : P) = (↑b : P) ∧ ¬(↑a : P) = (↑c : P) ∧ ¬(↑b : P) = (↑c : P)
⊢ ∃ (a : { p : P // p ∈ l₂ }) (b : { p : P // p ∈ l₂ }) (c : { p : P // p ∈ l₂ }), a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [Ne, Subtype.ext_iff]

Premises used: Ne, Subtype.ext_iff
-- 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₁ 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₃
val : Fintype { p : P // p ∈ l₂ }
⊢ @mkPoint.{u_1, u_2} _ L inst _ l₁ l₂ ⋯ ∈ l₁ ∧ @mkPoint.{u_1, u_2} _ L inst _ l₁ l₂ ⋯ ∈ l₂

Tactic:
have h := mkPoint_ax (P := P) (L := L) fun h => h₂₁ ((congr_arg (p₂ ∈ ·) h).mpr h₂₂)
-- 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₁ 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₃
val : Fintype { p : P // p ∈ l₂ }
h : @mkPoint.{u_1, u_2} _ L inst _ l₁ l₂ ⋯ ∈ l₁ ∧ @mkPoint.{u_1, u_2} _ L inst _ l₁ l₂ ⋯ ∈ l₂
⊢ ∃ (a : { p : P // p ∈ l₂ }) (b : { p : P // p ∈ l₂ }) (c : { p : P // p ∈ l₂ }),
    ¬(↑a : P) = (↑b : P) ∧ ¬(↑a : P) = (↑c : P) ∧ ¬(↑b : P) = (↑c : P)

Tactic:
⟨⟨mkPoint _, h.2⟩, ⟨p₂, h₂₂⟩, ⟨p₃, h₃₂⟩, ne_of_mem_of_not_mem h.1 h₂₁,
      ne_of_mem_of_not_mem h.1 h₃₁, ne_of_mem_of_not_mem h₂₃ h₃₃⟩

Premises used: ne_of_mem_of_not_mem, Subtype.mk, And.right, And.left, And.intro, Configuration.HasPoints.mkPoint, Exists.intro
-- 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₁ 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₃
val : Fintype { p : P // p ∈ l₂ }
h : @mkPoint.{u_1, u_2} _ L inst _ l₁ l₂ ⋯ ∈ l₁ ∧ @mkPoint.{u_1, u_2} _ L inst _ l₁ l₂ ⋯ ∈ l₂
⊢ ∃ (a : { p : P // p ∈ l₂ }) (b : { p : P // p ∈ l₂ }) (c : { p : P // p ∈ l₂ }),
    ¬(↑a : P) = (↑b : P) ∧ ¬(↑a : P) = (↑c : P) ∧ ¬(↑b : P) = (↑c : P)

Tactic:
exact
    ⟨⟨mkPoint _, h.2⟩, ⟨p₂, h₂₂⟩, ⟨p₃, h₃₂⟩, ne_of_mem_of_not_mem h.1 h₂₁,
      ne_of_mem_of_not_mem h.1 h₃₁, ne_of_mem_of_not_mem h₂₃ h₃₃⟩
-- 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 : P
⊢ 2 < lineCount L p

Tactic:
simpa only [lineCount_eq L p, Nat.succ_lt_succ_iff] using one_lt_order P L

Premises used: Nat.succ_lt_succ_iff, Configuration.ProjectivePlane.lineCount_eq, Configuration.ProjectivePlane.one_lt_order
-- 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
l : L
⊢ 2 < pointCount P l

Tactic:
simpa only [pointCount_eq P l, Nat.succ_lt_succ_iff] using one_lt_order P L

Premises used: Nat.succ_lt_succ_iff, Configuration.ProjectivePlane.one_lt_order, Configuration.ProjectivePlane.pointCount_eq
-- 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 : Finite L
intro : ∀ (val : Fintype L), Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
⊢ Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1

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 : Fintype P
inst_3 : Finite L
val : Fintype L
intro : ∀ (p : P), Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
⊢ Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1

Tactic:
obtain ⟨p, -⟩ := @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 : Fintype P
inst_3 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
apply : Fintype.card.{u_1} { q : P // q ≠ p } = Fintype.card P - Nat.succ 0
⊢ Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P

Tactic:
apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp

Premises used: Iff.mpr, Nat.succ_le_of_lt, Nonempty.intro, Iff.mp, eq_tsub_iff_add_eq_of_le, Fintype.card_pos_iff
-- 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 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card.{u_1} { x : P // ¬x = p } = Fintype.card P - 1

Tactic:
(Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))

Premises used: congr_arg, Fintype.card_subtype_compl, Eq.trans, Fintype.card_subtype_eq
-- 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 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card.{u_1} { q : P // q ≠ p } = Fintype.card P - Nat.succ 0

Tactic:
convert! (Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))

Premises used: congr_arg, Fintype.card_subtype_compl, Eq.trans, Fintype.card_subtype_eq
-- 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 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P

Tactic:
have h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P := by
      apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp
      convert! (Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))