awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s t : Set (Sym2 V)
Adj : ∀ (v w : V), (fromEdgeSet (s \ t)).Adj v w ↔ (fromEdgeSet s \ fromEdgeSet t).Adj v w
⊢ fromEdgeSet (s \ t) = fromEdgeSet s \ fromEdgeSet t

Tactic:
ext v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (fromEdgeSet (s \ t)).Adj v w → (fromEdgeSet s \ fromEdgeSet t).Adj v w
Adj₁ : (fromEdgeSet s \ fromEdgeSet t).Adj v w → (fromEdgeSet (s \ t)).Adj v w
⊢ (fromEdgeSet (s \ t)).Adj v w ↔ (fromEdgeSet s \ fromEdgeSet t).Adj v w

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (fromEdgeSet (s \ t)).Adj v w → (fromEdgeSet s \ fromEdgeSet t).Adj v w

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (fromEdgeSet s \ fromEdgeSet t).Adj v w → (fromEdgeSet (s \ t)).Adj v w

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
simp : s \ Sym2.diagSet ⊆ t
⊢ fromEdgeSet s ≤ fromEdgeSet t

Tactic:
simp only [le_fromEdgeSet_iff, edgeSet_fromEdgeSet]

Premises used: SimpleGraph.edgeSet_fromEdgeSet, SimpleGraph.le_fromEdgeSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
grw : t \ Sym2.diagSet ⊆ t
⊢ s \ Sym2.diagSet ⊆ t

Tactic:
grw [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
⊢ t \ Sym2.diagSet ⊆ t

Tactic:
sdiff_le

Premises used: sdiff_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
⊢ t \ Sym2.diagSet ⊆ t

Tactic:
exact sdiff_le

Premises used: sdiff_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
rw : Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)
| Disjoint G.edgeSet s

Tactic:
rw [← Set.diff_union_inter s Sym2.diagSet]

Premises used: Set.diff_union_inter, Sym2.diagSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
conv_rhs : Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)
⊢ Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet s

Tactic:
conv_rhs => rw [← Set.diff_union_inter s Sym2.diagSet]

Premises used: Set.diff_union_inter, Sym2.diagSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
rw : Disjoint G.edgeSet (s \ Sym2.diagSet) ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)
⊢ Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)

Tactic:
rw [← disjoint_edgeSet, edgeSet_fromEdgeSet]

Premises used: SimpleGraph.edgeSet_fromEdgeSet, SimpleGraph.disjoint_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G.edgeSet (s \ Sym2.diagSet) ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)

Tactic:
grind [edgeSet_subset_compl_diagSet]

Premises used: SimpleGraph.edgeSet_subset_compl_diagSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
rw : Disjoint G (fromEdgeSet s) ↔ Disjoint s G.edgeSet
rw₁ : Disjoint G.edgeSet s ↔ Disjoint s G.edgeSet
rw₂ rw₃ : Disjoint s G.edgeSet ↔ Disjoint s G.edgeSet
⊢ Disjoint (fromEdgeSet s) G ↔ Disjoint s G.edgeSet

Tactic:
rw [disjoint_comm, disjoint_fromEdgeSet, disjoint_comm]

Premises used: disjoint_comm, SimpleGraph.disjoint_fromEdgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
s : Set (Sym2 V)
inst : DecidableEq V
inst_1 : Fintype (↑s : Type u)
rw : Fintype (↑(s \ Sym2.diagSet) : Type u)
⊢ Fintype (↑(fromEdgeSet s).edgeSet : Type u)

Tactic:
rw [edgeSet_fromEdgeSet s]

