awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
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⟩

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s ∨ v - u ∈ s
Adj : ∀ (h1 : u - v ∈ s), u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
Adj₁ : ∀ (h1 : v - u ∈ s), u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
⊢ 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⟩

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
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:
Or.inl h1.left

Premises used: And.left, Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
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

Premises used: And.left, Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
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:
Or.inr h1.left

Premises used: And.left, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
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

Premises used: And.left, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
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}
Adj : ∀ (h1 : u - v ∈ s \ {0}), u - v ∈ s ∨ v - u ∈ s
Adj₁ : ∀ (h1 : v - u ∈ s \ {0}), u - v ∈ s ∨ v - u ∈ s
⊢ u - v ∈ s ∨ v - u ∈ s

Tactic:
cases h1 with
      | inl h1 => exact Or.inl h1.left
      | inr h1 => exact Or.inr h1.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
Adj : ∀ (x x_1 : G), (circulantGraph s).Adj x x_1 ↔ (circulantGraph (s ∪ -s)).Adj x x_1
⊢ circulantGraph s = circulantGraph (s ∪ -s)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
x x_1 : G
Adj : ¬x = x_1 ∧ (x - x_1 ∈ s ∨ x_1 - x ∈ s) ↔ ¬x = x_1 ∧ ((x - x_1 ∈ s ∨ x_1 - x ∈ s) ∨ x_1 - x ∈ s ∨ x - x_1 ∈ s)
⊢ (circulantGraph s).Adj x x_1 ↔ (circulantGraph (s ∪ -s)).Adj x x_1

Tactic:
simp only [circulantGraph_adj, Set.mem_union, Set.mem_neg, neg_sub]

Premises used: Set.mem_union, Set.mem_neg, neg_sub, SimpleGraph.circulantGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
x x_1 : G
⊢ ¬x = x_1 ∧ (x - x_1 ∈ s ∨ x_1 - x ∈ s) ↔ ¬x = x_1 ∧ ((x - x_1 ∈ s ∨ x_1 - x ∈ s) ∨ x_1 - x ∈ s ∨ x - x_1 ∈ s)

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v d : G
⊢ (circulantGraph s).Adj (u + d) (v + d) ↔ (circulantGraph s).Adj u v

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
n : ℕ
x : Fin (n + 2)
h : x - x = 1 ∨ x - x = 1
⊢ x - x = 1 → False

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
n : ℕ
⊢ DecidableRel (α := Fin (n + 2))
    (Adj
      (match (motive := (x : ℕ) → SimpleGraph (Fin x)) n + 2 with
      | 0 => ⊥
      | 1 => ⊥
      | n.succ.succ => { Adj := fun (a b : Fin (n + 2)) ↦ a - b = 1 ∨ b - a = 1, symm := ⋯, loopless := ⋯ }))

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
zero : Eq (α := SimpleGraph (Fin (HAdd.hAdd (α := ℕ) 0 1))) (cycleGraph (HAdd.hAdd (α := ℕ) 0 1)) (circulantGraph {1})
succ : ∀ (n : ℕ), Eq (α := SimpleGraph (Fin (n + 1 + 1))) (cycleGraph (n + 1 + 1)) (circulantGraph {1})
⊢ Eq (α := SimpleGraph (Fin (n + 1))) (cycleGraph (n + 1)) (circulantGraph {1})

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
⊢ Eq (α := SimpleGraph (Fin (HAdd.hAdd (α := ℕ) 0 1))) (cycleGraph (HAdd.hAdd (α := ℕ) 0 1)) (circulantGraph {1})

Tactic:
edgeFinset_inj.mp rfl

Premises used: SimpleGraph.edgeFinset_inj, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
⊢ Eq (α := SimpleGraph (Fin (HAdd.hAdd (α := ℕ) 0 1))) (cycleGraph (HAdd.hAdd (α := ℕ) 0 1)) (circulantGraph {1})

Tactic:
exact edgeFinset_inj.mp rfl

Premises used: SimpleGraph.edgeFinset_inj, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
⊢ Eq (α := SimpleGraph (Fin (n + 1 + 1))) (cycleGraph (n + 1 + 1)) (circulantGraph {1})

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
u v : Fin 0
⊢ ¬Adj (cycleGraph 0) u v

Tactic:
id

