mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hv : v ∈ s
⊢ G.Adj v ↑(f ⟨v, hv⟩)

pp: case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
w : V
hw : w ∈ s
⊢ G.Adj (↑(f ⟨w, hw⟩)) w

Tactic:
·

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hv : v ∈ s
⊢ G.Adj v ↑(f ⟨v, hv⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
w : V
hw : w ∈ s
⊢ G.Adj (↑(f ⟨w, hw⟩)) w

Tactic:
·

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
w : V
hw : w ∈ s
⊢ G.Adj (↑(f ⟨w, hw⟩)) w
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : c = a → d ≠ b
h : a = c
⊢ ∃ a b c,
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

pp: case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : c = a → d ≠ b
h : ¬a = c
⊢ ∃ a b c,
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
·

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : c = a → d ≠ b
h : a = c
⊢ ∃ a b c,
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ List.count b p.support = 1

Tactic:
by
  rw [← cons_support_tail hp.1.not_nil, List.count_cons_of_ne h, hp.isHamiltonian_tail]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
h✝ : Infinite α
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
h✝ : Finite α
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
h✝ : Infinite α
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a : α
⊢ G.Reachable a a

pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
⊢ G.Reachable a b

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a : α
⊢ G.Reachable a a
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
h : Fintype.card α = 2
hG : G.IsHamiltonian
⊢ Fintype.card α ≠ 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

pp: case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Tactic:
·

Goal state after:
case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ↑(f ⟨v, ⋯⟩) = ↑(f ⟨v, hl⟩)

pp: case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hys : y ∈ s
hl : ↑(f ⟨y, hys⟩) ∈ s
⊢ y = ↑(f ⟨↑(f ⟨y, hys⟩), hl⟩)

Tactic:
·

Goal state after:
case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ↑(f ⟨v, ⋯⟩) = ↑(f ⟨v, hl⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hys : y ∈ s
hl : ↑(f ⟨y, hys⟩) ∈ s
⊢ y = ↑(f ⟨↑(f ⟨y, hys⟩), hl⟩)

Tactic:
·

Goal state after:
case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hys : y ∈ s
hl : ↑(f ⟨y, hys⟩) ∈ s
⊢ y = ↑(f ⟨↑(f ⟨y, hys⟩), hl⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Tactic:
·

Goal state after:
case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
hy : v ∈ s
⊢ ↑(f ⟨v, hy⟩) = ↑(f.symm ⟨v, hr⟩)

pp: case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hy : y ∈ s
hr : ↑(f ⟨y, hy⟩) ∈ t
⊢ y = ↑(f.symm ⟨↑(f ⟨y, hy⟩), hr⟩)

Tactic:
·

Goal state after:
case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
hy : v ∈ s
⊢ ↑(f ⟨v, hy⟩) = ↑(f.symm ⟨v, hr⟩)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : c = a → d ≠ b
h : ¬a = c
⊢ ∃ a b c,
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
·

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : c = a → d ≠ b
h : ¬a = c
⊢ ∃ a b c,
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hy : y ∈ s
hr : ↑(f ⟨y, hy⟩) ∈ t
⊢ y = ↑(f.symm ⟨↑(f ⟨y, hy⟩), hr⟩)

Tactic:
·

Goal state after:
case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hy : y ∈ s
hr : ↑(f ⟨y, hy⟩) ∈ t
⊢ y = ↑(f.symm ⟨↑(f ⟨y, hy⟩), hr⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i

pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
x✝ : ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i
e : Sym2 V
he : e ∈ M.edgeSet
hv : v ∈ ↑e
⊢ v ∈ M.verts

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
x✝ : ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i
e : Sym2 V
he : e ∈ M.edgeSet
hv : v ∈ ↑e
⊢ v ∈ M.verts

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
x✝ : ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i
e : Sym2 V
he : e ∈ M.edgeSet
hv : v ∈ ↑e
⊢ v ∈ M.verts
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching → ∀ (v : V), ∃! w, M.Adj v w

pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v : V
⊢ v ∈ M.verts

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching → ∀ (v : V), ∃! w, M.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v : V
⊢ v ∈ M.verts

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v : V
⊢ v ∈ M.verts
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∈ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 2

pp: case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∈ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 2
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 0
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ v ≠ x

pp: case refine_2
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ w₁ ≠ x

pp: case refine_3
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ w₂ ≠ x

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ v ≠ x
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : a = b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = ↑(G.degree a)

pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : ¬a = b
h' : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

pp: case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : ¬a = b
h' : ¬G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : a = b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = ↑(G.degree a)
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : ¬a = b
h' : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

pp: case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : ¬a = b
h' : ¬G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : ¬a = b
h' : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : ¬a = b
h' : ¬G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : ¬a = b
h' : ¬G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 0
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj v y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj v z}) ≤ 2
haj : ¬G.Adj v a
hbj : ¬G.Adj v b
hcj : ¬G.Adj v a
hdj : ¬G.Adj v b
hax : v = a
⊢ False

pp: case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj v y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj v z}) ≤ 2
haj : ¬G.Adj v a
hbj : ¬G.Adj v b
hcj : ¬G.Adj v a
hdj : ¬G.Adj v b
hax : ¬v = a
⊢ False

Tactic:
·

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj v y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj v z}) ≤ 2
haj : ¬G.Adj v a
hbj : ¬G.Adj v b
hcj : ¬G.Adj v a
hdj : ¬G.Adj v b
hax : v = a
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj v y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj v z}) ≤ 2
haj : ¬G.Adj v a
hbj : ¬G.Adj v b
hcj : ¬G.Adj v a
hdj : ¬G.Adj v b
hax : ¬v = a
⊢ False

Tactic:
·

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj v y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj v z}) ≤ 2
haj : ¬G.Adj v a
hbj : ¬G.Adj v b
hcj : ¬G.Adj v a
hdj : ¬G.Adj v b
hax : ¬v = a
⊢ False