-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem circulantGraph_eq_erase_zero : circulantGraph s = circulantGraph (s \ {0})

Proof state:
case Adj.h.h.a.mp.inl
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩

Result:
no goals

Proof state:
case Adj.h.h.a.mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s ∨ v - u ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
cases h1 with
  | inl h1 => exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩
  | inr h1 => exact Or.inr ⟨h1, sub_ne_zero_of_ne h.symm⟩

Result:
no goals

Proof state:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ u ≠ v → (u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0})

Tactic:
intro (h : u ≠ v)

Result:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Proof state:
case Adj.h.h.a.mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0} → u - v ∈ s ∨ v - u ∈ s

Tactic:
intro h1

Result:
case Adj.h.h.a.mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
⊢ u - v ∈ s ∨ v - u ∈ s

Proof state:
case Adj.h.h.a.mp.inr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : v - u ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
exact Or.inr ⟨h1, sub_ne_zero_of_ne h.symm⟩

Result:
no goals

Proof state:
case Adj.h.h.a.mpr.inl
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s \ {0}
⊢ u - v ∈ s ∨ v - u ∈ s

Tactic:
exact Or.inl h1.left

Result:
no goals

Proof state:
case Adj.h.h.a.mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
⊢ u - v ∈ s ∨ v - u ∈ s

Tactic:
cases h1 with
  | inl h1 => exact Or.inl h1.left
  | inr h1 => exact Or.inr h1.left

Result:
no goals

Proof state:
case Adj.h.h.a.mpr.inr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : v - u ∈ s \ {0}
⊢ u - v ∈ s ∨ v - u ∈ s

Tactic:
exact Or.inr h1.left

Result:
no goals

Proof state:
G : Type u_1
inst✝ : AddGroup G
s : Set G
⊢ circulantGraph s = circulantGraph (s \ {0})

Tactic:
ext (u v : G)

Result:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ (circulantGraph s).Adj u v ↔ (circulantGraph (s \ {0})).Adj u v

Proof state:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
apply Iff.intro

Result:
case Adj.h.h.a.mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s ∨ v - u ∈ s → u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

case Adj.h.h.a.mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0} → u - v ∈ s ∨ v - u ∈ s

Proof state:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ (circulantGraph s).Adj u v ↔ (circulantGraph (s \ {0})).Adj u v

Tactic:
simp only [circulantGraph, fromRel_adj, and_congr_right_iff]

Result:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ u ≠ v → (u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0})

Proof state:
case Adj.h.h.a.mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s ∨ v - u ∈ s → u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
intro h1

Result:
case Adj.h.h.a.mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s ∨ v - u ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}