Premises used: id, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
⊢ Eq (α := SimpleGraph (Fin 0)) (cycleGraph 0) ⊥

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
⊢ Eq (α := SimpleGraph (Fin 1)) (cycleGraph 1) ⊥

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
⊢ Eq (α := SimpleGraph (Fin 0)) (cycleGraph 0) ⊤

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
⊢ Eq (α := SimpleGraph (Fin 1)) (cycleGraph 1) ⊤

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
simp : ∀ (x x_1 : Fin 2), Adj (cycleGraph 2) x x_1 = Adj ⊤ x x_1
⊢ Eq (α := SimpleGraph (Fin 2)) (cycleGraph 2) ⊤

Tactic:
simp only [SimpleGraph.ext_iff, funext_iff]

Premises used: funext_iff, SimpleGraph.ext_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
⊢ ∀ (x x_1 : Fin 2), Adj (cycleGraph 2) x x_1 = Adj ⊤ x x_1

Tactic:
decide
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
simp : ∀ (x x_1 : Fin 3), Adj (cycleGraph 3) x x_1 = Adj ⊤ x x_1
⊢ Eq (α := SimpleGraph (Fin 3)) (cycleGraph 3) ⊤

Tactic:
simp only [SimpleGraph.ext_iff, funext_iff]

Premises used: funext_iff, SimpleGraph.ext_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
⊢ ∀ (x x_1 : Fin 3), Adj (cycleGraph 3) x x_1 = Adj ⊤ x x_1

Tactic:
decide
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
u v : Fin 1
⊢ ¬Adj (cycleGraph 1) u v

Tactic:
simp [cycleGraph_one_eq_bot]

Premises used: SimpleGraph.cycleGraph_one_eq_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
u v : Fin (n + 2)
⊢ Adj (cycleGraph (n + 2)) u v ↔ u - v = 1 ∨ v - u = 1

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
u v : Fin 0
⊢ Adj (cycleGraph 0) u v ↔ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1

Tactic:
u.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
u v : Fin 0
⊢ Adj (cycleGraph 0) u v ↔ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1

Tactic:
exact u.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
u v : Fin 1
⊢ Adj (cycleGraph 1) u v ↔ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1

Tactic:
simp [cycleGraph_one_adj]

Premises used: SimpleGraph.cycleGraph_one_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
⊢ Adj (cycleGraph (n + 2)) u v ↔ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1

Tactic:
simp [cycleGraph_adj, Fin.ext_iff]

Premises used: Fin.ext_iff, SimpleGraph.cycleGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
u v : Fin n
⊢ (cycleGraph n).Adj u v ↔ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1

Tactic:
match n with
  | 0 => exact u.elim0
  | 1 => simp [cycleGraph_one_adj]
  | n + 2 => simp [cycleGraph_adj, Fin.ext_iff]
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
v : Fin (n + 2)
h :
  ∀ (w : Fin (n + 2)), w ∈ neighborSet (cycleGraph (n + 2)) v ↔ Membership.mem (γ := Set (Fin (n + 2))) {v - 1, v + 1} w
⊢ neighborSet (cycleGraph (n + 2)) v = {v - 1, v + 1}

Tactic:
ext w
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
v w : Fin (n + 2)
h : v - w = 1 ∨ w - v = 1 ↔ w = v - 1 ∨ w = v + 1
h₁ : v = w + 1 ∨ w - v = 1 ↔ w = v - 1 ∨ w = v + 1
h₂ : v = w + 1 ∨ w = v + 1 ↔ w = v - 1 ∨ w = v + 1
h₃ : v = w + 1 ∨ w = v + 1 ↔ w + 1 = v ∨ w = v + 1
h₄ h₅ : w + 1 = v ∨ w = v + 1 ↔ w + 1 = v ∨ w = v + 1
⊢ Adj (cycleGraph (n + 2)) v w ↔ w = v - 1 ∨ w = v + 1

Tactic:
rw [cycleGraph_adj, sub_eq_iff_eq_add', sub_eq_iff_eq_add', eq_sub_iff_add_eq, eq_comm]

Premises used: eq_sub_iff_add_eq, eq_comm, SimpleGraph.cycleGraph_adj, sub_eq_iff_eq_add'
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
v : Fin (n + 2)
⊢ neighborFinset (cycleGraph (n + 2)) v = {v - 1, v + 1}

Tactic:
simp [neighborFinset, cycleGraph_neighborSet]