Premises used: SimpleGraph.edgeSet_fromEdgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
s : Set (Sym2 V)
inst : DecidableEq V
inst_1 : Fintype (↑s : Type u)
⊢ Fintype (↑(s \ Sym2.diagSet) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G H : SimpleGraph V
⊢ Disjoint G H ↔ ∀ (x y : V), G.Adj x y → ¬H.Adj x y

Tactic:
simp [← disjoint_edgeSet, Set.disjoint_left, Sym2.forall]

Premises used: Set.disjoint_left, SimpleGraph.disjoint_edgeSet, Sym2.forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ G.incidenceSet v ⊆ G.edgeSet

Tactic:
fun _ h => h.1

Premises used: Set.Subset, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b c : V
⊢ s(b, c) ∈ G.incidenceSet a ↔ G.Adj b c ∧ (a = b ∨ a = c)

Tactic:
and_congr_right' Sym2.mem_iff

Premises used: SimpleGraph.incidenceSet, and_congr_right', Set.Mem, setOf, Sym2.mem_iff, Sym2.fromRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
⊢ s(a, b) ∈ G.incidenceSet a ↔ G.Adj a b

Tactic:
and_iff_left <| Sym2.mem_mk_left _ _

Premises used: SimpleGraph.incidenceSet, Set.Mem, setOf, and_iff_left, Sym2.mem_mk_left, Sym2.fromRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
⊢ s(a, b) ∈ G.incidenceSet b ↔ G.Adj a b

Tactic:
and_iff_left <| Sym2.mem_mk_right _ _

Premises used: SimpleGraph.incidenceSet, Sym2.mem_mk_right, Set.Mem, setOf, and_iff_left, Sym2.fromRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a : V
e : (↑G.edgeSet : Type u)
⊢ (↑e : Sym2 V) ∈ G.incidenceSet a ↔ a ∈ (↑e : Sym2 V)

Tactic:
and_iff_right e.2

Premises used: SimpleGraph.incidenceSet, Set.Mem, setOf, and_iff_right, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : a ≠ b
⊢ G.incidenceSet a ∩ G.incidenceSet b ⊆ {s(a, b)}

Tactic:
fun _e he =>
  (Sym2.mem_and_mem_iff h).1 ⟨he.1.2, he.2.2⟩

Premises used: Set.Mem, setOf, Sym2.mem_and_mem_iff, Set.Subset, And.right, And.left, And.intro, Set.singleton, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ G.incidenceSet a ∩ G.incidenceSet b = {s(a, b)}

Tactic:
(G.incidenceSet_inter_incidenceSet_subset <| h.ne).antisymm ?_

Premises used: SimpleGraph.Adj.ne, SimpleGraph.incidenceSet_inter_incidenceSet_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
refine : {s(a, b)} ⊆ G.incidenceSet a ∩ G.incidenceSet b
⊢ G.incidenceSet a ∩ G.incidenceSet b = {s(a, b)}

Tactic:
refine (G.incidenceSet_inter_incidenceSet_subset <| h.ne).antisymm ?_

Premises used: SimpleGraph.Adj.ne, SimpleGraph.incidenceSet_inter_incidenceSet_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ s(a, b) ∈ G.incidenceSet a ∩ G.incidenceSet b

Tactic:
⟨G.mk'_mem_incidenceSet_left_iff.2 h, G.mk'_mem_incidenceSet_right_iff.2 h⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.inter, And.intro, SimpleGraph.mk'_mem_incidenceSet_left_iff, SimpleGraph.mk'_mem_incidenceSet_right_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ s(a, b) ∈ G.incidenceSet a ∩ G.incidenceSet b

Tactic:
exact ⟨G.mk'_mem_incidenceSet_left_iff.2 h, G.mk'_mem_incidenceSet_right_iff.2 h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
e : Sym2 V
h : a ≠ b
ha : e ∈ G.incidenceSet a
hb : e ∈ G.incidenceSet b
rwa : s(a, b) ∈ G.incidenceSet a
rwa₁ rwa₂ rwa₃ rwa₄ : e ∈ G.incidenceSet a
⊢ G.Adj a b

Tactic:
rwa [← mk'_mem_incidenceSet_left_iff, ←
    Set.mem_singleton_iff.1 <| G.incidenceSet_inter_incidenceSet_subset h ⟨ha, hb⟩]

Premises used: SimpleGraph.incidenceSet_inter_incidenceSet_subset, Set.mem_singleton_iff, And.intro, SimpleGraph.mk'_mem_incidenceSet_left_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
simp_rw : ∀ x ∈ G.incidenceSet a, x ∉ G.incidenceSet b
⊢ G.incidenceSet a ∩ G.incidenceSet b = ∅

Tactic:
simp_rw [Set.eq_empty_iff_forall_notMem, Set.mem_inter_iff, not_and]

Premises used: Set.mem_inter_iff, Set.eq_empty_iff_forall_notMem, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
u : Sym2 V
ha : u ∈ G.incidenceSet a
hb : u ∈ G.incidenceSet b
⊢ False

Tactic:
h (G.adj_of_mem_incidenceSet hn ha hb)

Premises used: SimpleGraph.adj_of_mem_incidenceSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
u : Sym2 V
ha : u ∈ G.incidenceSet a
hb : u ∈ G.incidenceSet b
⊢ False

Tactic:
exact h (G.adj_of_mem_incidenceSet hn ha hb)

Premises used: SimpleGraph.adj_of_mem_incidenceSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ w ∈ G.neighborSet v ↔ G.Adj v w

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SimpleGraph.neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a : V
⊢ a ∉ G.neighborSet a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w

Tactic:
simp [incidenceSet]

Premises used: SimpleGraph.incidenceSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v

Tactic:
simp only [mem_incidenceSet, mem_neighborSet]

Premises used: SimpleGraph.mem_incidenceSet, SimpleGraph.mem_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
h₁ :
  ∀ (e' : Sym2 V), e' ∈ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) ↔ Membership.mem (γ := Set (Sym2 V)) {e} e'
⊢ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = {e}

Tactic:
ext e'
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e' ↔ e' = e

Tactic:
⟨fun h' => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h₁ : ∀ (h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'), e' = e
h₂ : e' = e → (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e' ↔ e' = e

