awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
v w : V
⊢ Adj ⊥ v w ↔ False

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
⊢ completeGraph V = ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
⊢ emptyGraph V = ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
⊢ G = ⊥ ↔ ∀ (a b : V), ¬G.Adj a b

Tactic:
simp [← le_bot_iff, le_iff_adj]

Premises used: le_bot_iff, SimpleGraph.le_iff_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
⊢ G ≠ ⊥ ↔ ∃ (a : V) (b : V), G.Adj a b

Tactic:
simp [eq_bot_iff_forall_not_adj]

Premises used: SimpleGraph.eq_bot_iff_forall_not_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
⊢ G = ⊤ ↔ ∀ (a b : V), a ≠ b → G.Adj a b

Tactic:
simp [← top_le_iff, le_iff_adj]

Premises used: SimpleGraph.le_iff_adj, top_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
⊢ G ≠ ⊤ ↔ ∃ (a : V) (b : V), a ≠ b ∧ ¬G.Adj a b

Tactic:
simp [eq_top_iff_forall_ne_adj]

Premises used: SimpleGraph.eq_top_iff_forall_ne_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v w : V
e : Sym2 V
inst : Subsingleton V
G : SimpleGraph V
Adj : ∀ (a b : V), G.Adj a b ↔ SimpleGraph.Adj ⊥ a b
⊢ G = ⊥

Tactic:
ext a b
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a_1 b_1 c u v w : V
e : Sym2 V
inst : Subsingleton V
G : SimpleGraph V
a b : V
⊢ a = b

Tactic:
have := Subsingleton.elim a b
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a_1 b_1 c u v w : V
e : Sym2 V
inst : Subsingleton V
G : SimpleGraph V
a b : V
this : a = b
⊢ G.Adj a b ↔ Adj ⊥ a b

Tactic:
simp [this]
-- 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
inst : Nontrivial V
h : Eq.{u + 1} (α := SimpleGraph V) ⊥ ⊤
⊢ ∀ (a b : V), a = b

Tactic:
simpa only [← adj_inj, funext_iff, bot_adj,
    top_adj, ne_eq, eq_iff_iff, false_iff, not_not] using h

Premises used: Classical.not_not, funext_iff, SimpleGraph.top_adj, false_iff, ne_eq, SimpleGraph.bot_adj, SimpleGraph.adj_inj, eq_iff_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ v ∈ G.support ↔ ∃ (w : V), G.Adj v w

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SetRel.dom, SimpleGraph.support
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
⊢ u ∈ G.support

Tactic:
G.mem_support.mpr ⟨v, hadj⟩

Premises used: Iff.mpr, SimpleGraph.mem_support, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
⊢ v ∈ G.support

Tactic:
hadj.symm.mem_support_left

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Adj.mem_support_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
⊢ G.support ⊆ G'.support

Tactic:
SetRel.dom_mono fun _uv huv ↦ h huv

Premises used: SimpleGraph.support, SetRel.dom_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
⊢ u ∈ G.support

Tactic:
⟨v, hadj⟩

Premises used: Set.Mem, setOf, SetRel.dom, SimpleGraph.support, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
⊢ v ∈ G.support

Tactic:
hadj.symm.left_mem_support

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Adj.left_mem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
inst : Nontrivial V
⊢ Eq.{u + 1} (α := Set V) (support ⊤) Set.univ

Tactic:
Set.eq_univ_of_forall fun v₁ => exists_ne v₁ |>.imp fun _v₂ h => h.symm

Premises used: exists_ne, Exists.imp, Set.eq_univ_of_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
⊢ Eq.{u + 1} (α := Set V) (support ⊥) ∅

Tactic:
SetRel.dom_eq_empty_iff.mpr <| Set.empty_def.symm

Premises used: Iff.mpr, Set.empty_def, SimpleGraph.support, SetRel.dom_eq_empty_iff, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
⊢ G.support = ∅ ↔ G = ⊥

Tactic:
⟨fun h ↦ eq_bot_iff_forall_not_adj.mpr fun v w nadj ↦
    Set.ext_iff.mp (SetRel.dom_eq_empty_iff.mp h) (v, w) |>.mp nadj |>.elim,
   (· ▸ support_bot)⟩

Premises used: Iff.mpr, False.elim, Eq.rec, Prod.mk, SimpleGraph.support_bot, SimpleGraph.eq_bot_iff_forall_not_adj, Iff.intro, Iff.mp, SetRel.dom_eq_empty_iff, Set.ext_iff, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
⊢ G.support = ∅

