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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ c : P, ∑ a ∈ Set.toFinset {l : L | c ∈ l}, lineCount L (c, a).1) (∑ i ∈ s, pointCount P i.2)
have rw : Eq (α := ℕ) (∑ c : L, ∑ a ∈ Set.toFinset {p : P | p ∈ c}, pointCount P (a, c).2)
  (∑ c : P, ∑ a ∈ Set.toFinset {l : L | c ∈ l}, lineCount L (c, a).1)
Tactic: rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
-- 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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
rw :
  Eq (α := ℕ) (∑ c : L, ∑ a ∈ Set.toFinset {p : P | p ∈ c}, pointCount P (a, c).2)
    (∑ c : P, ∑ a ∈ Set.toFinset {l : L | c ∈ l}, lineCount L (c, a).1)
⊢ Eq (α := ℕ) (∑ c : P, ∑ a ∈ Set.toFinset {l : L | c ∈ l}, lineCount L (c, a).1) (∑ i ∈ s, pointCount P i.2)
have h : ∀ (p : P × L),
  p ∈ s ↔
    Membership.mem (γ := Finset L) univ p.2 ∧ Membership.mem (γ := Finset P) (Set.toFinset {p_1 : P | p_1 ∈ p.2}) p.1
Tactic: rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
-- 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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ c : L, ∑ a ∈ Set.toFinset {p : P | p ∈ c}, pointCount P (a, c).2)
    (∑ c : P, ∑ a ∈ Set.toFinset {l : L | c ∈ l}, lineCount L (c, a).1)
have refine : ∀ (l : L),
  Membership.mem (γ := Finset L) univ l →
    Eq (α := ℕ) (∑ a ∈ Set.toFinset {p : P | p ∈ l}, pointCount P (a, l).2)
      (∑ a ∈ Set.toFinset {l_1 : L | f l ∈ l_1}, lineCount L (f l, a).1)
Tactic: refine sum_bijective _ hf1 (by simp) fun 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 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l_1 : L
hpl : p ∉ l_1
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
l : L
h : Membership.mem (γ := Finset L) univ l
⊢ Eq (α := ℕ) (∑ a ∈ Set.toFinset {p : P | p ∈ l}, pointCount P (a, l).2)
    (∑ a ∈ Set.toFinset {l_2 : L | f l ∈ l_2}, lineCount L (f l, a).1)
have simp_rw : Nat.card.{u_1} (↑{p : P | p ∈ l} : Type u_1) • lineCount L (f l) =
  Nat.card.{u_2} (↑{l_2 : L | f l ∈ l_2} : Type u_2) • lineCount L (f l)
Tactic: simp_rw [hf2, sum_const, Set.toFinset_card, ← 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 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l_1 : L
hpl : p ∉ l_1
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
l : L
h : Membership.mem (γ := Finset L) univ l
⊢ Nat.card.{u_1} (↑{p : P | p ∈ l} : Type u_1) • lineCount L (f l) =
    Nat.card.{u_2} (↑{l_2 : L | f l ∈ l_2} : Type u_2) • lineCount L (f l)
have change : pointCount P l • lineCount L (f l) = lineCount L (f l) • lineCount L (f l)
Tactic: change pointCount P l • _ = lineCount L (f 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 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l_1 : L
hpl : p ∉ l_1
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
l : L
h : Membership.mem (γ := Finset L) univ l
⊢ pointCount P l • lineCount L (f l) = lineCount L (f l) • lineCount L (f l)
have rw : lineCount L (f l) • lineCount L (f l) = lineCount L (f l) • lineCount L (f l)
Tactic: rw [hf2]
-- 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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ c : P, ∑ a ∈ Set.toFinset {l : L | c ∈ l}, lineCount L (c, a).1) (∑ i ∈ s, pointCount P i.2)
have h : ∀ (p : P × L),
  p ∈ s ↔
    Membership.mem (γ := Finset L) univ p.2 ∧ Membership.mem (γ := Finset P) (Set.toFinset {p_1 : P | p_1 ∈ p.2}) p.1
Tactic: on_goal 1 =>
        rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
        · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
          simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
          change pointCount P l • _ = lineCount L (f l) • _
          rw [hf2]
-- 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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
⊢ ∀ (p : P × L),
    p ∈ s ↔
      Membership.mem (γ := Finset L) univ p.2 ∧ Membership.mem (γ := Finset P) (Set.toFinset {p_1 : P | p_1 ∈ p.2}) p.1
have h : ∀ (p : P × L),
  Membership.mem (γ := Set (P × L)) {i : P × L | i.1 ∈ i.2} p ↔ Membership.mem (γ := Set P) {p_1 : P | p_1 ∈ p.2} p.1
Tactic: simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]
-- 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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
⊢ ∀ (p : P × L),
    p ∈ s ↔
      Membership.mem (γ := Finset P) univ p.1 ∧ Membership.mem (γ := Finset L) (Set.toFinset {l : L | p.1 ∈ l}) p.2
have h : ∀ (p : P × L),
  Membership.mem (γ := Set (P × L)) {i : P × L | i.1 ∈ i.2} p ↔ Membership.mem (γ := Set L) {l : L | p.1 ∈ l} p.2
Tactic: simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
⊢ lineCount L p = pointCount P l
have step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
Tactic: have step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 := by
      rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]
      on_goal 1 =>
        rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
        · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
          simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
          change pointCount P l • _ = lineCount L (f l) • _
          rw [hf2]
      all_goals simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]; exact fun p => Iff.rfl
