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 : 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₂
obtain₁ :
  ∀ (f : L → P),
    Function.Bijective f →
      ∀ (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)) (this : Nontrivial L), ∃ p ∈ l₁, p ∈ l₂
obtain₂ :
  ∀ (f : L → P),
    Function.Bijective f →
      ∀ (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)) (this : Nontrivial L) (this : Nontrivial P),
        ∃ p ∈ l₁, p ∈ l₂
obtain₃ :
  ∀ (f : L → P),
    Function.Bijective f →
      ∀ (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)) (this : Nontrivial L) (this : Nontrivial P)
        (h₁ : ∀ (p : P), 0 < lineCount L p), ∃ p ∈ l₁, p ∈ l₂
obtain₄ :
  ∀ (f : L → P),
    Function.Bijective f →
      ∀ (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)) (this : Nontrivial L) (this : Nontrivial P)
        (h₁ : ∀ (p : P), 0 < lineCount L p) (h₂ : ∀ (l : L), 0 < pointCount P l), ∃ p ∈ l₁, p ∈ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂
have obtain₅ : ∀ (f : L → P),
  Function.Bijective f →
    ∀ (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)) (this : Nontrivial L) (this : Nontrivial P)
      (h₁ : ∀ (p : P), 0 < lineCount L p) (h₂ : ∀ (l : L), 0 < pointCount P l) (p : P) (hl₁ : p ∈ l₁), ∃ p ∈ l₁, p ∈ l₂
Tactic: classical
      obtain ⟨f, _, hf2⟩ := HasLines.exists_bijective_of_card_eq h
      haveI : Nontrivial L := ⟨⟨l₁, l₂, hl⟩⟩
      haveI := Fintype.one_lt_card_iff_nontrivial.mp ((congr_arg _ h).mpr Fintype.one_lt_card)
      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⟩⟩)
      have h₂ : ∀ l : L, 0 < pointCount P l := fun l => (congr_arg _ (hf2 l)).mpr (h₁ (f l))
      obtain ⟨p, hl₁⟩ := Fintype.card_pos_iff.mp ((congr_arg _ Nat.card_eq_fintype_card).mp (h₂ l₁))
      by_cases hl₂ : p ∈ l₂
      · exact ⟨p, hl₁, hl₂⟩
      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
      have : ∀ q : { q // q ∈ l₂ }, p ≠ q := fun q hq => hl₂ ((congr_arg (· ∈ l₂) hq).mpr q.2)
      let f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } := fun q =>
        ⟨mkLine (this q), (mkLine_ax (this q)).1⟩
      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)
      have key' := ((Fintype.bijective_iff_injective_and_card f).mpr ⟨hf, key'⟩).2
      obtain ⟨q, hq⟩ := key' ⟨l₁, hl₁⟩
      exact ⟨q, (congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hq)).mp (mkLine_ax (this q)).2, q.2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ lineCount L p = lineCount L q
