awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
⊢ p.getVert (List.idxOf w p.support) = w

Tactic:
grind [getVert_eq_support_getElem]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.getVert ∘ Fin.val = p.support.get

Tactic:
grind [getVert_eq_support_getElem, length_support]

Premises used: SimpleGraph.Walk.length_support, SimpleGraph.Walk.getVert_eq_support_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x : V
⊢ x ∈ Set.range p.getVert → x ∈ Set.range p.support.get

Tactic:
grind [Set.range_list_get, getVert_mem_support]

Premises used: SimpleGraph.Walk.getVert_mem_support, Set.range_list_get
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x : V
h : x ∈ Set.range p.support.get
n : Fin p.support.length
h_1 : p.support.get n = x
⊢ p.getVert (↑n : ℕ) = x

Tactic:
grind [getVert_eq_support_getElem, length_support]

Premises used: SimpleGraph.Walk.length_support, SimpleGraph.Walk.getVert_eq_support_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : n < p.darts.length
⊢ n < p.length

Tactic:
rw [p.length_darts] at h

Premises used: SimpleGraph.Walk.length_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h_1 : n < p.darts.length
h : n < p.length
h₁ :
  (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1).toProd.1 =
    { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ : G.Dart }.toProd.1
h₂ :
  (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1).toProd.2 =
    { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ : G.Dart }.toProd.2
⊢ getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1 =
    { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h_1 : n < p.darts.length
h : n < p.length
⊢ (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1).toProd.1 =
    { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ : G.Dart }.toProd.1

Tactic:
simp [p.getVert_eq_support_getElem (le_of_lt h), p.getVert_eq_support_getElem h]

Premises used: le_of_lt, SimpleGraph.Walk.getVert_eq_support_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h_1 : n < p.darts.length
h : n < p.length
⊢ (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1).toProd.2 =
    { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ : G.Dart }.toProd.2

Tactic:
simp [p.getVert_eq_support_getElem (le_of_lt h), p.getVert_eq_support_getElem h]

Premises used: le_of_lt, SimpleGraph.Walk.getVert_eq_support_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : [u', v'] <:+: p.support
have :
  ∀ (k : ℕ) (hk : [u', v'].length + k ≤ p.support.length)
    (h :
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)),
    G.Adj u' v'
⊢ G.Adj u' v'

Tactic:
have ⟨k, hk, h⟩ := List.infix_iff_getElem?.mp h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)

Tactic:
have h₀ := Nat.zero_add _ ▸ h 0 Nat.zero_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (k + 1) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two)

Tactic:
have h₁ := Nat.add_comm .. ▸ h 1 Nat.one_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)
h₁ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (k + 1) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two)
⊢ k ≤ p.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ : some (p.getVert k) = some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)
h₁ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (k + 1) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two)
⊢ k + 1 ≤ p.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)
h₁ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (k + 1) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two)
⊢ p.getVert k = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two

Tactic:
rw [← getVert_eq_support_getElem? _ <| by grind, Option.some.injEq] at h₀ h₁

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem?, Option.some.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)
h₁ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (k + 1) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two)
h₂ : p.getVert k = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two
⊢ p.getVert (k + 1) = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two

Tactic:
rw [← getVert_eq_support_getElem? _ <| by grind, Option.some.injEq] at h₀ h₁

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem?, Option.some.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ : p.getVert k = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two
h₁ : p.getVert (k + 1) = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two
⊢ k < p.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ : p.getVert k = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two
h₁ : p.getVert (k + 1) = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two
⊢ G.Adj u' v'

Tactic:
exact h₀ ▸ h₁ ▸ p.adj_getVert_succ (i := k) <| by grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ 0 < p.length

Tactic:
simpa [not_nil_iff_lt_length] using hp

Premises used: SimpleGraph.Walk.not_nil_iff_lt_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ G.Adj v p.snd

Tactic:
simpa using adj_getVert_succ p (by simpa [not_nil_iff_lt_length] using hp : 0 < p.length)

Premises used: SimpleGraph.Walk.adj_getVert_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
hadj : G.Adj u v
⊢ (cons hadj q).snd = v

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ¬p.Nil
⊢ ∀ {u v w : V} (h : G.Adj u v) (q : G.Walk v w), (cons h q).snd ∈ (cons h q).support.tail

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : 1 < p.support.length
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 1 hp = p.snd

Tactic:
grind [getVert_eq_support_getElem]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hnil : ¬p.Nil
⊢ 1 < p.support.length

Tactic:
grind [not_nil_iff_lt_length]

