-- 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:
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)
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
step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2
step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2
⊢ lineCount L p = pointCount P l

Tactic:
rw [← Set.toFinset_compl] at step3

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)
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
step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2
step3 : ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, lineCount L i.1 = ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, pointCount P i.2
⊢ 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.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset

Tactic:
simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]

Result:
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 ∈ {i | i.1 ∈ i.2} ↔ p.2 ∈ {l | p.1 ∈ l}

Proof state:
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)
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
step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2
step3 : ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, lineCount L i.1 = ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, 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

Result:
no goals

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
⊢ ∑ y : L, ∑ x : P, lineCount L (x, y).1 = ∑ x : P, ∑ y : L, pointCount P (x, y).2

Tactic:
simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]

Result:
no goals

Proof state:
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

Tactic:
let s : Finset (P × L) := Set.toFinset { i | i.1 ∈ i.2 }

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)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ 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 ∈ {i | i.1 ∈ i.2} ↔ p.2 ∈ {l | p.1 ∈ l}

Tactic:
exact fun p => Iff.rfl

Result:
no goals

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
l : L
x✝ : l ∈ univ
⊢ Nat.card ↑{p | p ∈ l} • lineCount L (f l) = Nat.card ↑{l_1 | f l ∈ l_1} • lineCount L (f l)

Tactic:
change pointCount P l • _ = lineCount L (f 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
l : L
x✝ : l ∈ univ
⊢ pointCount P l • lineCount L (f l) = lineCount L (f l) • lineCount L (f 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
l : L
x✝ : l ∈ univ
⊢ pointCount P l • lineCount L (f l) = lineCount L (f l) • lineCount L (f l)

Tactic:
rw [hf2]

Result:
no goals

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
⊢ ∑ c : L, ∑ a ∈ {p | p ∈ c}.toFinset, pointCount P (a, c).2 = ∑ c : P, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1

Tactic:
refine sum_bijective _ hf1 (by simp) fun 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
l : L
x✝ : l ∈ univ
⊢ ∑ a ∈ {p | p ∈ l}.toFinset, pointCount P (a, l).2 = ∑ a ∈ {l_1 | f l ∈ l_1}.toFinset, lineCount L (f l, a).1