-- 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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
have rwa : ∀ (step1 : HAdd.hAdd (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ sᶜ, lineCount L i.1) = ∑ i : P × L, pointCount P i.2)
  (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
  Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
Tactic: rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
Cleared hypotheses: step1, step2
-- 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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
rwa :
  ∀ (step1 : HAdd.hAdd (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ sᶜ, lineCount L i.1) = ∑ i : P × L, pointCount P i.2)
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
have rwa₁ : ∀
  (step1 :
    HAdd.hAdd (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ sᶜ, lineCount L i.1) =
      HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, pointCount P i.2))
  (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
  Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
Tactic: rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
Cleared hypotheses: step1, step2
-- 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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
rwa :
  ∀ (step1 : HAdd.hAdd (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ sᶜ, lineCount L i.1) = ∑ i : P × L, pointCount P i.2)
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
rwa₁ :
  ∀
    (step1 :
      HAdd.hAdd (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ sᶜ, lineCount L i.1) =
        HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, pointCount P i.2))
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
have rwa₂ : ∀
  (step1 :
    HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, lineCount L i.1) =
      HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, pointCount P i.2))
  (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
  Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
Tactic: rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
Cleared hypotheses: step1, step2
-- 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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
rwa :
  ∀ (step1 : HAdd.hAdd (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ sᶜ, lineCount L i.1) = ∑ i : P × L, pointCount P i.2)
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
rwa₁ :
  ∀
    (step1 :
      HAdd.hAdd (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ sᶜ, lineCount L i.1) =
        HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, pointCount P i.2))
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
rwa₂ :
  ∀
    (step1 :
      HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, lineCount L i.1) =
        HAdd.hAdd (α := ℕ) (∑ i ∈ s, pointCount P i.2) (∑ i ∈ sᶜ, pointCount P i.2))
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
    Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
have rwa₃ : ∀ (step1 : Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2))
  (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)),
  Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
Tactic: rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
Cleared hypotheses: step1, step2
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
⊢ lineCount L p = pointCount P l
have step3 : Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
Tactic: have step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2 := by
      rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
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
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) := Set.toFinset {i : P × L | i.1 ∈ i.2}
step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
step3 : Eq (α := ℕ) (∑ i ∈ sᶜ, lineCount L i.1) (∑ i ∈ sᶜ, pointCount P i.2)
⊢ lineCount L p = pointCount P l
have step3₁ : Eq (α := ℕ) (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, lineCount L i.1)
  (∑ i ∈ Set.toFinset {i : P × L | i.1 ∈ i.2}ᶜ, pointCount P i.2)
Tactic: rw [← Set.toFinset_compl] at step3
Cleared hypotheses: step3
-- 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
⊢ lineCount L p = pointCount P l
have obtain : ∀ (f : L → P) (hf1 : Function.Bijective f) (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)),
  lineCount L p = pointCount P l
Tactic: classical
    obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL
    let s : Finset (P × L) := Set.toFinset { i | i.1 ∈ i.2 }
    have step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2 := by
      rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
      simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
    have step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 := by
      rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]
      on_goal 1 =>
        rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
        · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
          simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
          change pointCount P l • _ = lineCount L (f l) • _
          rw [hf2]
      all_goals simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]; exact fun p => Iff.rfl
    have step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2 := by
      rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
    rw [← Set.toFinset_compl] at step3
    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
-- 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
obtain :
  ∀ (f : L → P) (hf1 : Function.Bijective f) (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)),
    lineCount L p = pointCount P l
obtain₁ :
  ∀ (f : L → P) (hf1 : Function.Bijective f) (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)),
    lineCount L p = pointCount P l
⊢ lineCount L p = pointCount P l
have obtain₂ : ∀ (f : L → P) (hf1 : Function.Bijective f) (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l))
  (step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)), lineCount L p = pointCount P l
Tactic: classical
    obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL
    let s : Finset (P × L) := Set.toFinset { i | i.1 ∈ i.2 }
    have step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2 := by
      rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
      simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
    have step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 := by
      rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]
      on_goal 1 =>
        rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
        · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
          simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
          change pointCount P l • _ = lineCount L (f l) • _
          rw [hf2]
      all_goals simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]; exact fun p => Iff.rfl
    have step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2 := by
      rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
    rw [← Set.toFinset_compl] at step3
    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
-- 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
obtain :
  ∀ (f : L → P) (hf1 : Function.Bijective f) (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)),
    lineCount L p = pointCount P l
obtain₁ :
  ∀ (f : L → P) (hf1 : Function.Bijective f) (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)),
    lineCount L p = pointCount P l
obtain₂ :
  ∀ (f : L → P) (hf1 : Function.Bijective f) (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l))
    (step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)), lineCount L p = pointCount P l
⊢ lineCount L p = pointCount P l
have obtain₃ : ∀ (f : L → P) (hf1 : Function.Bijective f) (hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)),
  let s : Finset (P × L) := Set.toFinset {i : P × L | i.1 ∈ i.2};
  ∀ (step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2))
    (step2 : Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)), lineCount L p = pointCount P l
Tactic: classical
    obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL
    let s : Finset (P × L) := Set.toFinset { i | i.1 ∈ i.2 }
    have step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2 := by
      rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
      simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
    have step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 := by
      rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]
      on_goal 1 =>
        rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
        · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
          simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
          change pointCount P l • _ = lineCount L (f l) • _
          rw [hf2]
      all_goals simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]; exact fun p => Iff.rfl
    have step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2 := by
      rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
    rw [← Set.toFinset_compl] at step3
    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