Premises used: SimpleGraph.Walk.not_nil_iff_lt_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hnil : ¬p.Nil
⊢ p.snd = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 1 ⋯

Tactic:
support_getElem_one _ |>.symm

Premises used: SimpleGraph.Walk.support_getElem_one, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ penultimate (G := G) (u := v) nil = v

Tactic:
rfl

Premises used: rfl, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).penultimate = u

Tactic:
rfl

Premises used: rfl, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v w w' : V
h : G.Adj u v
h₂ : G.Adj v w
p : G.Walk w w'
⊢ (cons h (cons h₂ p)).penultimate = (cons h₂ p).penultimate

Tactic:
rfl

Premises used: Nat.pred, rfl, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
hp : ¬p.Nil
⊢ ∀ {u_1 v w : V} (h : G.Adj u_1 v) (q : G.Walk v w) (x : G.Adj u u_1),
    (cons x (cons h q)).penultimate = (cons h q).penultimate

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ G.Adj p.penultimate w

Tactic:
grind [getVert_length, length_eq_zero_iff, adj_getVert_succ]

Premises used: SimpleGraph.Walk.adj_getVert_succ, SimpleGraph.Walk.getVert_length, SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ¬p.Nil
⊢ p.penultimate ≠ v

Tactic:
have := adj_penultimate h |>.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ¬p.Nil
this : p.penultimate ≠ v
⊢ p.penultimate ∈ p.support.dropLast

Tactic:
grind [getVert_mem_support, List.dropLast_concat_getLast, getLast_support]

Premises used: List.dropLast_concat_getLast, SimpleGraph.Walk.getVert_mem_support, SimpleGraph.Walk.getLast_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (p.length - 1) ⋯ = p.penultimate

Tactic:
grind [getVert_eq_support_getElem]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ (p.firstDart hp).edge = s(v, p.snd)

Tactic:
rfl

Premises used: SimpleGraph.Dart.edge, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ (p.lastDart hp).edge = s(p.penultimate, w)

Tactic:
rfl

Premises used: SimpleGraph.Dart.edge, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
h₁ : ¬p.Nil
h₂ : 0 < p.darts.length
⊢ p.firstDart h₁ = getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts 0 h₂

Tactic:
simp [Dart.ext_iff, firstDart_toProd, darts_getElem_eq_getVert]

Premises used: SimpleGraph.Dart.ext_iff, SimpleGraph.Walk.darts_getElem_eq_getVert, SimpleGraph.Walk.firstDart_toProd
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
h₁ : ¬p.Nil
h₂ : 0 < p.darts.length
⊢ p.lastDart h₁ = getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts (p.darts.length - 1) ⋯

Tactic:
simp (disch := grind) [Dart.ext_iff, lastDart_toProd, darts_getElem_eq_getVert,
    p.getVert_of_length_le]

Premises used: SimpleGraph.Walk.lastDart_toProd, SimpleGraph.Dart.ext_iff, SimpleGraph.Walk.getVert_of_length_le, SimpleGraph.Walk.darts_getElem_eq_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : p.darts ≠ []
⊢ p.darts.head hnil = p.firstDart ⋯

Tactic:
grind [firstDart_eq]

Premises used: SimpleGraph.Walk.firstDart_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ p.firstDart hnil = p.darts.head ⋯

Tactic:
head_darts_eq_firstDart _ |>.symm

Premises used: Eq.symm, SimpleGraph.Walk.head_darts_eq_firstDart
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
hp : p.darts ≠ []
⊢ (p.darts.head hp).toProd.1 = a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ p.firstDart hnil ∈ p.darts

Tactic:
p.firstDart_eq_head_darts _ ▸ List.head_mem _

Premises used: List.head_mem, SimpleGraph.Walk.firstDart_eq_head_darts, Eq.rec, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : p.darts ≠ []
⊢ p.darts.getLast hnil = p.lastDart ⋯

Tactic:
grind [lastDart_eq, not_nil_iff_lt_length]

Premises used: SimpleGraph.Walk.lastDart_eq, SimpleGraph.Walk.not_nil_iff_lt_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ p.lastDart hnil = p.darts.getLast ⋯

Tactic:
grind [lastDart_eq, not_nil_iff_lt_length]

Premises used: SimpleGraph.Walk.lastDart_eq, SimpleGraph.Walk.not_nil_iff_lt_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
hp : p.darts ≠ []
⊢ (p.darts.getLast hp).toProd.2 = b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ p.lastDart hnil ∈ p.darts

Tactic:
p.lastDart_eq_getLast_darts _ ▸ List.getLast_mem _