Premises used: SimpleGraph.neighborFinset, SimpleGraph.cycleGraph_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
v : Fin (n + 2)
rw : (neighborFinset (cycleGraph (n + 2)) v).card = Finset.card (α := Fin (n + 2)) {v - 1, v + 1}
rw₁ rw₂ : Finset.card (α := Fin (n + 2)) {v - 1, v + 1} = Finset.card (α := Fin (n + 2)) {v - 1, v + 1}
⊢ degree (cycleGraph (n + 2)) v = Finset.card (α := Fin (n + 2)) {v - 1, v + 1}

Tactic:
rw [SimpleGraph.degree, cycleGraph_neighborFinset]

Premises used: SimpleGraph.cycleGraph_neighborFinset, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
v : Fin (n + 3)
rw : v - 1 ≠ v + 1
⊢ degree (cycleGraph (n + 3)) v = 2

Tactic:
rw [cycleGraph_degree_two_le, Finset.card_pair]

Premises used: Finset.card_pair, SimpleGraph.cycleGraph_degree_two_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
v : Fin (n + 3)
simp : ¬HAdd.hAdd (α := Fin (n + 3)) 1 1 = 0
⊢ v - 1 ≠ v + 1

Tactic:
simp only [ne_eq, sub_eq_iff_eq_add, add_assoc v, left_eq_add]

Premises used: left_eq_add, add_assoc, ne_eq, sub_eq_iff_eq_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
v : Fin (n + 3)
⊢ ¬HAdd.hAdd (α := Fin (n + 3)) 1 1 = 0

Tactic:
ne_of_beq_false rfl

Premises used: ne_of_beq_false, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
v : Fin (n + 3)
⊢ ¬HAdd.hAdd (α := Fin (n + 3)) 1 1 = 0

Tactic:
exact ne_of_beq_false rfl

