awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
hV : U ∈ P.parts
hy : y ∈ U
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
exact Or.inr (Or.inl ⟨U, hU, hx, hy, G.ne_of_adj h⟩)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
pos :
  ∀ (h₂ : G.IsUniform (ε / 8) U V),
    (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
      (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
        ∃ (a : Finset α) (b : Finset α),
          a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
neg :
  ∀ (h₂ : ¬G.IsUniform (ε / 8) U V),
    (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
      (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
        ∃ (a : Finset α) (b : Finset α),
          a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
by_cases h₂ : G.IsUniform (ε / 8) U V

Premises used: HDiv.hDiv, SimpleGraph.IsUniform, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : G.IsUniform (ε / 8) U V
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
Or.inr <| Or.inr ⟨U, V, hU, hV, hUV, h' _ hU _ hV hx hy hUV h₂, hx, hy, h⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : G.IsUniform (ε / 8) U V
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
exact Or.inr <| Or.inr ⟨U, V, hU, hV, hUV, h' _ hU _ hV hx hy hUV h₂, hx, hy, h⟩

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : ¬G.IsUniform (ε / 8) U V
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
Or.inl ⟨U, V, hU, hV, hUV, h₂, hx, hy⟩

Premises used: And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : ¬G.IsUniform (ε / 8) U V
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
exact Or.inl ⟨U, V, hU, hV, hUV, h₂, hx, hy⟩

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
ℓ : ℕ
v w : V
h : v ≠ w
simp : filter (Membership.mem (commonNeighbors ⊥ v w)) univ = ∅
⊢ ¬Adj ⊥ v w → Fintype.card.{u} (↑(commonNeighbors ⊥ v w) : Type u) = 0

Tactic:
simp only [card_eq_zero, Fintype.card_ofFinset, forall_true_left, not_false_iff, bot_adj]

Premises used: Fintype.card_ofFinset, forall_true_left, SimpleGraph.bot_adj, Finset.card_eq_zero, not_false_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
ℓ : ℕ
v w : V
h_1 : v ≠ w
h : ∀ (a : V), a ∈ filter (Membership.mem (commonNeighbors ⊥ v w)) univ ↔ Membership.mem (γ := Finset V) ∅ a
⊢ filter (Membership.mem (commonNeighbors ⊥ v w)) univ = ∅

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
ℓ : ℕ
v w : V
h : v ≠ w
a : V
⊢ a ∈ filter (Membership.mem (commonNeighbors ⊥ v w)) univ ↔ Membership.mem (γ := Finset V) ∅ a

Tactic:
simp [mem_commonNeighbors]

Premises used: SimpleGraph.mem_commonNeighbors
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
a₁ : 2 ≤ G.ediam
⊢ G.ediam = 2

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 : ∀ (u v : V), G.edist u v ≤ 2
⊢ G.ediam ≤ 2

Tactic:
rw [ediam_le_iff]

Premises used: SimpleGraph.ediam_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
a : ∀ (hc : 2 < G.edist u v), False
⊢ G.edist u v ≤ 2

Tactic:
by_contra! hc
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
⊢ u ≠ v

Tactic:
obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc

Premises used: Iff.mp, SimpleGraph.two_lt_edist_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
⊢ ¬G.Adj u v

Tactic:
obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc

Premises used: Iff.mp, SimpleGraph.two_lt_edist_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
⊢ G.commonNeighbors u v = ∅

Tactic:
obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc

Premises used: Iff.mp, SimpleGraph.two_lt_edist_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 = ∅
⊢ Fintype.card.{u} (↑(G.commonNeighbors u v) : Type u) = μ

Tactic:
have h := h.of_not_adj hn ha
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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) = μ
⊢ 0 = μ

Tactic:
simp_rw [he, Fintype.card_eq_zero] at h

Premises used: Fintype.card_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 : 0 = μ
⊢ False

Tactic:
false_of_ne (h ▸ hm)

Premises used: false_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 : 0 = μ
⊢ False

Tactic:
exact false_of_ne (h ▸ hm)

Premises used: false_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 : ∀ (hc : G.ediam < 2), False
⊢ 2 ≤ G.ediam

Tactic:
by_contra! hc
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
⊢ Subsingleton V

Tactic:
rw [ediam_eq_zero_iff_subsingleton] at hc

Premises used: SimpleGraph.ediam_eq_zero_iff_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 : Subsingleton V
⊢ False

Tactic:
false_of_nontrivial_of_subsingleton V

Premises used: false_of_nontrivial_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 : Subsingleton V
⊢ False

Tactic:
exact false_of_nontrivial_of_subsingleton V

Premises used: false_of_nontrivial_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 = 1
⊢ False

Tactic:
ht.elim (ediam_eq_one.mp hc)

Premises used: SimpleGraph.ediam_eq_one, Iff.mp, Ne.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 = 1
⊢ False

Tactic:
exact ht.elim (ediam_eq_one.mp hc)

Premises used: SimpleGraph.ediam_eq_one, Iff.mp, Ne.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
⊢ 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)

Premises used: SimpleGraph.ediam_eq_zero_iff_subsingleton, Iff.mp, ENat.le_one_iff_eq_zero_or_eq_one, Order.le_of_lt_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 ℓ μ
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)
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)