Premises used: SimpleGraph.Walk.lastDart_eq_getLast_darts, Eq.rec, List.getLast_mem, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.edges ≠ []
⊢ p.edges.head hp = s(v, p.snd)

Tactic:
simp [p.edge_firstDart, Walk.edges]

Premises used: SimpleGraph.Walk.edge_firstDart, SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ s(v, p.snd) = p.edges.head ⋯

Tactic:
head_edges_eq_mk_start_snd _ |>.symm

Premises used: SimpleGraph.Walk.head_edges_eq_mk_start_snd, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ s(v, p.snd) ∈ p.edges

Tactic:
p.mk_start_snd_eq_head_edges hnil ▸ List.head_mem _

Premises used: List.head_mem, SimpleGraph.Walk.mk_start_snd_eq_head_edges, Eq.rec, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.edges ≠ []
⊢ p.edges.getLast hp = s(p.penultimate, w)

Tactic:
simp [p.edge_lastDart, Walk.edges]

Premises used: SimpleGraph.Walk.edge_lastDart, SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ s(p.penultimate, w) = p.edges.getLast ⋯

Tactic:
getLast_edges_eq_mk_penultimate_end _ |>.symm

Premises used: SimpleGraph.Walk.getLast_edges_eq_mk_penultimate_end, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ s(p.penultimate, w) ∈ p.edges

Tactic:
p.mk_penultimate_end_eq_getLast_edges hnil ▸ List.getLast_mem _

Premises used: Eq.rec, SimpleGraph.Walk.mk_penultimate_end_eq_getLast_edges, List.getLast_mem, Eq.symm
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
c : Set X
s : Subgroup ↥(MulAction.stabilizer G c)
⊢ (↑{ carrier := c, symmetries := s : Prototile G X } : Set X) = c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
x : X
p : Prototile G X
⊢ x ∈ (↑p : Set X) ↔ x ∈ p

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
t : ιₚ → Prototile G X
⊢ (↑{ tiles := t : Protoset G X ιₚ } : ιₚ → Prototile G X) = t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps₁ ps₂ : Protoset G X ιₚ
⊢ (↑ps₁ : ιₚ → Prototile G X) = (↑ps₂ : ιₚ → Prototile G X) ↔ ps₁ = ps₂

Tactic:
Protoset.ext_iff.symm

Premises used: DiscreteTiling.Protoset.ext_iff, Iff.symm
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
⊢ Injective (α := Protoset G X ιₚ) tiles

Tactic:
fun _ _ ↦ coe_inj.1

Premises used: DiscreteTiling.Protoset.coe_inj, Iff.mp, Function.Injective
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
inst_2 : Nonempty ιₚ
⊢ Nonempty (PlacedTile ps)

Tactic:
⟨⟨Classical.arbitrary _, (1 : G)⟩⟩

Premises used: QuotientGroup.mk, DiscreteTiling.PlacedTile.mk, Nonempty.intro, Classical.arbitrary, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
ppt : PlacedTile ps → Prop
pt : PlacedTile ps
h :
  ∀ (i : ιₚ) (gx : G),
    ppt
      { index := i,
        groupElts :=
          (↑gx :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) }
rcases :
  ∀ (i : ιₚ)
    (gx :
      G ⧸
        Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)))
          ((↑ps : ιₚ → Prototile G X) i).symmetries),
    ppt { index := i, groupElts := gx }
⊢ ppt pt

Tactic:
rcases pt with ⟨i, gx⟩
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
ppt : PlacedTile ps → Prop
h :
  ∀ (i : ιₚ) (gx : G),
    ppt
      { index := i,
        groupElts :=
          (↑gx :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) }
i : ιₚ
gx :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i).symmetries
h₁ : ∀ (a : G), ppt { index := i, groupElts := ⟦a⟧ }
⊢ ppt { index := i, groupElts := gx }

Tactic:
induction gx using Quotient.inductionOn
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
ppt : PlacedTile ps → Prop
h :
  ∀ (i : ιₚ) (gx : G),
    ppt
      { index := i,
        groupElts :=
          (↑gx :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) }
i : ιₚ
a : G
⊢ ppt { index := i, groupElts := ⟦a⟧ }

Tactic:
apply h
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
⊢ pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts

Tactic:
⟨fun h ↦ ?_, fun ⟨h, g, hg₁, hg₂⟩ ↦ ?_⟩

Premises used: _private.0.DiscreteTiling.PlacedTile.ext_iff_of_exists.match_1, Iff.intro, Eq