awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
ℓ : ℕ
v w : V
h : v ≠ w
⊢ (fun (v w : V) ↦ ¬Adj ⊥ v w → Fintype.card.{u} (↑(commonNeighbors ⊥ v w) : Type u) = 0) v w
have simp : filter (Membership.mem (commonNeighbors ⊥ v w)) univ = ∅
Tactic: simp only [card_eq_zero, Fintype.card_ofFinset, forall_true_left, not_false_iff, bot_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
ℓ : ℕ
v w : V
h : v ≠ w
⊢ filter (Membership.mem (commonNeighbors ⊥ v w)) univ = ∅
have h : ∀ (a : V), a ∈ filter (Membership.mem (commonNeighbors ⊥ v w)) univ ↔ Membership.mem (γ := Finset V) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ G.ediam = 2
have a : G.ediam ≤ 2
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
a : G.ediam ≤ 2
⊢ G.ediam = 2
have a₁ : 2 ≤ G.ediam
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ G.ediam ≤ 2
have a : ∀ (u v : V), G.edist u v ≤ 2
Tactic: rw [ediam_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u v : V
⊢ G.edist u v ≤ 2
have a : ∀ (hc : 2 < G.edist u v), False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u v : V
hc : 2 < G.edist u v
⊢ False
have hn : u ≠ v
Tactic: obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u v : V
hc : 2 < G.edist u v
hn : u ≠ v
⊢ False
have ha : ¬G.Adj u v
Tactic: obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u v : V
hc : 2 < G.edist u v
hn : u ≠ v
ha : ¬G.Adj u v
⊢ False
have he : G.commonNeighbors u v = ∅
Tactic: obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u v : V
hc : 2 < G.edist u v
hn : u ≠ v
ha : ¬G.Adj u v
he : G.commonNeighbors u v = ∅
⊢ False
have h₁ : Fintype.card.{u} (↑(G.commonNeighbors u v) : Type u) = μ
Tactic: have h := h.of_not_adj hn ha
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h_1 : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u v : V
hc : 2 < G.edist u v
hn : u ≠ v
ha : ¬G.Adj u v
he : G.commonNeighbors u v = ∅
h : Fintype.card.{u} (↑(G.commonNeighbors u v) : Type u) = μ
⊢ False
have h₁ : 0 = μ
Tactic: simp_rw [he, Fintype.card_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ 2 ≤ G.ediam
have a : ∀ (hc : G.ediam < 2), False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
hc_1 : G.ediam < 2
hc : G.ediam = 0
⊢ False
have hc₁ : Subsingleton V
Tactic: rw [ediam_eq_zero_iff_subsingleton] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
hc : G.ediam < 2
⊢ False
have x : G.ediam = 0 ∨ G.ediam = 1
Tactic: cases ENat.le_one_iff_eq_zero_or_eq_one.mp (Order.le_of_lt_succ hc) with
    | inl hc =>
      rw [ediam_eq_zero_iff_subsingleton] at hc
      exact false_of_nontrivial_of_subsingleton V
    | inr hc => exact ht.elim (ediam_eq_one.mp hc)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)
have apply : #(G.neighborFinset v ∪ G.neighborFinset w) + Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) =
  2 * k - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) + Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)
Tactic: apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) =
    2 * k - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) + Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)
have rw : #(G.neighborFinset v ∪ G.neighborFinset w) + #(G.commonNeighbors v w).toFinset = 2 * k
Tactic: rw [Nat.sub_add_cancel, ← Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
rw : #(G.neighborFinset v ∪ G.neighborFinset w) + #(G.commonNeighbors v w).toFinset = 2 * k
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) =
    2 * k - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) + Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)