Tactic:
refine ⟨fun h' => ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
h₁ : e' = s(v, Sym2.Mem.other h)
⊢ e' = e

Tactic:
rw [← Sym2.other_spec h]

Premises used: Sym2.other_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = s(v, Sym2.Mem.other h)

Tactic:
(Sym2.mem_and_mem_iff (edge_other_ne G he h).symm).mp ⟨h'.1.2, h'.2.2⟩

Premises used: Sym2.mem_and_mem_iff, Ne.symm, And.right, And.left, And.intro, Iff.mp, SimpleGraph.edge_other_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = s(v, Sym2.Mem.other h)

Tactic:
exact (Sym2.mem_and_mem_iff (edge_other_ne G he h).symm).mp ⟨h'.1.2, h'.2.2⟩

Premises used: Sym2.mem_and_mem_iff, Ne.symm, And.right, And.left, And.intro, Iff.mp, SimpleGraph.edge_other_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
e' : Sym2 V
he : e' ∈ G.edgeSet
h : v ∈ e'
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'

Tactic:
⟨⟨he, h⟩, he, Sym2.other_mem _⟩

Premises used: Sym2.other_mem, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
e' : Sym2 V
he : e' ∈ G.edgeSet
h : v ∈ e'
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'

Tactic:
exact ⟨⟨he, h⟩, he, Sym2.other_mem _⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
rw : G.neighborSet v ∩ Gᶜ.neighborSet v ⊆ ∅
⊢ Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)

Tactic:
rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : w ∈ Gᶜ.neighborSet v
⊢ v ≠ w ∧ ¬G.Adj v w

Tactic:
rw [mem_neighborSet, compl_adj] at h'

Premises used: SimpleGraph.compl_adj, SimpleGraph.mem_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : v ≠ w ∧ ¬G.Adj v w
⊢ Membership.mem (γ := Set V) ∅ w

Tactic:
h'.2 h

Premises used: Set.Mem, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : v ≠ w ∧ ¬G.Adj v w
⊢ Membership.mem (γ := Set V) ∅ w

Tactic:
exact h'.2 h

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
h : ∀ (w : V), w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ Membership.mem (γ := Set V) {v}ᶜ w
⊢ G.neighborSet v ∪ Gᶜ.neighborSet v = {v}ᶜ

Tactic:
ext w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ ∀ {a b : V} (h : G.Adj a b), a ≠ b

Tactic:
have h := @ne_of_adj _ G
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
h₁ : G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ Membership.mem (γ := Set V) {v}ᶜ w

Tactic:
simp_rw [Set.mem_union, mem_neighborSet, compl_adj, Set.mem_compl_iff, Set.mem_singleton_iff]