Premises used: ne_of_beq_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
⊢ LE.le (α := SimpleGraph (Fin 0)) (pathGraph 0) (cycleGraph 0)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
⊢ LE.le (α := SimpleGraph (Fin 1)) (pathGraph 1) (cycleGraph 1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
h : Adj (pathGraph (n + 2)) u v
⊢ (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ)

Tactic:
rw [pathGraph_adj] at h

Premises used: SimpleGraph.pathGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
h : (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ)
rw : (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1
⊢ Adj (cycleGraph (n + 2)) u v

Tactic:
rw [cycleGraph_adj']

Premises used: SimpleGraph.cycleGraph_adj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
h : (↑u : ℕ) + 1 = (↑v : ℕ)
⊢ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1

Tactic:
simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

Premises used: Iff.mpr, Nat.lt_of_succ_le, LT.lt.le, Eq.le, Nat.eq_sub_of_add_eq', Fin.coe_sub_iff_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
h : (↑v : ℕ) + 1 = (↑u : ℕ)
⊢ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1

Tactic:
simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

Premises used: Iff.mpr, Nat.lt_of_succ_le, LT.lt.le, Eq.le, Nat.eq_sub_of_add_eq', Fin.coe_sub_iff_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
h : (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ)
inl : ∀ (h : (↑u : ℕ) + 1 = (↑v : ℕ)), (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1
inr : ∀ (h : (↑v : ℕ) + 1 = (↑u : ℕ)), (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1
⊢ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1

Tactic:
cases h with
    | inl h | inr h =>
      simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
h : (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ)
⊢ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1

Tactic:
cases h with
    | inl h | inr h =>
      simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
⊢ pathGraph n ≤ cycleGraph n

Tactic:
match n with
  | 0 | 1 => simp
  | n + 2 =>
    intro u v h
    rw [pathGraph_adj] at h
    rw [cycleGraph_adj']
    cases h with
    | inl h | inr h =>
      simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
⊢ (cycleGraph n).Preconnected

Tactic:
(pathGraph_preconnected n).mono pathGraph_le_cycleGraph

Premises used: SimpleGraph.Preconnected.mono, SimpleGraph.pathGraph_preconnected, SimpleGraph.pathGraph_le_cycleGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
⊢ Connected (V := Fin (n + 1)) (cycleGraph (n + 1))

Tactic:
(pathGraph_connected n).mono pathGraph_le_cycleGraph

Premises used: SimpleGraph.pathGraph_connected, SimpleGraph.Connected.mono, SimpleGraph.pathGraph_le_cycleGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
n m : ℕ
h : m + 1 < n + 3
⊢ Adj (cycleGraph (n + 3)) (⟨m + 1, h⟩ : Fin (n + 3)) ⟨m, ⋯⟩

Tactic:
simp [cycleGraph_adj, Fin.ext_iff, Fin.sub_val_of_le]

Premises used: Fin.sub_val_of_le, Fin.ext_iff, SimpleGraph.cycleGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
n : ℕ
⊢ Adj (V := Fin (n + 3)) (cycleGraph (n + 3)) 0 (Fin.last (n + 2))

Tactic:
simp [cycleGraph_adj]

Premises used: SimpleGraph.cycleGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
h : 0 < n + 3
unfold :
  length (V := Fin (n + 3)) (G := cycleGraph (n + 3)) (u := (⟨0, h⟩ : Fin (n + 3))) nil = (↑(⟨0, h⟩ : Fin (n + 3)) : ℕ)
⊢ length (u := (⟨0, h⟩ : Fin (n + 3))) (cycleCons n (⟨0, h⟩ : Fin (n + 3))) = (↑(⟨0, h⟩ : Fin (n + 3)) : ℕ)

Tactic:
unfold cycleGraph.cycleCons

Premises used: _private.0.SimpleGraph.cycleGraph.cycleCons
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
h : 0 < n + 3
⊢ length (V := Fin (n + 3)) (G := cycleGraph (n + 3)) (u := (⟨0, h⟩ : Fin (n + 3))) nil = (↑(⟨0, h⟩ : Fin (n + 3)) : ℕ)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n m : ℕ
h : m + 1 < n + 3
unfold :
  length (V := Fin (n + 3)) (G := cycleGraph (n + 3)) (u := (⟨m + 1, h⟩ : Fin (n + 3))) (v := 0)
      (have hadj := ⋯;
      cons hadj (cycleCons n (⟨m, ⋯⟩ : Fin (n + 3)))) =
    (↑(⟨m + 1, h⟩ : Fin (n + 3)) : ℕ)
⊢ length (u := (⟨m + 1, h⟩ : Fin (n + 3))) (cycleCons n (⟨m + 1, h⟩ : Fin (n + 3))) = (↑(⟨m + 1, h⟩ : Fin (n + 3)) : ℕ)

Tactic:
unfold cycleGraph.cycleCons

Premises used: _private.0.SimpleGraph.cycleGraph.cycleCons
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n m : ℕ
h : m + 1 < n + 3
rw rw₁ : (↑(⟨m, ⋯⟩ : Fin (n + 3)) : ℕ) + 1 = m + 1
⊢ length (u := (⟨m, ⋯⟩ : Fin (n + 3))) (cycleCons n (⟨m, ⋯⟩ : Fin (n + 3))) + 1 = m + 1

Tactic:
rw [cycleGraph.length_cycle_cons n]
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
⊢ length (V := Fin (n + 3)) (G := cycleGraph (n + 3)) (u := 0) (v := 0)
      (have hadj := ⋯;
      cons hadj (cycleCons n (Fin.last (n + 2)))) =
    n + 3

Tactic:
simp [cycleGraph.length_cycle_cons]

Premises used: _private.0.SimpleGraph.cycleGraph.length_cycle_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
m : Fin (n + 3)
i : ℕ
hi : i ≤ (↑m : ℕ)
obtain :
  ∀ (m : ℕ) (hm : m < n + 3) (hi : i ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)),
    (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) i) : ℕ) =
      ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - i) % (n + 3)
⊢ (↑((cycleCons n m).getVert i) : ℕ) = ((↑m : ℕ) - i) % (n + 3)

Tactic:
obtain ⟨m, hm⟩ := m
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n i m : ℕ
hm : m < n + 3
hi : i ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)
zero :
  ∀ (m : ℕ) (hm : m < n + 3) (hi : 0 ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)),
    (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) 0) : ℕ) =
      ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - 0) % (n + 3)
succ :
  ∀ (n_1 : ℕ),
    (∀ (m : ℕ) (hm : m < n + 3) (hi : n_1 ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)),
        (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) n_1) : ℕ) =
          ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - n_1) % (n + 3)) →
      ∀ (m : ℕ) (hm : m < n + 3) (hi : n_1 + 1 ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)),
        (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) (n_1 + 1)) : ℕ) =
          ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - (n_1 + 1)) % (n + 3)
⊢ (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) i) : ℕ) =
    ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - i) % (n + 3)

