awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
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
⊢ u - v ∈ s ∨ v - u ∈ s
have Adj₁ : ∀ (h1 : 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
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
⊢ circulantGraph s = circulantGraph (s ∪ -s)
have Adj : ∀ (x x_1 : G), (circulantGraph s).Adj x x_1 ↔ (circulantGraph (s ∪ -s)).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
x x_1 : G
⊢ (circulantGraph s).Adj x x_1 ↔ (circulantGraph (s ∪ -s)).Adj x x_1
have 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)
Tactic: simp only [circulantGraph_adj, Set.mem_union, Set.mem_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
⊢ Eq (α := SimpleGraph (Fin (n + 1))) (cycleGraph (n + 1)) (circulantGraph {1})
have zero : Eq (α := SimpleGraph (Fin (HAdd.hAdd (α := ℕ) 0 1))) (cycleGraph (HAdd.hAdd (α := ℕ) 0 1)) (circulantGraph {1})
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
zero : Eq (α := SimpleGraph (Fin (HAdd.hAdd (α := ℕ) 0 1))) (cycleGraph (HAdd.hAdd (α := ℕ) 0 1)) (circulantGraph {1})
⊢ Eq (α := SimpleGraph (Fin (n + 1))) (cycleGraph (n + 1)) (circulantGraph {1})
have succ : ∀ (n : ℕ), Eq (α := SimpleGraph (Fin (n + 1 + 1))) (cycleGraph (n + 1 + 1)) (circulantGraph {1})
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
⊢ Eq (α := SimpleGraph (Fin 2)) (cycleGraph 2) ⊤
have simp : ∀ (x x_1 : Fin 2), Adj (cycleGraph 2) x x_1 = Adj ⊤ x x_1
Tactic: simp only [SimpleGraph.ext_iff, funext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
⊢ Eq (α := SimpleGraph (Fin 3)) (cycleGraph 3) ⊤
have simp : ∀ (x x_1 : Fin 3), Adj (cycleGraph 3) x x_1 = Adj ⊤ x x_1
Tactic: simp only [SimpleGraph.ext_iff, funext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
v : Fin (n + 2)
⊢ neighborSet (cycleGraph (n + 2)) v = {v - 1, v + 1}
have h : ∀ (w : Fin (n + 2)), w ∈ neighborSet (cycleGraph (n + 2)) v ↔ Membership.mem (γ := Set (Fin (n + 2))) {v - 1, v + 1} w
Tactic: ext w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
v w : Fin (n + 2)
⊢ Adj (cycleGraph (n + 2)) v w ↔ w = v - 1 ∨ w = v + 1
have h : v - w = 1 ∨ w - v = 1 ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
v w : Fin (n + 2)
h : v - w = 1 ∨ w - v = 1 ↔ w = v - 1 ∨ w = v + 1
⊢ Adj (cycleGraph (n + 2)) v w ↔ w = v - 1 ∨ w = v + 1
have h₁ : v = w + 1 ∨ w - v = 1 ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
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
⊢ Adj (cycleGraph (n + 2)) v w ↔ w = v - 1 ∨ w = v + 1
have h₂ : v = w + 1 ∨ w = v + 1 ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
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
⊢ Adj (cycleGraph (n + 2)) v w ↔ w = v - 1 ∨ w = v + 1
have h₃ : v = w + 1 ∨ w = v + 1 ↔ w + 1 = v ∨ w = v + 1
Tactic: rw [cycleGraph_adj, sub_eq_iff_eq_add', sub_eq_iff_eq_add', eq_sub_iff_add_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
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
⊢ Adj (cycleGraph (n + 2)) v w ↔ w = v - 1 ∨ w = v + 1
have h₄ : w + 1 = v ∨ w = v + 1 ↔ w + 1 = v ∨ w = v + 1
Tactic: rw [cycleGraph_adj, sub_eq_iff_eq_add', sub_eq_iff_eq_add', eq_sub_iff_add_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
v : Fin (n + 2)
⊢ degree (cycleGraph (n + 2)) v = Finset.card (α := Fin (n + 2)) {v - 1, v + 1}
have rw : (neighborFinset (cycleGraph (n + 2)) v).card = Finset.card (α := Fin (n + 2)) {v - 1, v + 1}
Tactic: rw [SimpleGraph.degree, cycleGraph_neighborFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
v : Fin (n + 2)
rw : (neighborFinset (cycleGraph (n + 2)) v).card = Finset.card (α := Fin (n + 2)) {v - 1, v + 1}
⊢ degree (cycleGraph (n + 2)) v = Finset.card (α := Fin (n + 2)) {v - 1, v + 1}
have rw₁ : Finset.card (α := Fin (n + 2)) {v - 1, v + 1} = Finset.card (α := Fin (n + 2)) {v - 1, v + 1}
Tactic: rw [SimpleGraph.degree, cycleGraph_neighborFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
v : Fin (n + 3)
⊢ degree (cycleGraph (n + 3)) v = 2
have rw : v - 1 ≠ v + 1
Tactic: rw [cycleGraph_degree_two_le, Finset.card_pair]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
v : Fin (n + 3)
⊢ v - 1 ≠ v + 1
have simp : ¬HAdd.hAdd (α := Fin (n + 3)) 1 1 = 0
Tactic: simp only [ne_eq, sub_eq_iff_eq_add, add_assoc v, left_eq_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (hypothesis)
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
h : Adj (pathGraph (n + 2)) u v
⊢ Adj (cycleGraph (n + 2)) u v
have h₁ : (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ)
Tactic: rw [pathGraph_adj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
h : (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ)
⊢ Adj (cycleGraph (n + 2)) u v
have rw : (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1
Tactic: rw [cycleGraph_adj']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n_1 n : ℕ
u v : Fin (n + 2)
h : (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ)
⊢ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1
have inl : ∀ (h : (↑u : ℕ) + 1 = (↑v : ℕ)), (↑(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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
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
⊢ (↑(u - v) : ℕ) = 1 ∨ (↑(v - u) : ℕ) = 1
have inr : ∀ (h : (↑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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
h : 0 < n + 3
⊢ length (u := (⟨0, h⟩ : Fin (n + 3))) (cycleCons n (⟨0, h⟩ : Fin (n + 3))) = (↑(⟨0, h⟩ : Fin (n + 3)) : ℕ)
have unfold : length (V := Fin (n + 3)) (G := cycleGraph (n + 3)) (u := (⟨0, h⟩ : Fin (n + 3))) nil = (↑(⟨0, h⟩ : Fin (n + 3)) : ℕ)
Tactic: unfold cycleGraph.cycleCons
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n m : ℕ
h : m + 1 < n + 3
⊢ length (u := (⟨m + 1, h⟩ : Fin (n + 3))) (cycleCons n (⟨m + 1, h⟩ : Fin (n + 3))) = (↑(⟨m + 1, h⟩ : Fin (n + 3)) : ℕ)
have unfold : length (V := Fin (n + 3)) (G := cycleGraph (n + 3)) (u := (⟨m + 1, h⟩ : Fin (n + 3))) (v := 0)
    (have hadj := sorry;
    cons hadj (cycleCons n (⟨m, sorry⟩ : Fin (n + 3)))) =
  (↑(⟨m + 1, h⟩ : Fin (n + 3)) : ℕ)
Tactic: unfold cycleGraph.cycleCons
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n m : ℕ
h : m + 1 < n + 3
⊢ length (u := (⟨m, ⋯⟩ : Fin (n + 3))) (cycleCons n (⟨m, ⋯⟩ : Fin (n + 3))) + 1 = m + 1
have rw : (↑(⟨m, sorry⟩ : Fin (n + 3)) : ℕ) + 1 = m + 1
Tactic: rw [cycleGraph.length_cycle_cons n]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
m : Fin (n + 3)
i : ℕ
hi : i ≤ (↑m : ℕ)
⊢ (↑((cycleCons n m).getVert i) : ℕ) = ((↑m : ℕ) - i) % (n + 3)
have 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)
Tactic: obtain ⟨m, hm⟩ := m
Cleared hypotheses: m, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n i 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)
have 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)
Tactic: induction i generalizing m
Cleared hypotheses: i, m, hm, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
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)
⊢ (↑(getVert (u := (⟨m, hm⟩ : Fin (n + 3))) (cycleCons n (⟨m, hm⟩ : Fin (n + 3))) i) : ℕ) =
    ((↑(⟨m, hm⟩ : Fin (n + 3)) : ℕ) - i) % (n + 3)
have 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)
Tactic: induction i generalizing m
Cleared hypotheses: i, m, hm, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
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)) : ℕ)
⊢ (↑(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)
have 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)
Tactic: cases m
Cleared hypotheses: m, hm, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
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)
⊢ (↑(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)
have 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)
Tactic: cases m
Cleared hypotheses: m, hm, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n m : ℕ
hm : m ≤ n + 3
⊢ (cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), ⋯⟩
have zero : ∀ (hm : 0 ≤ n + 3), (cycle n).getVert 0 = ⟨(n + 3 - 0) % (n + 3), sorry⟩
Tactic: cases m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n m : ℕ
hm : m ≤ n + 3
zero : ∀ (hm : 0 ≤ n + 3), (cycle n).getVert 0 = ⟨(n + 3 - 0) % (n + 3), ⋯⟩
⊢ (cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), ⋯⟩
have succ : ∀ (n_1 : ℕ) (hm : n_1 + 1 ≤ n + 3), (cycle n).getVert (n_1 + 1) = ⟨(n + 3 - (n_1 + 1)) % (n + 3), sorry⟩
Tactic: cases m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
n : ℕ
⊢ (cycle n).tail.IsPath
have 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⟩
Tactic: refine isPath_iff_injective_get_support _ |>.mpr fun ⟨i, hi⟩ ⟨j, hj⟩ hij ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
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⟩)
⊢ (⟨i, hi⟩ : Fin (cycle n).tail.support.length) = ⟨j, hj⟩
have 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⟩
Tactic: rw [support_tail_of_not_nil _ (of_decide_eq_false rfl)] at hi hj
Cleared hypotheses: j, hj, hij
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (hypothesis)
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⟩)
⊢ (⟨i, hi_1⟩ : Fin (cycle n).tail.support.length) = ⟨j, hj_1⟩
have hij₁ : (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
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adj ↔ induce s G = ⊤
have mp : s.Pairwise G.Adj → induce s G = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
mp : s.Pairwise G.Adj → induce s G = ⊤
⊢ s.Pairwise G.Adj ↔ induce s G = ⊤
have mpr : induce s G = ⊤ → s.Pairwise G.Adj
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
⊢ induce s G = ⊤
have mp : ∀ (v : α) (hv : v ∈ s) (w : α) (hw : w ∈ s),
  (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) ↔
    Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
Tactic: ext ⟨v, hv⟩ ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) ↔
    Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
have mp : G.Adj
    ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : { x : α // x ∈ s }) → α)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv))
    ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : { x : α // x ∈ s }) → α)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)) ↔
  ¬v = w
Tactic: simp only [comap_adj, top_adj, Ne, Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
⊢ G.Adj v w
have h2 : (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
  (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
Tactic: have h2 : (G.induce s).Adj ⟨v, hv⟩ ⟨w, hw⟩ = _ := rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
    (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
| (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
have rw : Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
    (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
⊢ G.Adj v w
have h2₁ : Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
  (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
Tactic: conv_lhs at h2 => rw [h]
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
    (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
⊢ G.Adj v w
have h2₁ : ¬v = w ↔ (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
Tactic: simp only [top_adj, ne_eq, Subtype.mk.injEq, eq_iff_iff] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t
have refine_1 : ∀ (h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t), G.IsClique ((⇑f : (a : α) → β) ⁻¹' t)
Tactic: refine ⟨fun h ↦ ⟨f ⁻¹' t, ?_, ?_⟩, by rintro ⟨x, hs, rfl⟩; exact hs.map⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
refine_1 : ∀ (h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t), G.IsClique ((⇑f : (a : α) → β) ⁻¹' t)
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t
have refine_2 : ∀ (h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t),
  Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' t) = t
Tactic: refine ⟨fun h ↦ ⟨f ⁻¹' t, ?_, ?_⟩, by rintro ⟨x, hs, rfl⟩; exact hs.map⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : α
hx : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
y : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
hne : x ≠ y
⊢ G.Adj x y
have refine_1 : ∀ (u v : α) (huv : G.Adj u v) (hux : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) x : β))
  (hvy : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) v : β) ((f : (a : α) → β) y : β)), G.Adj x y
Tactic: obtain ⟨-, u, v, huv, hux, hvy⟩ := h hx hy (by simpa)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : α
hx : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
y : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) x : β)
hvy : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) v : β) ((f : (a : α) → β) y : β)
⊢ G.Adj x y
have hux₁ : u = x
Tactic: rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy
Cleared hypotheses: hux, hvy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : α
hx : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
y : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) x : β)
hvy : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) v : β) ((f : (a : α) → β) y : β)
hux₁ : u = x
⊢ G.Adj x y
have hvy₁ : v = y
Tactic: rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy
Cleared hypotheses: hux, hvy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : α
hx : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
y : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : u = x
hvy : v = y
⊢ G.Adj x y
have refine_1 : G.Adj u y
Tactic: rwa [← hux, ← hvy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
⊢ Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' t) = t
have refine_2 : t ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
Tactic: rw [Set.image_preimage_eq_iff]