Tactic:
uniqueOfSubsingleton.uniq G ▸ support_bot

Premises used: Eq.rec, SimpleGraph.uniqueOfSubsingleton, SimpleGraph.support_bot, Unique.uniq, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ⊆ G.support

Tactic:
fun _ hadj ↦ ⟨v, hadj.symm⟩

Premises used: SimpleGraph.Adj.symm, Set.Mem, setOf, SetRel.dom, Set.Subset, SimpleGraph.support, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ s(v, w) ∈ G.edgeSet ↔ G.Adj v w

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Sym2.fromRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
e : Sym2 V
⊢ e ∈ G.edgeSet → ¬e.IsDiag

Tactic:
Sym2.ind (fun _ _ => Adj.ne) e

Premises used: Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
e : Sym2 V
⊢ e.IsDiag → e ∉ G.edgeSet

Tactic:
imp_not_comm.1 G.not_isDiag_of_mem_edgeSet

Premises used: imp_not_comm, Iff.mp, SimpleGraph.not_isDiag_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ G₁.edgeSet = G₂.edgeSet ↔ G₁ = G₂

Tactic:
(edgeSetEmbedding V).eq_iff_eq

Premises used: SimpleGraph.edgeSetEmbedding, OrderEmbedding.eq_iff_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ G₁.edgeSet ⊆ G₂.edgeSet ↔ G₁ ≤ G₂

Tactic:
(edgeSetEmbedding V).le_iff_le

Premises used: SimpleGraph.edgeSetEmbedding, OrderEmbedding.le_iff_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ G₁.edgeSet ⊂ G₂.edgeSet ↔ G₁ < G₂

Tactic:
(edgeSetEmbedding V).lt_iff_lt

Premises used: SimpleGraph.edgeSetEmbedding, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
⊢ Injective.{u + 1, u + 1} (α := SimpleGraph V) edgeSet

Tactic:
(edgeSetEmbedding V).injective

Premises used: RelEmbedding.injective, SimpleGraph.edgeSetEmbedding
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
⊢ Eq.{u + 1} (α := Set (Sym2 V)) (edgeSet ⊥) ∅

Tactic:
Sym2.fromRel_bot

Premises used: setOf, Sym2.fromRel_bot, Sym2.fromRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
⊢ Eq.{u + 1} (α := Set (Sym2 V)) (edgeSet ⊤) Sym2.diagSetᶜ

Tactic:
Sym2.diagSet_compl_eq_fromRel_ne.symm

Premises used: setOf, Sym2.diagSet_compl_eq_fromRel_ne, Sym2.fromRel, Eq.symm, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
⊢ G.edgeSet ⊆ Sym2.diagSetᶜ

Tactic:
simpa [Set.subset_compl_iff_disjoint_left, edgeSet, edgeSetEmbedding] using G.loopless

Premises used: SimpleGraph.edgeSet, Set.subset_compl_iff_disjoint_left, SimpleGraph.edgeSetEmbedding, SimpleGraph.loopless
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
h :
  ∀ (x : Sym2 V) (x y : V),
    Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊔ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∪ G₂.edgeSet
⊢ (G₁ ⊔ G₂).edgeSet = G₁.edgeSet ∪ G₂.edgeSet

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
x_1 : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊔ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∪ G₂.edgeSet

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
h :
  ∀ (x : Sym2 V) (x y : V),
    Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊓ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∩ G₂.edgeSet
⊢ (G₁ ⊓ G₂).edgeSet = G₁.edgeSet ∩ G₂.edgeSet

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
x_1 : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊓ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∩ G₂.edgeSet

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
h :
  ∀ (x : Sym2 V) (x y : V),
    Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ \ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet \ G₂.edgeSet
⊢ (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
x_1 : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ \ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet \ G₂.edgeSet

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
rw : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ Disjoint G₁ G₂
rw₁ : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₂ : (G₁ ⊓ G₂).edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₃ : (G₁ ⊓ G₂).edgeSet ⊆ edgeSet ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₄ : (G₁ ⊓ G₂).edgeSet ≤ edgeSet ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₅ rw₆ : G₁ ⊓ G₂ ≤ ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂

Tactic:
rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
    OrderEmbedding.le_iff_le]

Premises used: SimpleGraph.edgeSet_bot, SimpleGraph.edgeSet_inf, Set.le_iff_subset, disjoint_iff_inf_le, OrderEmbedding.le_iff_le, Set.disjoint_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
rw : G.edgeSet = edgeSet ⊥ ↔ G = ⊥
rw₁ rw₂ : G = ⊥ ↔ G = ⊥
⊢ G.edgeSet = ∅ ↔ G = ⊥