have intro : ∀ (val : Fintype P), lineCount L p = lineCount L q
Tactic: cases nonempty_fintype P
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ lineCount L p = lineCount L q
have intro : ∀ (val : Fintype L), lineCount L p = lineCount L q
Tactic: cases nonempty_fintype L
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ lineCount L p = lineCount L q
have 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
Tactic: obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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₃
⊢ lineCount L p = lineCount L q
have h : Fintype.card P = Fintype.card L
Tactic: have h := card_points_eq_card_lines P L
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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 = lineCount L q
have hp₂ : lineCount L p₂ = n
Tactic: have hp₂ : lineCount L p₂ = n := rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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
⊢ lineCount L p = lineCount L q
have hl₁ : pointCount P l₁ = n
Tactic: have hl₁ : pointCount P l₁ = n := (HasLines.lineCount_eq_pointCount h h₂₁).symm.trans 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 : 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 = lineCount L q
have hp₃ : lineCount L p₃ = n
Tactic: have hp₃ : lineCount L p₃ = n := (HasLines.lineCount_eq_pointCount h h₃₁).trans hl₁
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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
⊢ lineCount L p = lineCount L q
have hl₃ : pointCount P l₃ = n
Tactic: have hl₃ : pointCount P l₃ = n := (HasLines.lineCount_eq_pointCount h h₃₃).symm.trans 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 : 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 = lineCount L q
have hp₁ : lineCount L p₁ = n
Tactic: have hp₁ : lineCount L p₁ = n := (HasLines.lineCount_eq_pointCount h h₁₃).trans hl₃
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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
⊢ lineCount L p = lineCount L q
have hl₂ : pointCount P l₂ = n
Tactic: have hl₂ : pointCount P l₂ = n := (HasLines.lineCount_eq_pointCount h h₁₂).symm.trans 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 : 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
⊢ lineCount L p = lineCount L q
have intro : ∀ (p : P), lineCount L p = n
Tactic: suffices ∀ p : P, lineCount L p = n by exact (this p).trans (this q).symm
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
have intro : ∀ (p : P) (h₂ : p ∈ l₂), lineCount L p = n
Tactic: refine fun p =>
    or_not.elim (fun h₂ => ?_) fun h₂ => (HasLines.lineCount_eq_pointCount h h₂).trans hl₂
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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
have h₃ : p ∈ l₃
Tactic: refine or_not.elim (fun h₃ => ?_) fun h₃ => (HasLines.lineCount_eq_pointCount h h₃).trans 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 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Finite L
p : P
l : L
q : P
hq : q ∉ l
⊢ lineCount L q = pointCount P l
have intro : ∀ (val : Fintype P), lineCount L q = pointCount P l
Tactic: cases nonempty_fintype P
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ lineCount L q = pointCount P l
have intro : ∀ (val : Fintype L), lineCount L q = pointCount P l
Tactic: cases nonempty_fintype L
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ lineCount L p = order P L + 1
have obtain : ∀ (q : P) (l : L) (h : q ∈ l), lineCount L p = order P L + 1
Tactic: obtain ⟨q, -, -, l, -, -, -, -, h, -⟩ := Classical.choose_spec (@exists_config P L _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ lineCount L p = order P L + 1
have intro : ∀ (val : Fintype { l : L // q ∈ l }), lineCount L p = order P L + 1
Tactic: cases nonempty_fintype { l : L // q ∈ l }
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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 }
⊢ lineCount L p = order P L + 1
have intro : 1 ≤ Fintype.card.{u_2} { l : L // q ∈ l }
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ lineCount L p = order P L + 1
have obtain : ∀ (q : P) (l : L) (h : 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⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
have intro : ∀ (q : P) (l : L) (h : q ∈ l) (val : Fintype { 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⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ lineCount L p = order P L + 1
have intro₁ : ∀ (q : P) (l : L) (h : q ∈ l) (val : Fintype { l : L // q ∈ l }), 1 ≤ Fintype.card.{u_2} { l : L // q ∈ l }
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⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ 1 < order P L
have 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
Tactic: obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, -, -, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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₃
⊢ 1 < order P L
have intro : ∀ (val : Fintype { p : P // p ∈ l₂ }), 1 < order P L
Tactic: cases nonempty_fintype { p : P // p ∈ l₂ }
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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₂ }
⊢ 1 < order P L
have intro : ∃ (a : { p : P // p ∈ l₂ }) (b : { p : P // p ∈ l₂ }) (c : { p : P // p ∈ l₂ }), a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: rw [← add_lt_add_iff_right 1, ← pointCount_eq _ l₂, pointCount, Nat.card_eq_fintype_card,
    Fintype.two_lt_card_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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₂ }
⊢ ∃ (a : { p : P // p ∈ l₂ }) (b : { p : P // p ∈ l₂ }) (c : { p : P // p ∈ l₂ }), a ≠ b ∧ a ≠ c ∧ b ≠ c
have 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)
Tactic: simp_rw [Ne, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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₂ }
⊢ ∃ (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)
have h : @mkPoint.{u_1, u_2} _ L inst _ l₁ l₂ sorry ∈ l₁ ∧ @mkPoint.{u_1, u_2} _ L inst _ l₁ l₂ sorry ∈ l₂
Tactic: have h := mkPoint_ax (P := P) (L := L) fun h => h₂₁ ((congr_arg (p₂ ∈ ·) h).mpr h₂₂)
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
have intro : ∀ (val : Fintype L), Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
Tactic: cases nonempty_fintype L
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
⊢ Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
have intro : ∀ (p : P), Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
Tactic: obtain ⟨p, -⟩ := @exists_config P L _ _
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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
have apply : Fintype.card.{u_1} { q : P // q ≠ p } = Fintype.card P - Nat.succ 0
Tactic: apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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 P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
have h1 : 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))
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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 := ⋯ }
h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
l : { l : L // p ∈ l }
⊢ Fintype.card.{u_1} { q : P // q ∈ (↑l : L) ∧ q ≠ p } = order P L
have rw : Nat.card.{u_1} { x : P // x ∈ (↑l : L) } - Fintype.card.{u_1} { x : { x : P // x ∈ (↑l : L) } // (↑x : P) = p } =
  order P L
Tactic: rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
        Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ←
        Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
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 := ⋯ }
h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
l : { l : L // p ∈ l }
⊢ Nat.card.{u_1} { x : P // x ∈ (↑l : L) } - Fintype.card.{u_1} { x : { x : P // x ∈ (↑l : L) } // (↑x : P) = p } =
    order P L
have refine : order P L + 1 = order P L + Fintype.card.{u_1} { x : { x : P // x ∈ (↑l : L) } // (↑x : P) = p }
Tactic: refine tsub_eq_of_eq_add ((pointCount_eq P l.1).trans ?_)