Tactic:
induction i generalizing m
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n m : ℕ
hm : m < n + 3
hi : 0 ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)
⊢ (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) 0) : ℕ) =
    ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - 0) % (n + 3)

Tactic:
simp [Nat.mod_eq_of_lt hm]

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n n_1 : ℕ
h :
  ∀ (m : ℕ) (hm : m < n + 3) (hi : n_1 ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)),
    (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) n_1) : ℕ) =
      ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - n_1) % (n + 3)
m : ℕ
hm : m < n + 3
hi : n_1 + 1 ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)
succ :
  ∀ (hm : 0 < n + 3) (hi : n_1 + 1 ≤ (↑(⟨0, hm⟩ : Fin (n + 3)) : ℕ)),
    (↑(getVert (u := (⟨0, hm⟩ : Fin (n + 3))) (cycleCons n (⟨0, hm⟩ : Fin (n + 3))) (n_1 + 1)) : ℕ) =
      ((↑(⟨0, hm⟩ : Fin (n + 3)) : ℕ) - (n_1 + 1)) % (n + 3)
succ₁ :
  ∀ (n_2 : ℕ) (hm : n_2 + 1 < n + 3) (hi : n_1 + 1 ≤ (↑(⟨n_2 + 1, hm⟩ : Fin (n + 3)) : ℕ)),
    (↑(getVert (u := (⟨n_2 + 1, hm⟩ : Fin (n + 3))) (cycleCons n (⟨n_2 + 1, hm⟩ : Fin (n + 3))) (n_1 + 1)) : ℕ) =
      ((↑(⟨n_2 + 1, hm⟩ : Fin (n + 3)) : ℕ) - (n_1 + 1)) % (n + 3)
⊢ (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) (n_1 + 1)) : ℕ) =
    ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - (n_1 + 1)) % (n + 3)

Tactic:
cases m
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n n_1 : ℕ
h :
  ∀ (m : ℕ) (hm : m < n + 3) (hi : n_1 ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)),
    (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) n_1) : ℕ) =
      ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - n_1) % (n + 3)
hm : 0 < n + 3
hi : n_1 + 1 ≤ (↑(⟨0, hm⟩ : Fin (n + 3)) : ℕ)
⊢ (↑(getVert (u := (⟨0, hm⟩ : Fin (n + 3))) (cycleCons n (⟨0, hm⟩ : Fin (n + 3))) (n_1 + 1)) : ℕ) =
    ((↑(⟨0, hm⟩ : Fin (n + 3)) : ℕ) - (n_1 + 1)) % (n + 3)

Tactic:
grind +locals [getVert_cons_succ]

Premises used: SimpleGraph.Walk.getVert_cons_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n n_1 : ℕ
h :
  ∀ (m : ℕ) (hm : m < n + 3) (hi : n_1 ≤ (↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ)),
    (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) n_1) : ℕ) =
      ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - n_1) % (n + 3)
n_2 : ℕ
hm : n_2 + 1 < n + 3
hi : n_1 + 1 ≤ (↑(⟨n_2 + 1, hm⟩ : Fin (n + 3)) : ℕ)
⊢ (↑(getVert (u := (⟨n_2 + 1, hm⟩ : Fin (n + 3))) (cycleCons n (⟨n_2 + 1, hm⟩ : Fin (n + 3))) (n_1 + 1)) : ℕ) =
    ((↑(⟨n_2 + 1, hm⟩ : Fin (n + 3)) : ℕ) - (n_1 + 1)) % (n + 3)

Tactic:
grind +locals [getVert_cons_succ]

Premises used: SimpleGraph.Walk.getVert_cons_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
n m : ℕ
hm : m ≤ n + 3
⊢ 0 < n + 3

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n m : ℕ
hm : m ≤ n + 3
zero : ∀ (hm : 0 ≤ n + 3), (cycle n).getVert 0 = ⟨(n + 3 - 0) % (n + 3), ⋯⟩
succ : ∀ (n_1 : ℕ) (hm : n_1 + 1 ≤ n + 3), (cycle n).getVert (n_1 + 1) = ⟨(n + 3 - (n_1 + 1)) % (n + 3), ⋯⟩
⊢ (cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), ⋯⟩

Tactic:
cases m
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
hm : 0 ≤ n + 3
⊢ (cycle n).getVert 0 = ⟨(n + 3 - 0) % (n + 3), ⋯⟩

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n n_1 : ℕ
hm : n_1 + 1 ≤ n + 3
⊢ (cycle n).getVert (n_1 + 1) = ⟨(n + 3 - (n_1 + 1)) % (n + 3), ⋯⟩

