-- Mathlib/Combinatorics/Configuration.lean
theorem HasLines.lineCount_eq_pointCount [HasLines P L] [Fintype P] [Fintype L]
    (hPL : Fintype.card P = Fintype.card L) {p : P} {l : L} (hpl : p ∉ l) :
    lineCount L p = pointCount P l

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : 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) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2
⊢ ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2

Tactic:
rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]

Result:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : 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) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2
⊢ ∑ c : P, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1 = ∑ i ∈ s, pointCount P i.2

case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : 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) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
⊢ lineCount L p = pointCount P l

Tactic:
obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL

Result:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : 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)
⊢ lineCount L p = pointCount P l

Proof state:
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : 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) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.2 ∈ univ ∧ p.1 ∈ {p_1 | p_1 ∈ p.2}.toFinset

case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : 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) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset

Tactic:
all_goals simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]; exact fun p => Iff.rfl

Result:
no goals