Tactic:
apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))

Premises used: Nat.add_right_cancel
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
rw₁ : Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) ≤ 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)

Tactic:
rw [Nat.sub_add_cancel, ← Set.toFinset_card]

Premises used: Set.toFinset_card, Nat.sub_add_cancel
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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) + #(G.commonNeighbors v w).toFinset = 2 * k

Tactic:
simp [commonNeighbors, ← neighborFinset_def, Finset.card_union_add_card_inter,
      h.regular.degree_eq, two_mul]

Premises used: two_mul, SimpleGraph.commonNeighbors, SimpleGraph.IsSRGWith.regular, Finset.card_union_add_card_inter, SimpleGraph.IsRegularOfDegree.degree_eq, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 ℓ μ
apply : G.degree v ≤ 2 * k
⊢ Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u) ≤ 2 * k

Tactic:
apply le_trans (card_commonNeighbors_le_degree_left _ _ _)

Premises used: SimpleGraph.card_commonNeighbors_le_degree_left, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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.degree v ≤ 2 * k

Tactic:
simp [h.regular.degree_eq, two_mul]

Premises used: two_mul, SimpleGraph.IsSRGWith.regular, SimpleGraph.IsRegularOfDegree.degree_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
rw : #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - μ

Tactic:
rw [← h.of_not_adj hne ha]

Premises used: SimpleGraph.IsSRGWith.of_not_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)

Tactic:
h.card_neighborFinset_union_eq

Premises used: SimpleGraph.IsSRGWith.card_neighborFinset_union_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)

Tactic:
exact h.card_neighborFinset_union_eq

Premises used: SimpleGraph.IsSRGWith.card_neighborFinset_union_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
rw : #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - ℓ

Tactic:
rw [← h.of_adj v w ha]

Premises used: SimpleGraph.IsSRGWith.of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)

Tactic:
h.card_neighborFinset_union_eq

Premises used: SimpleGraph.IsSRGWith.card_neighborFinset_union_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 - Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)

Tactic:
exact h.card_neighborFinset_union_eq

Premises used: SimpleGraph.IsSRGWith.card_neighborFinset_union_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v w : V
⊢ (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) =
    ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v w : V
h : G.Adj v w
⊢ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) = (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Tactic:
simpa using ⟨h, adj_symm _ h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 ℓ μ
rw : Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)
⊢ Gᶜ.IsRegularOfDegree (n - k - 1)

Tactic:
rw [← h.card, Nat.sub_sub, add_comm, ← Nat.sub_sub]

Premises used: SimpleGraph.IsSRGWith.card, Nat.sub_sub, add_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 (Fintype.card V - 1 - k)

Tactic:
h.regular.compl

Premises used: SimpleGraph.IsRegularOfDegree.compl, SimpleGraph.IsSRGWith.regular
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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 (Fintype.card V - 1 - k)

Tactic:
exact h.regular.compl

Premises used: SimpleGraph.IsRegularOfDegree.compl, SimpleGraph.IsSRGWith.regular
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
simp : #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2
⊢ Fintype.card.{u} (↑(Gᶜ.commonNeighbors v w) : Type u) = 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]

Premises used: Set.toFinset_compl, Set.toFinset_diff, SimpleGraph.neighborSet_compl, SimpleGraph.commonNeighbors, Set.toFinset_card, Set.toFinset_singleton, Set.toFinset_inter, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
simp_rw : #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2

Tactic:
simp_rw [compl_neighborFinset_sdiff_inter_eq]

Premises used: SimpleGraph.compl_neighborFinset_sdiff_inter_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
⊢ v ≠ w

Tactic:
have hne : v ≠ w := ne_of_adj _ ha
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
⊢ v ≠ w ∧ ¬G.Adj v w

Tactic:
rw [compl_adj] at ha

Premises used: SimpleGraph.compl_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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
ha₁ : v ≠ w ∧ ¬G.Adj v w
⊢ v ≠ w

Tactic:
rw [compl_adj] at ha

Premises used: SimpleGraph.compl_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
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}
rw₂ : {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Tactic:
rw [card_sdiff_of_subset, ← insert_eq, card_insert_of_notMem, card_singleton,
    ← Finset.compl_union]

Premises used: Finset.insert_eq, Finset.compl_union, Finset.card_sdiff_of_subset, Finset.card_insert_of_notMem, Finset.card_singleton