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 : Fintype P
inst_2 : Fintype L
⊢ Eq (α := ℕ) (∑ p : P, lineCount L p) (∑ l : L, pointCount P l)
have simp : Fintype.card ((i : P) × { l : L // i ∈ l }) = Fintype.card ((i : L) × { p : P // p ∈ i })
Tactic: classical
    simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]
    apply Fintype.card_congr
    calc
      (Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } :=
        (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
      _ ≃ { x : L × P // x.2 ∈ x.1 } := (Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl
      _ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (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 : Fintype P
inst_2 : Fintype L
simp : Fintype.card ((i : P) × { l : L // i ∈ l }) = Fintype.card ((i : L) × { p : P // p ∈ i })
⊢ Eq (α := ℕ) (∑ p : P, lineCount L p) (∑ l : L, pointCount P l)
have f : (i : P) × { l : L // i ∈ l } ≃ (i : L) × { p : P // p ∈ i }
Tactic: classical
    simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]
    apply Fintype.card_congr
    calc
      (Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } :=
        (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
      _ ≃ { x : L × P // x.2 ∈ x.1 } := (Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl
      _ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (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 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
have pos : ∀ (hf : Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }), pointCount P l ≤ lineCount L p
Tactic: by_cases hf : Infinite { 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 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
pos : ∀ (hf : Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }), pointCount P l ≤ lineCount L p
⊢ pointCount P l ≤ lineCount L p
have neg : ∀ (hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }), pointCount P l ≤ lineCount L p
Tactic: by_cases hf : Infinite { 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 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
have neg : ∀ (this : Fintype { p : P // p ∈ l }), pointCount P l ≤ lineCount L p
Tactic: haveI := fintypeOfNotInfinite hf
-- 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
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
this : Fintype { p : P // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
have neg : ∀ (val : Fintype { l : L // p ∈ l }), pointCount P l ≤ lineCount L p
Tactic: cases nonempty_fintype { l : L // 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 : HasLines P L
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
this : Fintype { p : P // p ∈ l }
val : Fintype { l : L // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
have neg : Fintype.card.{u_1} { p : P // p ∈ l } ≤ Fintype.card.{u_2} { l : L // p ∈ l }
Tactic: rw [lineCount, pointCount, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
-- 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
p : P
l : L
h : p ∉ l
inst_2 : Finite.{max 1 (u_2 + 1)} { l : L // p ∈ l }
hf : ¬Infinite.{max 1 (u_1 + 1)} { p : P // p ∈ l }
this : Fintype { p : P // p ∈ l }
val : Fintype { l : L // p ∈ l }
⊢ Fintype.card.{u_1} { p : P // p ∈ l } ≤ Fintype.card.{u_2} { l : L // p ∈ l }
have this₁ : ∀ (p' : { p : P // p ∈ l }), p ≠ (↑p' : P)
Tactic: have : ∀ p' : { p // p ∈ l }, p ≠ p' := fun p' hp' => h ((congr_arg (· ∈ l) hp').mpr p'.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 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
⊢ Fintype.card P ≤ Fintype.card L
have by_contra : ∀ (hc₂ : ¬Fintype.card P ≤ Fintype.card L), False
Tactic: by_contra hc₂
-- 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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
⊢ False
have obtain : ∀ (f : L → P) (hf₁ : Function.Injective f) (hf₂ : ∀ (l : L), f l ∉ l), False
Tactic: obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_ge hc₂)
-- 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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ Eq (α := ℕ) (∑ l : L, lineCount L (f l)) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p)
have rw : Eq (α := ℕ) (∑ l : L, lineCount L (f l))
  (∑ x : L, lineCount.{u_1, u_2} (P := P) L (({ toFun := f, inj' := hf₁ : L ↪ P } : (a : L) → P) x : P))
Tactic: rw [sum_map]
-- 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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ LT.lt (α := ℕ) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p) (∑ p : P, lineCount L p)
have obtain : ∀ (p : P) (hp : ¬∃ (a : L), f a = p),
  LT.lt (α := ℕ) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p) (∑ p : P, lineCount L p)
Tactic: obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
-- 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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ (a : L), f a = p
⊢ LT.lt (α := ℕ) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p) (∑ p : P, lineCount L p)
have refine_1 : p ∉ map { toFun := f, inj' := hf₁ : L ↪ P } univ
Tactic: refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
-- 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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ (a : L), f a = p
refine_1 : p ∉ map { toFun := f, inj' := hf₁ : L ↪ P } univ
⊢ LT.lt (α := ℕ) (∑ p ∈ map { toFun := f, inj' := hf₁ : L ↪ P } univ, lineCount L p) (∑ p : P, lineCount L p)
have refine_2 : 0 < lineCount L p
Tactic: refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
-- 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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ (a : L), f a = p
⊢ 0 < lineCount L p
have refine_2 : Nonempty.{u_2 + 1} { l : L // p ∈ l }
Tactic: rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_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 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ (a : L), f a = p
⊢ Nonempty.{u_2 + 1} { l : L // p ∈ l }
have refine_2 : ∀ (l : L), p ∉ l → Nonempty.{u_2 + 1} { l : L // p ∈ l }
Tactic: obtain ⟨l, _⟩ := @exists_line P L _ _ p
-- 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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ False
have this : LT.lt (α := ℕ) (∑ p : P, lineCount L p) (∑ p : P, lineCount L p)
Tactic: have :=
    calc
      ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
      _ ≤ ∑ l, lineCount L (f l) :=
        (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
      _ = ∑ p ∈ univ.map ⟨f, hf₁⟩, lineCount L p := by rw [sum_map]; dsimp
      _ < ∑ p, lineCount L p := by
        obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
        refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
        · simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]
        · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
          obtain ⟨l, _⟩ := @exists_line P L _ _ p
          exact
            let this := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).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 : HasLines P L
inst_2 : Fintype P
inst_3 : Fintype L
⊢ Fintype.card P ≤ Fintype.card L
have by_contra : ¬Fintype.card P ≤ Fintype.card L → False
Tactic: classical
  by_contra hc₂
  obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_ge hc₂)
  have :=
    calc
      ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
      _ ≤ ∑ l, lineCount L (f l) :=
        (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
      _ = ∑ p ∈ univ.map ⟨f, hf₁⟩, lineCount L p := by rw [sum_map]; dsimp
      _ < ∑ p, lineCount L p := by
        obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
        refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
        · simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]
        · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
          obtain ⟨l, _⟩ := @exists_line P L _ _ p
          exact
            let this := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩
  exact lt_irrefl _ this
-- 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
by_contra by_contra₁ by_contra₂ : ∀ (hc₂ : ¬Fintype.card P ≤ Fintype.card L), False
⊢ Fintype.card P ≤ Fintype.card L
have by_contra₃ : ∀ (hc₂ : ¬Fintype.card P ≤ Fintype.card L) (f : L → P) (hf₁ : Function.Injective f) (hf₂ : ∀ (l : L), f l ∉ l), False
Tactic: classical
  by_contra hc₂
  obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_ge hc₂)
  have :=
    calc
      ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
      _ ≤ ∑ l, lineCount L (f l) :=
        (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
      _ = ∑ p ∈ univ.map ⟨f, hf₁⟩, lineCount L p := by rw [sum_map]; dsimp
      _ < ∑ p, lineCount L p := by
        obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
        refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
        · simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]
        · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
          obtain ⟨l, _⟩ := @exists_line P L _ _ p
          exact
            let this := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩
  exact lt_irrefl _ this
-- 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
by_contra by_contra₁ by_contra₂ : ∀ (hc₂ : ¬Fintype.card P ≤ Fintype.card L), False
by_contra₃ :
  ∀ (hc₂ : ¬Fintype.card P ≤ Fintype.card L) (f : L → P) (hf₁ : Function.Injective f) (hf₂ : ∀ (l : L), f l ∉ l), False
⊢ Fintype.card P ≤ Fintype.card L
have by_contra₄ : ∀ (hc₂ : ¬Fintype.card P ≤ Fintype.card L) (f : L → P) (hf₁ : Function.Injective f) (hf₂ : ∀ (l : L), f l ∉ l)
  (this : LT.lt (α := ℕ) (∑ p : P, lineCount L p) (∑ p : P, lineCount L p)), False
Tactic: classical
  by_contra hc₂
  obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_ge hc₂)
  have :=
    calc
      ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
      _ ≤ ∑ l, lineCount L (f l) :=
        (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
      _ = ∑ p ∈ univ.map ⟨f, hf₁⟩, lineCount L p := by rw [sum_map]; dsimp
      _ < ∑ p, lineCount L p := by
        obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
        refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
        · simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]
        · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
          obtain ⟨l, _⟩ := @exists_line P L _ _ p
          exact
            let this := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩
  exact lt_irrefl _ this
-- 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
⊢ ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
have obtain : ∀ (f : L → P) (hf1 : Function.Injective f) (hf2 : ∀ (l : L), f l ∉ l),
  ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
Tactic: obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)
-- 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
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), f l ∉ l
⊢ ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
have hf3 : Function.Bijective f
Tactic: have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.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
h : Fintype.card P = Fintype.card L
⊢ ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
have obtain : ∀ (f : L → P) (hf1 : Function.Injective f) (hf2 : ∀ (l : L), f l ∉ l),
  ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
Tactic: classical
    obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)
    have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩
    exact ⟨f, hf3, fun l ↦ (sum_eq_sum_iff_of_le fun l _ ↦ pointCount_le_lineCount (hf2 l)).1
          ((hf3.sum_comp _).trans (sum_lineCount_eq_sum_pointCount P L)).symm _ <| mem_univ _⟩
-- 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
obtain :
  ∀ (f : L → P) (hf1 : Function.Injective f) (hf2 : ∀ (l : L), f l ∉ l),
    ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
⊢ ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
have obtain₁ : ∀ (f : L → P) (hf1 : Function.Injective f) (hf2 : ∀ (l : L), f l ∉ l) (hf3 : Function.Bijective f),
  ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
Tactic: classical
    obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)
    have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩
    exact ⟨f, hf3, fun l ↦ (sum_eq_sum_iff_of_le fun l _ ↦ pointCount_le_lineCount (hf2 l)).1
          ((hf3.sum_comp _).trans (sum_lineCount_eq_sum_pointCount P L)).symm _ <| mem_univ _⟩
-- 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: obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL
-- 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}
⊢ Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
have rw : Eq (α := ℕ) (∑ y : L, ∑ x : P, lineCount L (x, y).1) (∑ x : P, ∑ y : L, pointCount P (x, y).2)
Tactic: rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
-- 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}
⊢ Eq (α := ℕ) (∑ y : L, ∑ x : P, lineCount L (x, y).1) (∑ x : P, ∑ y : L, pointCount P (x, y).2)
have simp_rw : Eq (α := ℕ) (∑ x : L, ∑ x : P, lineCount L x) (∑ x : P, ∑ x : L, pointCount P x)
Tactic: simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
-- 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}
simp_rw simp_rw₁ : Eq (α := ℕ) (∑ x : L, ∑ x : P, lineCount L x) (∑ x : P, ∑ x : L, pointCount P x)
⊢ Eq (α := ℕ) (∑ y : L, ∑ x : P, lineCount L (x, y).1) (∑ x : P, ∑ y : L, pointCount P (x, y).2)
have simp_rw₂ : HSMul.hSMul (β := ℕ) (card.{u_2} (α := L) univ) (∑ x : P, lineCount L x) =
  HSMul.hSMul (β := ℕ) (card.{u_1} (α := P) univ) (∑ x : L, pointCount P x)
Tactic: simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
-- 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}
simp_rw simp_rw₁ : Eq (α := ℕ) (∑ x : L, ∑ x : P, lineCount L x) (∑ x : P, ∑ x : L, pointCount P x)
simp_rw₂ :
  HSMul.hSMul (β := ℕ) (card.{u_2} (α := L) univ) (∑ x : P, lineCount L x) =
    HSMul.hSMul (β := ℕ) (card.{u_1} (α := P) univ) (∑ x : L, pointCount P x)
⊢ Eq (α := ℕ) (∑ y : L, ∑ x : P, lineCount L (x, y).1) (∑ x : P, ∑ y : L, pointCount P (x, y).2)
have simp_rw₃ : HSMul.hSMul (β := ℕ) (Fintype.card L) (∑ x : P, lineCount L x) =
  HSMul.hSMul (β := ℕ) (Fintype.card P) (∑ x : L, pointCount P x)
Tactic: simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
-- 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}
simp_rw simp_rw₁ : Eq (α := ℕ) (∑ x : L, ∑ x : P, lineCount L x) (∑ x : P, ∑ x : L, pointCount P x)
simp_rw₂ :
  HSMul.hSMul (β := ℕ) (card.{u_2} (α := L) univ) (∑ x : P, lineCount L x) =
    HSMul.hSMul (β := ℕ) (card.{u_1} (α := P) univ) (∑ x : L, pointCount P x)
simp_rw₃ :
  HSMul.hSMul (β := ℕ) (Fintype.card L) (∑ x : P, lineCount L x) =
    HSMul.hSMul (β := ℕ) (Fintype.card P) (∑ x : L, pointCount P x)
⊢ Eq (α := ℕ) (∑ y : L, ∑ x : P, lineCount L (x, y).1) (∑ x : P, ∑ y : L, pointCount P (x, y).2)
have simp_rw₄ : HSMul.hSMul (β := ℕ) (Fintype.card L) (∑ x : P, lineCount L x) =
  HSMul.hSMul (β := ℕ) (Fintype.card L) (∑ x : L, pointCount P x)
Tactic: simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
-- 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}
⊢ lineCount L p = pointCount P l
have step1 : Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)
Tactic: 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]
-- 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 (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
have rw : Eq (α := ℕ) (∑ c : P, ∑ a ∈ Set.toFinset {l : L | c ∈ l}, lineCount L (c, a).1) (∑ i ∈ s, pointCount P i.2)
Tactic: rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | 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 : 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 : P, ∑ a ∈ Set.toFinset {l : L | c ∈ l}, lineCount L (c, a).1) (∑ i ∈ s, pointCount P i.2)
⊢ Eq (α := ℕ) (∑ i ∈ s, lineCount L i.1) (∑ i ∈ s, pointCount P i.2)
have h : ∀ (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
Tactic: rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]