Tactic:
rw [← edgeSet_bot, edgeSet_inj]

Premises used: SimpleGraph.edgeSet_bot, SimpleGraph.edgeSet_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
rw : G.edgeSet ≠ ∅ ↔ G ≠ ⊥
rw₁ rw₂ : G ≠ ⊥ ↔ G ≠ ⊥
⊢ G.edgeSet.Nonempty ↔ G ≠ ⊥

Tactic:
rw [Set.nonempty_iff_ne_empty, edgeSet_eq_empty.ne]

Premises used: Iff.ne, Set.nonempty_iff_ne_empty, SimpleGraph.edgeSet_eq_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.edgeSet \ (s \ Sym2.diagSet) = G.edgeSet \ s

Tactic:
grind [Sym2.mem_diagSet, not_isDiag_of_mem_edgeSet]

Premises used: SimpleGraph.not_isDiag_of_mem_edgeSet, Sym2.mem_diagSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ s(v, w) ∈ G.edgeSet ∧ v ∈ s(v, w) ∧ w ∈ s(v, w)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
refine : (v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e) → G.Adj v w
⊢ G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e

Tactic:
refine ⟨fun _ => ⟨G.ne_of_adj ‹_›, s(v, w), by simpa⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e ∧ w ∈ e
⊢ e = s(v, w)

Tactic:
rw [Sym2.mem_and_mem_iff hne] at hv

Premises used: Sym2.mem_and_mem_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : e = s(v, w)
⊢ s(v, w) ∈ G.edgeSet

Tactic:
subst e
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
he : s(v, w) ∈ G.edgeSet
rwa rwa₁ rwa₂ rwa₃ : ∀ (he : G.Adj v w), G.Adj v w
⊢ G.Adj v w

Tactic:
rwa [mem_edgeSet] at he

Premises used: SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
⊢ G.Adj a b ↔ ∃ (e : (↑G.edgeSet : Type u)), (↑e : Sym2 V) = s(a, b)

Tactic:
simp only [mem_edgeSet, exists_prop, SetCoe.exists, exists_eq_right]

Premises used: exists_eq_right, SetCoe.exists, exists_prop, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ G.edgeSet ⊆ s.sym2 ↔ G.support ⊆ s

Tactic:
⟨fun h u hu ↦ ?_, fun h e hadj ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set V
refine_1 : ∀ (h : G.edgeSet ⊆ s.sym2) (u : V) (hu : u ∈ G.support), u ∈ s
refine_2 : ∀ (h : G.support ⊆ s) (e : Sym2 V) (hadj : e ∈ G.edgeSet), e ∈ s.sym2
⊢ G.edgeSet ⊆ s.sym2 ↔ G.support ⊆ s

Tactic:
refine ⟨fun h u hu ↦ ?_, fun h e hadj ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h : G.edgeSet ⊆ s.sym2
u : V
hu : u ∈ G.support
refine_1 :
  ∀ (v : V)
    (huv :
      Membership.mem (γ := SetRel V V)
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (u, v) => G.Adj u v}
        (u, v)),
    u ∈ s
⊢ u ∈ s

Tactic:
have ⟨v, huv⟩ := hu
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h : G.edgeSet ⊆ s.sym2
u : V
hu : u ∈ G.support
v : V
huv :
  Membership.mem (γ := SetRel V V)
    {x : V × V |
      match (motive := V × V → Prop) x with
      | (u, v) => G.Adj u v}
    (u, v)
⊢ u ∈ s

Tactic:
(Set.mk_mem_sym2_iff.mp <| h huv).left

Premises used: And.left, Iff.mp, Set.mk_mem_sym2_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h : G.edgeSet ⊆ s.sym2
u : V
hu : u ∈ G.support
v : V
huv :
  Membership.mem (γ := SetRel V V)
    {x : V × V |
      match (motive := V × V → Prop) x with
      | (u, v) => G.Adj u v}
    (u, v)
⊢ u ∈ s

Tactic:
exact (Set.mk_mem_sym2_iff.mp <| h huv).left

Premises used: And.left, Iff.mp, Set.mk_mem_sym2_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
e : Sym2 V
hadj : e ∈ G.edgeSet
refine_2 : ∀ (x y : V) (hadj : s(x, y) ∈ G.edgeSet), s(x, y) ∈ s.sym2
⊢ e ∈ s.sym2