Premises used: Set.mem_union, SimpleGraph.compl_adj, SimpleGraph.mem_neighborSet, Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
h₁ : G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w → ¬w = v
h₂ : ¬w = v → G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w
h₃ : G.Adj v w → ¬w = v
h₄ : v ≠ w → ¬G.Adj v w → ¬w = v
h₅ : G.Adj v w → ¬w = v
h₆ : v ≠ w → ¬G.Adj v w → ¬w = v
h₇ : G.Adj v w → w = v → False
h₈ : v ≠ w → ¬G.Adj v w → w = v → False
h₉ h₁₀ : ¬w = v → G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w
h₁₁ : ¬w = v → ¬G.Adj v w → v ≠ w
h₁₂ : ¬w = v → ¬G.Adj v w → ¬G.Adj v w
h₁₃ h₁₄ h₁₅ : G.Adj v w → w = v → False
h₁₆ h₁₇ h₁₈ : v ≠ w → ¬G.Adj v w → w = v → False
h₁₉ h₂₀ h₂₁ : ¬w = v → ¬G.Adj v w → v = w → False
h₂₂ h₂₃ h₂₄ : G.Adj v w → w = v → False
h₂₅ h₂₆ h₂₇ : v ≠ w → ¬G.Adj v w → w = v → False
h₂₈ h₂₉ h₃₀ : ¬w = v → ¬G.Adj v w → v = w → False
h₃₁ h₃₂ : G.Adj v w → w = v → False
h₃₃ h₃₄ : v ≠ w → ¬G.Adj v w → w = v → False
h₃₅ h₃₆ : ¬w = v → ¬G.Adj v w → v = w → False
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
simp_rw : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
simp_rw₁ : card (α := V) (Set.toFinset {v})ᶜ = Fintype.card V - 1
simp_rw₂ : Fintype.card V - card (α := V) (Set.toFinset {v}) = Fintype.card V - 1
simp_rw₃ : Fintype.card V - Fintype.card.{u} (↑{v} : Type u) = Fintype.card V - 1
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1

Tactic:
simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]

Premises used: Set.toFinset_compl, Finset.card_compl, SimpleGraph.neighborSet_union_compl_neighborSet_eq, Set.toFinset_card, Set.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
classical : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
classical₁ : card (α := V) (Set.toFinset {v})ᶜ = Fintype.card V - 1
classical₂ : Fintype.card V - card (α := V) (Set.toFinset {v}) = Fintype.card V - 1
classical₃ : Fintype.card V - Fintype.card.{u} (↑{v} : Type u) = Fintype.card V - 1
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1

Tactic:
classical simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]

Premises used: Set.toFinset_compl, Finset.card_compl, SimpleGraph.neighborSet_union_compl_neighborSet_eq, Set.toFinset_card, Set.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
h : ∀ (w : V), w ∈ Gᶜ.neighborSet v ↔ w ∈ (G.neighborSet v)ᶜ \ {v}
⊢ Gᶜ.neighborSet v = (G.neighborSet v)ᶜ \ {v}

Tactic:
ext w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ w ∈ Gᶜ.neighborSet v ↔ w ∈ (G.neighborSet v)ᶜ \ {v}

Tactic:
simp [and_comm, eq_comm]

Premises used: and_comm, eq_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.commonNeighbors v w = G.neighborSet v ∩ G.neighborSet w

Tactic:
rfl

Premises used: SimpleGraph.commonNeighbors, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
⊢ u ∈ G.commonNeighbors v w ↔ G.Adj v u ∧ G.Adj w u

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SimpleGraph.neighborSet, SimpleGraph.commonNeighbors, Set.inter
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.commonNeighbors v w = G.commonNeighbors w v

Tactic:
Set.inter_comm _ _

Premises used: SimpleGraph.commonNeighbors, Set.inter_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ v ∉ G.commonNeighbors v w

Tactic:
fun h =>
  ne_of_adj G h.1 rfl

Premises used: SimpleGraph.ne_of_adj, And.left, Not, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ w ∉ G.commonNeighbors v w

Tactic:
fun h =>
  ne_of_adj G h.2 rfl

Premises used: SimpleGraph.ne_of_adj, And.right, Not, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.commonNeighbors v w ⊆ G.neighborSet v

Tactic:
Set.inter_subset_left

Premises used: SimpleGraph.commonNeighbors, Set.inter_subset_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.commonNeighbors v w ⊆ G.neighborSet w

Tactic:
Set.inter_subset_right

Premises used: SimpleGraph.commonNeighbors, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
v w : V
h : ∀ (u : V), u ∈ commonNeighbors ⊤ v w ↔ Membership.mem (γ := Set V) (Set.univ \ {v, w}) u
⊢ commonNeighbors ⊤ v w = Set.univ \ {v, w}