have rw₁ : Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) ≤ 2 * k
Tactic: rw [Nat.sub_add_cancel, ← Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) ≤ 2 * k
have apply : G.degree v ≤ 2 * k
Tactic: apply le_trans (card_commonNeighbors_le_degree_left _ _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
hne : v ≠ w
ha : ¬G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - μ
have rw : #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)
Tactic: rw [← h.of_not_adj hne ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
ha : G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - ℓ
have rw : #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)
Tactic: rw [← h.of_adj v w ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
⊢ Gᶜ.IsRegularOfDegree (n - k - 1)
have rw : Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)
Tactic: rw [← h.card, Nat.sub_sub, add_comm, ← Nat.sub_sub]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ Fintype.card.{u} (↑(Gᶜ.commonNeighbors v w) : Type u) = n - (2 * k - μ) - 2
have simp : #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2
Tactic: simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl,
    Set.toFinset_diff, Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2
have simp_rw : #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
Tactic: simp_rw [compl_neighborFinset_sdiff_inter_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
have hne : v ≠ w
Tactic: have hne : v ≠ w := ne_of_adj _ ha
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
have ha₁ : v ≠ w ∧ ¬G.Adj v w
Tactic: rw [compl_adj] at ha
Cleared hypotheses: ha, hne
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
have rw : #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
Tactic: rw [card_sdiff_of_subset, ← insert_eq, card_insert_of_notMem, card_singleton,
    ← Finset.compl_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
rw : #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
have rw₁ : w ∉ {v}
Tactic: rw [card_sdiff_of_subset, ← insert_eq, card_insert_of_notMem, card_singleton,
    ← Finset.compl_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
rw : #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
rw₁ : w ∉ {v}
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
have rw₂ : {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
Tactic: rw [card_sdiff_of_subset, ← insert_eq, card_insert_of_notMem, card_singleton,
    ← Finset.compl_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
have rw : Fintype.card V - #(G.neighborFinset v ∪ G.neighborFinset w) - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
Tactic: rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
rw : Fintype.card V - #(G.neighborFinset v ∪ G.neighborFinset w) - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
⊢ #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
have rw₁ : Fintype.card V - (2 * k - μ) - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
Tactic: rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
rw : Fintype.card V - #(G.neighborFinset v ∪ G.neighborFinset w) - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
rw₁ : Fintype.card V - (2 * k - μ) - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
⊢ #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
have rw₂ : Fintype.card V - (2 * k - μ) - HAdd.hAdd (α := ℕ) 1 1 = Fintype.card V - (2 * k - μ) - 2
Tactic: rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
u : V
⊢ Membership.mem (γ := Finset V) ({w} ∪ {v}) u → u ∈ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
have simp : u = w ∨ u = v → ¬G.Adj v u ∧ ¬G.Adj w u
Tactic: simp only [mem_union, mem_compl, mem_neighborFinset, mem_inter, mem_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Gᶜ.Adj v w
⊢ Fintype.card.{u} (↑(Gᶜ.commonNeighbors v w) : Type u) = n - (2 * k - ℓ)
have simp : #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)
Tactic: simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl,
    Set.toFinset_diff, Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)
have hna₁ : v ≠ w → G.Adj v w
Tactic: simp only [not_and, Classical.not_not, compl_adj] at hna
Cleared hypotheses: hna
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)
have h2' : G.Adj v w
Tactic: have h2' := hna hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)
have simp_rw : #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) = n - (2 * k - ℓ)
Tactic: simp_rw [compl_neighborFinset_sdiff_inter_eq, sdiff_compl_neighborFinset_inter_eq h2']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) = n - (2 * k - ℓ)
have rwa : #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ = n - (2 * k - ℓ)
Tactic: rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
rwa : #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ = n - (2 * k - ℓ)
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) = n - (2 * k - ℓ)
have rwa₁ : Fintype.card V - #(G.neighborFinset v ∪ G.neighborFinset w) = n - (2 * k - ℓ)
Tactic: rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
rwa : #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ = n - (2 * k - ℓ)
rwa₁ : Fintype.card V - #(G.neighborFinset v ∪ G.neighborFinset w) = n - (2 * k - ℓ)
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) = n - (2 * k - ℓ)
have rwa₂ : Fintype.card V - (2 * k - ℓ) = n - (2 * k - ℓ)
Tactic: rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
rwa : #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ = n - (2 * k - ℓ)
rwa₁ : Fintype.card V - #(G.neighborFinset v ∪ G.neighborFinset w) = n - (2 * k - ℓ)
rwa₂ : Fintype.card V - (2 * k - ℓ) = n - (2 * k - ℓ)
rwa₃ : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) = n - (2 * k - ℓ)
have rwa₄ : Fintype.card V - (2 * k - ℓ) = Fintype.card V - (2 * k - ℓ)
Tactic: rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
hn : 0 < n
this : DecidableEq V := Classical.decEq V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
have hn₁ : Nonempty V
Tactic: rw [← h.card, Fintype.card_pos_iff] at hn
Cleared hypotheses: hn, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
hn : Nonempty V
this : DecidableEq V := Classical.decEq V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
have obtain : ∀ (v : V), k * (k - ℓ - 1) = (n - k - 1) * μ
Tactic: obtain ⟨v⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
have h₁ : k = #(G.neighborFinset v)
Tactic: convert! card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
h₁ : k = #(G.neighborFinset v)
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
have h₂ : n - k - 1 = #(Gᶜ.neighborFinset v)
Tactic: convert! card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
h₁ : k = #(G.neighborFinset v)
h₂ : n - k - 1 = #(Gᶜ.neighborFinset v)
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
have convert_3 : ∀ a ∈ G.neighborFinset v, #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) a) = k - ℓ - 1
Tactic: convert! card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
h₁ : k = #(G.neighborFinset v)
h₂ : n - k - 1 = #(Gᶜ.neighborFinset v)
convert_3 : ∀ a ∈ G.neighborFinset v, #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) a) = k - ℓ - 1
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
have convert_4 : ∀ b ∈ Gᶜ.neighborFinset v, #(bipartiteBelow G.Adj (G.neighborFinset v) b) = μ
Tactic: convert! card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : w ∈ G.neighborFinset v
⊢ #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) w) = k - ℓ - 1
have hw₁ : G.Adj v w
Tactic: rw [mem_neighborFinset] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
⊢ #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) w) = k - ℓ - 1
have convert_3 : #(Gᶜ.neighborFinset v ∩ G.neighborFinset w) = k - ℓ - 1
Tactic: simp_rw [bipartiteAbove, ← mem_neighborFinset, filter_mem_eq_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
⊢ {v} ⊆ G.neighborFinset w \ G.neighborFinset v
have rw : G.Adj w v ∧ v ∉ G.neighborFinset v
Tactic: rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
⊢ #(Gᶜ.neighborFinset v ∩ G.neighborFinset w) = k - ℓ - 1
have s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
Tactic: have s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v := by
      rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
      exact ⟨hw.symm, G.notMem_neighborFinset_self v⟩