Tactic:
cases e
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
x y : V
hadj : s(x, y) ∈ G.edgeSet
⊢ s(x, y) ∈ s.sym2

Tactic:
⟨h hadj.mem_support_left, h hadj.mem_support_right⟩

Premises used: Set.Mem, SimpleGraph.Adj.mem_support_left, setOf, SimpleGraph.Adj.mem_support_right, Set.sym2, And.intro, Sym2.fromRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
x y : V
hadj : s(x, y) ∈ G.edgeSet
⊢ s(x, y) ∈ s.sym2

Tactic:
exact ⟨h hadj.mem_support_left, h hadj.mem_support_right⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
e : Sym2 V
he : e ∈ G.edgeSet
v : V
h : v ∈ e
⊢ s(Sym2.Mem.other h, v) ∈ G.edgeSet

Tactic:
rw [← Sym2.other_spec h, Sym2.eq_swap] at he

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

Tactic:
G.ne_of_adj he

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

Tactic:
exact G.ne_of_adj he

Premises used: SimpleGraph.ne_of_adj
-- 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
G₁ G₂ : SimpleGraph V
rw : Fintype (↑∅ : Type u)
⊢ Fintype (↑(edgeSet ⊥) : Type u)

Tactic:
rw [edgeSet_bot]

Premises used: SimpleGraph.edgeSet_bot
-- 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
G₁ G₂ : SimpleGraph V
⊢ Fintype (↑∅ : Type u)

Tactic:
infer_instance
-- 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
G₁ G₂ : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G₁.edgeSet : Type u)
inst_2 : Fintype (↑G₂.edgeSet : Type u)
rw : Fintype (↑(G₁.edgeSet ∪ G₂.edgeSet) : Type u)
⊢ Fintype (↑(G₁ ⊔ G₂).edgeSet : Type u)

Tactic:
rw [edgeSet_sup]

Premises used: SimpleGraph.edgeSet_sup
-- 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
G₁ G₂ : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G₁.edgeSet : Type u)
inst_2 : Fintype (↑G₂.edgeSet : Type u)
⊢ Fintype (↑(G₁.edgeSet ∪ G₂.edgeSet) : Type u)

Tactic:
infer_instance
-- 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
G₁ G₂ : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G₁.edgeSet : Type u)
inst_2 : Fintype (↑G₂.edgeSet : Type u)
rw : Fintype (↑(G₁.edgeSet ∩ G₂.edgeSet) : Type u)
⊢ Fintype (↑(G₁ ⊓ G₂).edgeSet : Type u)

Tactic:
rw [edgeSet_inf]

Premises used: SimpleGraph.edgeSet_inf
-- 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
G₁ G₂ : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G₁.edgeSet : Type u)
inst_2 : Fintype (↑G₂.edgeSet : Type u)
⊢ Fintype (↑(G₁.edgeSet ∩ G₂.edgeSet) : Type u)

Tactic:
exact Set.fintypeInter _ _

Premises used: Set.fintypeInter
-- 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
G₁ G₂ : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G₁.edgeSet : Type u)
inst_2 : Fintype (↑G₂.edgeSet : Type u)
rw : Fintype (↑(G₁.edgeSet \ G₂.edgeSet) : Type u)
⊢ Fintype (↑(G₁ \ G₂).edgeSet : Type u)

Tactic:
rw [edgeSet_sdiff]

Premises used: SimpleGraph.edgeSet_sdiff
-- 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
G₁ G₂ : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G₁.edgeSet : Type u)
inst_2 : Fintype (↑G₂.edgeSet : Type u)
⊢ Fintype (↑(G₁.edgeSet \ G₂.edgeSet) : Type u)

Tactic:
exact Set.fintypeDiff _ _

Premises used: Set.fintypeDiff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
v w : V
s : Set (Sym2 V)
⊢ (fromEdgeSet s).Adj v w ↔ s(v, w) ∈ s ∧ v ≠ w

Tactic:
Iff.rfl

Premises used: Iff.rfl, Sym2.ToRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s : Set (Sym2 V)
h : ∀ (e : Sym2 V), e ∈ (fromEdgeSet s).edgeSet ↔ e ∈ s \ Sym2.diagSet
⊢ (fromEdgeSet s).edgeSet = s \ Sym2.diagSet

Tactic:
ext e
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s : Set (Sym2 V)
e : Sym2 V
⊢ ∀ (x y : V), s(x, y) ∈ (fromEdgeSet s).edgeSet ↔ s(x, y) ∈ s \ Sym2.diagSet

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ (fromEdgeSet s).edgeSet ↔ e ∈ s \ Sym2.diagSet