Tactic:
ext u
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
v w u : V
⊢ u ∈ commonNeighbors ⊤ v w ↔ Membership.mem (γ := Set V) (Set.univ \ {v, w}) u

Tactic:
simp [commonNeighbors, eq_comm, not_or]

Premises used: SimpleGraph.commonNeighbors, eq_comm, not_or
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
right : G.otherVertexOfIncident h ∈ e
⊢ e ∈ G.incidenceSet (G.otherVertexOfIncident h)

Tactic:
use h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ G.otherVertexOfIncident h ∈ e

Tactic:
simp [otherVertexOfIncident, Sym2.other_mem']

Premises used: Sym2.other_mem', SimpleGraph.otherVertexOfIncident
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ e ∈ G.edgeSet

Tactic:
obtain ⟨he, hv⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
he : e ∈ G.edgeSet
⊢ v ∈ e

Tactic:
obtain ⟨he, hv⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e
rwa : ∀ (he_1 : s(v, Sym2.Mem.other' hv) ∈ G.edgeSet), G.otherVertexOfIncident ⋯ ∈ G.neighborSet v
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (he_1 : G.Adj v (Sym2.Mem.other' hv)), G.otherVertexOfIncident ⋯ ∈ G.neighborSet v
⊢ G.otherVertexOfIncident ⋯ ∈ G.neighborSet v

Tactic:
rwa [← Sym2.other_spec' hv, mem_edgeSet] at he

Premises used: Sym2.other_spec', SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v w : V
h : w ∈ G.neighborSet v
⊢ G.otherVertexOfIncident ⋯ = w

Tactic:
Sym2.congr_right.mp (Sym2.other_spec' (G.mem_incidence_iff_neighbor.mpr h).right)

Premises used: Iff.mpr, SimpleGraph.mem_incidence_iff_neighbor, And.right, Iff.mp, Sym2.other_spec', Sym2.congr_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w : V
e : Sym2 V
inst : DecidableEq V
v : V
x : (↑(G.incidenceSet v) : Type u)
⊢ (fun (w : (↑(G.neighborSet v) : Type u)) ↦ Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.incidenceSet v) s(v, (↑w : V)) ⋯)
      ((fun (e : (↑(G.incidenceSet v) : Type u)) ↦
          Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) (G.otherVertexOfIncident ⋯) ⋯)
        x) =
    x

Tactic:
simp [otherVertexOfIncident]

Premises used: SimpleGraph.otherVertexOfIncident
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
inst : DecidableEq V
v : V
x : (↑(G.neighborSet v) : Type u)
w : V
hw : w ∈ G.neighborSet v
simp : G.otherVertexOfIncident (v := v) (e := s(v, w)) ⋯ = w
⊢ (fun (e : (↑(G.incidenceSet v) : Type u)) ↦
        Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) (G.otherVertexOfIncident ⋯) ⋯)
      ((fun (w : (↑(G.neighborSet v) : Type u)) ↦
          Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.incidenceSet v) s(v, (↑w : V)) ⋯)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w hw)) =
    Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w hw

Tactic:
simp only [Subtype.mk.injEq]

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
inst : DecidableEq V
v : V
x : (↑(G.neighborSet v) : Type u)
w : V
hw : w ∈ G.neighborSet v
⊢ G.otherVertexOfIncident (v := v) (e := s(v, w)) ⋯ = w

Tactic:
incidence_other_neighbor_edge _ hw

Premises used: SimpleGraph.incidence_other_neighbor_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
inst : DecidableEq V
v : V
x : (↑(G.neighborSet v) : Type u)
w : V
hw : w ∈ G.neighborSet v
⊢ G.otherVertexOfIncident (v := v) (e := s(v, w)) ⋯ = w

Tactic:
exact incidence_other_neighbor_edge _ hw

Premises used: SimpleGraph.incidence_other_neighbor_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
⊢ Disjoint s t

Tactic:
Set.disjoint_left.mpr fun v hv₁ hv₂ ↦ (G.loopless.irrefl v) (h hv₁ hv₂)

Premises used: Iff.mpr, Std.Irrefl.irrefl, Set.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
⊢ Subsingleton.{u + 1} (SimpleGraph V) ↔ Subsingleton V

Tactic:
⟨fun h ↦ ?_, fun _ ↦ Unique.instSubsingleton⟩

Premises used: Unique.instSubsingleton, Iff.intro