Tactic:
grind +locals [getVert_cons_succ, cycleGraph.getVert_cycleCons]

Premises used: _private.0.SimpleGraph.cycleGraph.getVert_cycleCons, SimpleGraph.Walk.getVert_cons_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
⊢ (cycle n).tail.IsPath

Tactic:
isPath_iff_injective_get_support _ |>.mpr fun ⟨i, hi⟩ ⟨j, hj⟩ hij ↦ ?_

Premises used: Iff.mpr, _private.0.SimpleGraph.cycleGraph.isPath_tail_cycle.match_1, Fin.mk, _private.0.SimpleGraph.cycleGraph.isPath_tail_cycle.match_2, SimpleGraph.Walk.isPath_iff_injective_get_support, Eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
refine :
  ∀ (x x : Fin (cycle n).tail.support.length) (i : ℕ) (hi : i < (cycle n).tail.support.length) (j : ℕ)
    (hj : j < (cycle n).tail.support.length)
    (hij :
      Eq (α := Fin (n + 3)) ((fun (x : Fin (cycle n).tail.support.length) ↦ (cycle n).tail.support.get x) ⟨i, hi⟩)
        ((fun (x : Fin (cycle n).tail.support.length) ↦ (cycle n).tail.support.get x) ⟨j, hj⟩)),
    (⟨i, hi⟩ : Fin (cycle n).tail.support.length) = ⟨j, hj⟩
⊢ (cycle n).tail.IsPath

Tactic:
refine isPath_iff_injective_get_support _ |>.mpr fun ⟨i, hi⟩ ⟨j, hj⟩ hij ↦ ?_

Premises used: Iff.mpr, SimpleGraph.Walk.isPath_iff_injective_get_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
x x_1 : Fin (cycle n).tail.support.length
i : ℕ
hi : i < (cycle n).tail.support.length
j : ℕ
hj : j < (cycle n).tail.support.length
hij :
  Eq (α := Fin (n + 3)) ((fun (x : Fin (cycle n).tail.support.length) ↦ (cycle n).tail.support.get x) ⟨i, hi⟩)
    ((fun (x : Fin (cycle n).tail.support.length) ↦ (cycle n).tail.support.get x) ⟨j, hj⟩)
rw :
  ∀ (hi_1 : i < (cycle n).support.tail.length) (j : ℕ) (hj : j < (cycle n).tail.support.length)
    (hj_1 : j < (cycle n).support.tail.length)
    (hij :
      Eq (α := Fin (n + 3)) ((fun (x : Fin (cycle n).tail.support.length) ↦ (cycle n).tail.support.get x) ⟨i, hi⟩)
        ((fun (x : Fin (cycle n).tail.support.length) ↦ (cycle n).tail.support.get x) ⟨j, hj⟩)),
    (⟨i, hi⟩ : Fin (cycle n).tail.support.length) = ⟨j, hj⟩
⊢ (⟨i, hi⟩ : Fin (cycle n).tail.support.length) = ⟨j, hj⟩

Tactic:
rw [support_tail_of_not_nil _ (of_decide_eq_false rfl)] at hi hj

Premises used: SimpleGraph.Walk.support_tail_of_not_nil, of_decide_eq_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
x x_1 : Fin (cycle n).tail.support.length
i : ℕ
hi_1 : i < (cycle n).tail.support.length
hi : i < (cycle n).support.tail.length
j : ℕ
hj_1 : j < (cycle n).tail.support.length
hj : j < (cycle n).support.tail.length
hij :
  Eq (α := Fin (n + 3)) ((fun (x : Fin (cycle n).tail.support.length) ↦ (cycle n).tail.support.get x) ⟨i, hi_1⟩)
    ((fun (x : Fin (cycle n).tail.support.length) ↦ (cycle n).tail.support.get x) ⟨j, hj_1⟩)
⊢ (cycle n).getVert (i + 1) = (cycle n).getVert (j + 1)

Tactic:
simp only [List.get_eq_getElem, support_getElem_eq_getVert, getVert_tail] at hij

Premises used: List.get_eq_getElem, SimpleGraph.Walk.getVert_tail, SimpleGraph.Walk.support_getElem_eq_getVert