Tactic:
exact Sym2.ind (by simp) e
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
Adj : ∀ (v w : V), (fromEdgeSet G.edgeSet).Adj v w ↔ G.Adj v w
⊢ fromEdgeSet G.edgeSet = G

Tactic:
ext v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ (fromEdgeSet G.edgeSet).Adj v w ↔ G.Adj v w

Tactic:
⟨fun h => h.1, fun h => ⟨h, G.ne_of_adj h⟩⟩

Premises used: SimpleGraph.ne_of_adj, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ (fromEdgeSet G.edgeSet).Adj v w ↔ G.Adj v w

Tactic:
exact ⟨fun h => h.1, fun h => ⟨h, G.ne_of_adj h⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
simp : (∀ x ∈ G.edgeSet, x ∈ s ∧ ¬x.IsDiag) ↔ ∀ x ∈ G.edgeSet, x ∈ s
⊢ G ≤ fromEdgeSet s ↔ G.edgeSet ⊆ s

Tactic:
simp [← edgeSet_subset_edgeSet, Set.subset_def]

Premises used: Set.subset_def, SimpleGraph.edgeSet_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ (∀ x ∈ G.edgeSet, x ∈ s ∧ ¬x.IsDiag) ↔ ∀ x ∈ G.edgeSet, x ∈ s

Tactic:
grind [not_isDiag_of_mem_edgeSet]

Premises used: SimpleGraph.not_isDiag_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ fromEdgeSet s ≤ G ↔ s \ Sym2.diagSet ⊆ G.edgeSet

Tactic:
simp [← edgeSet_subset_edgeSet]

Premises used: SimpleGraph.edgeSet_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
⊢ G = fromEdgeSet G.edgeSet ∧ Disjoint G.edgeSet Sym2.diagSet

Tactic:
simp +contextual [Set.disjoint_right]

Premises used: Set.disjoint_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s : Set (Sym2 V)
hs : Disjoint s Sym2.diagSet
⊢ (fromEdgeSet s).edgeSet = s

Tactic:
simp [hs]
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
Adj : ∀ (v w : V), SimpleGraph.Adj (fromEdgeSet ∅) v w ↔ SimpleGraph.Adj ⊥ v w
⊢ Eq.{u + 1} (α := SimpleGraph V) (fromEdgeSet ∅) ⊥

Tactic:
ext v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
v w : V
⊢ Adj (fromEdgeSet ∅) v w ↔ Adj ⊥ v w

Tactic:
simp only [fromEdgeSet_adj, Set.mem_empty_iff_false, false_and, bot_adj]

Premises used: false_and, SimpleGraph.fromEdgeSet_adj, SimpleGraph.bot_adj, Set.mem_empty_iff_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
Adj : ∀ (x x_1 : V), SimpleGraph.Adj (fromEdgeSet Sym2.diagSetᶜ) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1
⊢ Eq.{u + 1} (α := SimpleGraph V) (fromEdgeSet Sym2.diagSetᶜ) ⊤

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
x x_1 : V
⊢ Adj (fromEdgeSet Sym2.diagSetᶜ) x x_1 ↔ Adj ⊤ x x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
Adj : ∀ (v w : V), SimpleGraph.Adj (fromEdgeSet Set.univ) v w ↔ SimpleGraph.Adj ⊤ v w
⊢ Eq.{u + 1} (α := SimpleGraph V) (fromEdgeSet Set.univ) ⊤

Tactic:
ext v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
v w : V
⊢ Adj (fromEdgeSet Set.univ) v w ↔ Adj ⊤ v w

Tactic:
simp only [fromEdgeSet_adj, Set.mem_univ, true_and, top_adj]

Premises used: SimpleGraph.fromEdgeSet_adj, SimpleGraph.top_adj, Set.mem_univ, true_and
-- 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 : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₁ : (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Adj₂ Adj₃ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₄ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ s
Adj₅ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
Adj₆ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ t
Adj₇ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
Adj₈ Adj₉ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Adj₁₀ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → s(v, w) ∈ s
Adj₁₁ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → s(v, w) ∈ t
Adj₁₂ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → ¬v = w
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w

Tactic:
tauto
-- 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
⊢ (fromEdgeSet (s ∪ t)).Adj v w ↔ (fromEdgeSet s ⊔ fromEdgeSet t).Adj v w

Tactic:
simp [Set.mem_union, or_and_right]

Premises used: Set.mem_union, or_and_right