awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Configuration
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_2 : Nonempty.{u_2 + 1} { l : L // p ∈ l }
⊢ 0 < lineCount L p

Tactic:
rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]

Premises used: Configuration.lineCount, Fintype.card_pos_iff, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.Configuration
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_2 : ∀ (l : L), p ∉ l → Nonempty.{u_2 + 1} { l : L // p ∈ l }
⊢ Nonempty.{u_2 + 1} { l : L // p ∈ l }

Tactic:
obtain ⟨l, _⟩ := @exists_line P L _ _ p

Premises used: Configuration.Nondegenerate.exists_line
-- Module: Mathlib.Combinatorics.Configuration
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
l : L
h : p ∉ l
⊢ Nonempty.{u_2 + 1} { l : L // p ∈ l }

Tactic:
let this := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩

Premises used: not_exists, Configuration.HasLines.mkLine_ax, Nonempty.intro, Configuration.HasLines.mkLine, Subtype.mk, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.Configuration
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
l : L
h : p ∉ l
⊢ Nonempty.{u_2 + 1} { l : L // p ∈ l }

Tactic:
exact
            let this := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩

Premises used: not_exists, Iff.mp
-- Module: Mathlib.Combinatorics.Configuration
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 : 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⟩⟩
-- Module: Mathlib.Combinatorics.Configuration
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
this : LT.lt (α := ℕ) (∑ p : P, lineCount L p) (∑ p : P, lineCount L p)
⊢ False

Tactic:
lt_irrefl _ this

Premises used: lt_irrefl
-- Module: Mathlib.Combinatorics.Configuration
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
this : LT.lt (α := ℕ) (∑ p : P, lineCount L p) (∑ p : P, lineCount L p)
⊢ False

Tactic:
exact lt_irrefl _ this

Premises used: lt_irrefl
-- Module: Mathlib.Combinatorics.Configuration
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
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
⊢ Fintype.card P ≤ Fintype.card L

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
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasPoints P L
inst_2 : Fintype P
inst_3 : Fintype L
⊢ Fintype.card L ≤ Fintype.card P

Tactic:
@HasLines.card_le (Dual L) (Dual P) _ _ _ _

Premises used: Configuration.Dual, Configuration.HasLines.card_le
-- Module: Mathlib.Combinatorics.Configuration
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)

Tactic:
obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)

Premises used: Configuration.Nondegenerate.exists_injective_of_card_le, ge_of_eq
-- Module: Mathlib.Combinatorics.Configuration
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
⊢ Function.Bijective f

Tactic:
have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩
-- Module: Mathlib.Combinatorics.Configuration
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
hf3 : Function.Bijective f
⊢ ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Tactic:
⟨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 _⟩

Premises used: Finset.mem_univ, Function.Bijective.sum_comp, Configuration.lineCount, Finset.sum_eq_sum_iff_of_le, Configuration.HasLines.pointCount_le_lineCount, Configuration.sum_lineCount_eq_sum_pointCount, And.intro, Exists.intro, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.Configuration
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
hf3 : Function.Bijective f
⊢ ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Tactic:
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 _⟩
-- Module: Mathlib.Combinatorics.Configuration
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)
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)
⊢ ∃ (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 _⟩

Premises used: Configuration.Nondegenerate.exists_injective_of_card_le, ge_of_eq
-- Module: Mathlib.Combinatorics.Configuration
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
⊢ lineCount L p = pointCount P l

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

Premises used: Configuration.HasLines.exists_bijective_of_card_eq
-- Module: Mathlib.Combinatorics.Configuration
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}
rw : Eq (α := ℕ) (∑ y : L, ∑ x : P, lineCount L (x, y).1) (∑ x : P, ∑ y : L, pointCount P (x, y).2)
⊢ Eq (α := ℕ) (∑ i : P × L, lineCount L i.1) (∑ i : P × L, pointCount P i.2)

Tactic:
rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]

Premises used: Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product
-- Module: Mathlib.Combinatorics.Configuration
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)
simp_rw₄ :
  HSMul.hSMul (β := ℕ) (Fintype.card L) (∑ x : P, lineCount L x) =
    HSMul.hSMul (β := ℕ) (Fintype.card L) (∑ x : L, pointCount P x)
⊢ Eq (α := ℕ) (∑ 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]

Premises used: Finset.card_univ, Configuration.sum_lineCount_eq_sum_pointCount, Finset.sum_const
-- Module: Mathlib.Combinatorics.Configuration
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)

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]
-- Module: Mathlib.Combinatorics.Configuration
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)
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
⊢ Eq (α := ℕ) (∑ 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 }]

Premises used: Finset.univ, setOf, Membership.mem, Finset.sum_finset_product, Set.toFinset
-- Module: Mathlib.Combinatorics.Configuration
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)
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
⊢ 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_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]

Premises used: Finset.univ, setOf, Membership.mem, Set.toFinset, eq_comm, Finset.sum_finset_product_right
-- Module: Mathlib.Combinatorics.Configuration
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)
⊢ ∀ (i : L), Membership.mem (γ := Finset L) univ i ↔ Membership.mem (γ := Finset P) univ (f i)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Configuration
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)
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)
⊢ 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:
refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_

Premises used: Finset.sum_bijective
-- Module: Mathlib.Combinatorics.Configuration
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
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)
⊢ 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)

Tactic:
simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]

Premises used: Set.toFinset_card, Nat.card_eq_fintype_card, Finset.sum_const
-- Module: Mathlib.Combinatorics.Configuration
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
change : pointCount P l • lineCount L (f l) = lineCount L (f l) • lineCount L (f 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)

Tactic:
change pointCount P l • _ = lineCount L (f l) • _

Premises used: Configuration.lineCount, Configuration.pointCount
-- Module: Mathlib.Combinatorics.Configuration
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
rw rw₁ : lineCount L (f l) • lineCount L (f l) = lineCount L (f l) • lineCount L (f l)
⊢ pointCount P l • lineCount L (f l) = lineCount L (f l) • lineCount L (f l)

Tactic:
rw [hf2]
-- Module: Mathlib.Combinatorics.Configuration
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)
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
⊢ Eq (α := ℕ) (∑ c : P, ∑ a ∈ Set.toFinset {l : L | c ∈ l}, lineCount L (c, a).1) (∑ i ∈ s, pointCount P i.2)

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]

Premises used: Finset.univ, setOf, Configuration.lineCount, Membership.mem, Set.toFinset_card, Set.toFinset, eq_comm, Finset.sum_bijective, Configuration.pointCount, Finset.sum_finset_product_right, Nat.card_eq_fintype_card, Finset.sum_const
-- Module: Mathlib.Combinatorics.Configuration
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)
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
⊢ ∀ (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:
simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]

Premises used: Finset.mem_univ, Set.mem_toFinset, true_and
-- Module: Mathlib.Combinatorics.Configuration
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),
    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:
fun p => Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Combinatorics.Configuration
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),
    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:
exact fun p => Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Configuration
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)
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
⊢ ∀ (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:
simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]

Premises used: Finset.mem_univ, Set.mem_toFinset, true_and
-- Module: Mathlib.Combinatorics.Configuration
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),
    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:
fun p => Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Combinatorics.Configuration
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),
    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:
exact fun p => Iff.rfl

Premises used: Iff.rfl