-- Mathlib/Combinatorics/Configuration.lean
theorem lineCount_eq_lineCount [Finite P] [Finite L] (p q : P) : lineCount L p = lineCount L q

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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:
refine fun p =>
  or_not.elim (fun h₂ => ?_) fun h₂ => (HasLines.lineCount_eq_pointCount h h₂).trans hl₂

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p✝ q : P
val✝¹ : Fintype P
val✝ : 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

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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

Tactic:
suffices ∀ p : P, lineCount L p = n by exact (this p).trans (this q).symm

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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

Proof state:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝ : Fintype P
⊢ lineCount L p = lineCount L q

Tactic:
cases nonempty_fintype L

Result:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : Fintype L
⊢ lineCount L p = lineCount L q

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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

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

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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

Proof state:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : Fintype 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 _ _

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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

Tactic:
have hl₃ : pointCount P l₃ = n := (HasLines.lineCount_eq_pointCount h h₃₃).symm.trans hp₃

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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

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

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : 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