awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a b : V
h : s(v, w) = s(a, b)
⊢ (a ∈ s(v, w)) = (a ∈ s(a, b))

Tactic:
apply_fun fun e ↦ a ∈ e at h

Premises used: Membership.mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a b : V
h : (a ∈ s(v, w)) = (a ∈ s(a, b))
⊢ a = v ∨ a = w

Tactic:
simp only [Sym2.mem_iff, true_or, eq_iff_iff, iff_true] at h

Premises used: true_or, iff_true, Sym2.mem_iff, eq_iff_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a b : V
h : a = v ∨ a = w
⊢ Membership.mem (γ := Set V) {v, w} a

Tactic:
h

Premises used: Set.insert, Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a b : V
h : a = v ∨ a = w
⊢ Membership.mem (γ := Set V) {v, w} a

Tactic:
exact h
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Std.Irrefl G'.Adj

Tactic:
⟨fun v h ↦ G.loopless.irrefl v (G'.adj_sub h)⟩

Premises used: Std.Irrefl.irrefl, SimpleGraph.Subgraph.adj_sub, Std.Irrefl.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v w : V
⊢ G'.Adj v w ↔ G'.Adj w v

Tactic:
⟨fun x ↦ G'.symm x, fun x ↦ G'.symm x⟩

Premises used: SimpleGraph.Subgraph.symm, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
u v : V
h : G'.Adj u v
⊢ G'.Adj v u

Tactic:
G'.symm h

Premises used: SimpleGraph.Subgraph.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ G.Adj u v

Tactic:
H.adj_sub h

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ u ∈ H.verts

Tactic:
H.edge_vert h

Premises used: SimpleGraph.Subgraph.edge_vert
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ v ∈ H.verts

Tactic:
h.symm.fst_mem

Premises used: SimpleGraph.Subgraph.Adj.symm, SimpleGraph.Subgraph.Adj.fst_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ u ≠ v

Tactic:
h.adj_sub.ne

Premises used: SimpleGraph.Adj.ne, SimpleGraph.Subgraph.Adj.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : s(u, v) = s(w, x)
⊢ u = w ∧ v = x ∨ u = x ∧ v = w

Tactic:
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h2

Premises used: Sym2.eq, Prod.swap_prod_mk, Sym2.rel_iff', Prod.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : u = w ∧ v = x ∨ u = x ∧ v = w
inl : ∀ (hl : u = w ∧ v = x), H.Adj u v ↔ H.Adj w x
inr : ∀ (hr : u = x ∧ v = w), H.Adj u v ↔ H.Adj w x
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
rcases h2 with hl | hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hl : u = w ∧ v = x
inl : H.Adj w v ↔ H.Adj w x
inl₁ inl₂ : H.Adj w x ↔ H.Adj w x
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
rw [hl.1, hl.2]

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
inr : H.Adj x v ↔ H.Adj w x
inr₁ : H.Adj x w ↔ H.Adj w x
inr₂ inr₃ : H.Adj w x ↔ H.Adj w x
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
rw [hr.1, hr.2, Subgraph.adj_comm]

Premises used: SimpleGraph.Subgraph.adj_comm, And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
u v : (↑G'.verts : Type u)
h : G'.Adj (↑u : V) (↑v : V)
⊢ G.Adj (↑u : V) (↑v : V)

Tactic:
G'.adj_sub h

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
u v : (↑G'.verts : Type u)
h : G'.coe.Adj u v
⊢ G.Adj (↑u : V) (↑v : V)

Tactic:
G'.adj_sub h

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ H.coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u ⋯) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v ⋯)

Tactic:
h
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.IsSpanning ↔ G'.verts = Set.univ

Tactic:
Set.eq_univ_iff_forall.symm

Premises used: Set.eq_univ_iff_forall, SimpleGraph.Subgraph.IsSpanning, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
Adj : ∀ (x x_1 : V), G'.coe.spanningCoe (s := G'.verts).Adj x x_1 ↔ G'.spanningCoe.Adj x x_1
⊢ G'.coe.spanningCoe (s := G'.verts) = G'.spanningCoe

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
Adj :
  (∃ (a : V) (h : a ∈ G'.verts) (a_1 : V) (h_1 : a_1 ∈ G'.verts),
      G'.coe.Adj (Subtype.mk (p := fun (a : V) ↦ a ∈ G'.verts) a ⋯)
          (Subtype.mk (p := fun (a : V) ↦ a ∈ G'.verts) a_1 ⋯) ∧
        a = x ∧ a_1 = x_1) ↔
    G'.spanningCoe.Adj x x_1
⊢ G'.coe.spanningCoe (s := G'.verts).Adj x x_1 ↔ G'.spanningCoe.Adj x x_1

Tactic:
simp only [map_adj, Function.Embedding.subtype_apply, Subtype.exists]

Premises used: Subtype.exists, SimpleGraph.map_adj, Function.Embedding.subtype_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
⊢ (∃ (a : V) (h : a ∈ G'.verts) (a_1 : V) (h_1 : a_1 ∈ G'.verts),
      G'.coe.Adj (Subtype.mk (p := fun (a : V) ↦ a ∈ G'.verts) a ⋯)
          (Subtype.mk (p := fun (a : V) ↦ a ∈ G'.verts) a_1 ⋯) ∧
        a = x ∧ a_1 = x_1) ↔
    G'.spanningCoe.Adj x x_1

Tactic:
grind [spanningCoe_adj, coe_adj, edge_vert, adj_symm]

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.coe_adj, SimpleGraph.Subgraph.spanningCoe_adj, SimpleGraph.Subgraph.adj_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
u v : (↑G'.verts : Type u)
h : G'.spanningCoe.Adj (↑u : V) (↑v : V)
⊢ G.Adj (↑u : V) (↑v : V)

Tactic:
G'.adj_sub h

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.spanningCoe ≤ G

Tactic:
fun _ _ ↦ G'.3

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
⊢ G₁.spanningCoe = G₂.spanningCoe ↔ G₁.Adj = G₂.Adj

Tactic:
simp [Subgraph.spanningCoe]

Premises used: SimpleGraph.Subgraph.spanningCoe
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
v w : V
s : Set V
G : SimpleGraph (↑s : Type u)
hadj : G.spanningCoe (s := s).Adj v w
⊢ v ∈ s

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hadj : G.Adj v w
Adj : ∀ (v_1 w_1 : V), (G.subgraphOfAdj hadj).spanningCoe.Adj v_1 w_1 ↔ SimpleGraph.Adj (fromEdgeSet {s(v, w)}) v_1 w_1
⊢ (G.subgraphOfAdj hadj).spanningCoe = fromEdgeSet {s(v, w)}

Tactic:
ext v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 : V
hadj : G.Adj v_1 w_1
v w : V
⊢ (G.subgraphOfAdj hadj).spanningCoe.Adj v w ↔ SimpleGraph.Adj (fromEdgeSet {s(v_1, w_1)}) v w

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
hG' : G'.IsInduced
a b : (↑G'.verts : Type u)
⊢ G'.Adj (↑a : V) (↑b : V) ↔ G.Adj (↑a : V) (↑b : V)

Tactic:
⟨coe_adj_sub _ _ _, hG' a.2 b.2⟩

Premises used: SimpleGraph.Subgraph.coe_adj_sub, Iff.intro, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
⊢ v ∈ H.support ↔ ∃ (w : V), H.Adj v w

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SetRel.dom, SimpleGraph.Subgraph.support
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.support ⊆ H.verts

Tactic:
fun _ ⟨_, h⟩ ↦ H.edge_vert h

Premises used: SimpleGraph.Subgraph.edge_vert, Membership.mem, Set.Subset, _private.0.SimpleGraph.Subgraph.support_subset_verts.match_1, SimpleGraph.Subgraph.verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
⊢ G'.neighborSet v ⊆ G.neighborSet v

Tactic:
fun _ ↦ G'.adj_sub

Premises used: Set.Mem, setOf, SimpleGraph.Subgraph.adj_sub, SimpleGraph.neighborSet, SimpleGraph.Subgraph.neighborSet, Set.Subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
⊢ G'.neighborSet v ⊆ G'.verts

Tactic:
fun _ h ↦ G'.edge_vert (adj_symm G' h)

Premises used: SimpleGraph.Subgraph.edge_vert, Set.Subset, SimpleGraph.Subgraph.adj_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v w : V
⊢ w ∈ G'.neighborSet v ↔ G'.Adj v w

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SimpleGraph.Subgraph.neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.edgeSet ⊆ G.edgeSet

Tactic:
Sym2.ind (fun _ _ ↦ G'.adj_sub)

Premises used: Set.Subset, Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v w : V
⊢ s(v, w) ∈ G'.edgeSet ↔ G'.Adj v w

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Sym2.fromRel, SimpleGraph.Subgraph.edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h :
  ∀ (e : Sym2 (↑G'.verts : Type u)),
    e ∈ G'.coe.edgeSet ↔
      Membership.mem (γ := Set (Sym2 (↑G'.verts : Type u)))
        (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' G'.edgeSet) e
⊢ G'.coe.edgeSet = Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' G'.edgeSet

Tactic:
ext e
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 (↑G'.verts : Type u)
h :
  ∀ (x y : (↑G'.verts : Type u)),
    s(x, y) ∈ G'.coe.edgeSet ↔
      Membership.mem (γ := Set (Sym2 (↑G'.verts : Type u)))
        (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' G'.edgeSet) s(x, y)
⊢ e ∈ G'.coe.edgeSet ↔
    Membership.mem (γ := Set (Sym2 (↑G'.verts : Type u)))
      (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' G'.edgeSet) e

Tactic:
induction e using Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x y : (↑G'.verts : Type u)
⊢ s(x, y) ∈ G'.coe.edgeSet ↔
    Membership.mem (γ := Set (Sym2 (↑G'.verts : Type u)))
      (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' G'.edgeSet) s(x, y)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
rw : G'.edgeSet ⊆ Set.range (ι := Sym2 (↑G'.verts : Type u)) (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)))
⊢ Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' G'.coe.edgeSet = G'.edgeSet

Tactic:
rw [edgeSet_coe, Set.image_preimage_eq_iff]

Premises used: SimpleGraph.Subgraph.edgeSet_coe, Set.image_preimage_eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
a b : V
he : s(a, b) ∈ G'.edgeSet
⊢ G'.Adj a b

Tactic:
rw [Subgraph.mem_edgeSet] at he

Premises used: SimpleGraph.Subgraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
a b : V
he : G'.Adj a b
⊢ Membership.mem (γ := Set (Sym2 V))
    (Set.range (ι := Sym2 (↑G'.verts : Type u)) (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)))) s(a, b)

Tactic:
⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_mk ..⟩

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.Adj.symm, Sym2.mk, Set.Mem, setOf, Subtype.mk, Sym2.map_mk, Exists.intro, Set.range
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
a b : V
he : G'.Adj a b
⊢ Membership.mem (γ := Set (Sym2 V))
    (Set.range (ι := Sym2 (↑G'.verts : Type u)) (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)))) s(a, b)

Tactic:
exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_mk ..⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
he : e ∈ G'.edgeSet
h :
  ∀ (a b : V) (he : s(a, b) ∈ G'.edgeSet),
    Membership.mem (γ := Set (Sym2 V))
      (Set.range (ι := Sym2 (↑G'.verts : Type u)) (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)))) s(a, b)
⊢ Membership.mem (γ := Set (Sym2 V))
    (Set.range (ι := Sym2 (↑G'.verts : Type u)) (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)))) e

Tactic:
induction e using Sym2.ind with | h a b =>
  rw [Subgraph.mem_edgeSet] at he
  exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_mk ..⟩

Premises used: SimpleGraph.Subgraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.spanningCoe.edgeSet = G'.edgeSet

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
v : V
he : e ∈ G'.edgeSet
hv : v ∈ e
h : ∀ (x y : V) (he : s(x, y) ∈ G'.edgeSet) (hv : v ∈ s(x, y)), v ∈ G'.verts
⊢ v ∈ G'.verts

Tactic:
induction e
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x y : V
he : s(x, y) ∈ G'.edgeSet
hv : v ∈ s(x, y)
h : ∀ (he : s(v, y) ∈ G'.edgeSet) (hv : v ∈ s(v, y)), v ∈ G'.verts
h₁ : ∀ (he : s(x, v) ∈ G'.edgeSet) (hv : v ∈ s(x, v)), v ∈ G'.verts
⊢ v ∈ G'.verts

Tactic:
rcases Sym2.mem_iff.mp hv with (rfl | rfl)

Premises used: Sym2.mem_iff, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v y : V
he : s(v, y) ∈ G'.edgeSet
hv : v ∈ s(v, y)
⊢ v ∈ G'.verts

Tactic:
G'.edge_vert he

Premises used: SimpleGraph.Subgraph.edge_vert
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v y : V
he : s(v, y) ∈ G'.edgeSet
hv : v ∈ s(v, y)
⊢ v ∈ G'.verts

Tactic:
exact G'.edge_vert he

Premises used: SimpleGraph.Subgraph.edge_vert
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x : V
he : s(x, v) ∈ G'.edgeSet
hv : v ∈ s(x, v)
⊢ v ∈ G'.verts

Tactic:
G'.edge_vert (G'.symm he)

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x : V
he : s(x, v) ∈ G'.edgeSet
hv : v ∈ s(x, v)
⊢ v ∈ G'.verts

Tactic:
exact G'.edge_vert (G'.symm he)

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
⊢ G'.incidenceSet v ⊆ G.incidenceSet v

Tactic:
fun _ h ↦ ⟨G'.edgeSet_subset h.1, h.2⟩

Premises used: SimpleGraph.incidenceSet, Set.Mem, setOf, Set.Subset, SimpleGraph.Subgraph.edgeSet_subset, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
⊢ G'.incidenceSet v ⊆ G'.edgeSet

Tactic:
fun _ h ↦ h.1

Premises used: Set.Subset, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
V'' : Set V
hV : V'' = G'.verts
adj' : V → V → Prop
hadj : adj' = G'.Adj
⊢ G'.copy V'' hV adj' hadj = G'

Tactic:
Subgraph.ext hV hadj

Premises used: SimpleGraph.Subgraph.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a_1 b_1 : V
s : Set G.Subgraph
a b : V
G' : G.Subgraph
hab : G'.Adj a b
⊢ G.Adj a b

Tactic:
G'.adj_sub hab

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a_1 b_1 : V
s : Set G.Subgraph
a b : V
G' : G.Subgraph
hab : G'.Adj a b
⊢ G.Adj a b

Tactic:
exact G'.adj_sub hab

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a_1 b_1 : V
s : Set G.Subgraph
a b : V
G' : G.Subgraph
hG' : G' ∈ s
hab : G'.Adj a b
⊢ Membership.mem (γ := Set V) (⋃ G' ∈ s, G'.verts) a

Tactic:
Set.mem_iUnion₂_of_mem hG' (G'.edge_vert hab)

Premises used: SimpleGraph.Subgraph.edge_vert, Set.mem_iUnion₂_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a_1 b_1 : V
s : Set G.Subgraph
a b : V
G' : G.Subgraph
hG' : G' ∈ s
hab : G'.Adj a b
⊢ Membership.mem (γ := Set V) (⋃ G' ∈ s, G'.verts) a

Tactic:
exact Set.mem_iUnion₂_of_mem hG' (G'.edge_vert hab)

Premises used: Set.mem_iUnion₂_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a_1 b_1 : V
s : Set G.Subgraph
a b : V
h : (fun (a b : V) ↦ ∃ G' ∈ s, G'.Adj a b) a b
⊢ (fun (a b : V) ↦ ∃ G' ∈ s, G'.Adj a b) b a

Tactic:
simpa [adj_comm] using h

Premises used: SimpleGraph.Subgraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
⊢ (G₁ ⊔ G₂).Adj a b ↔ G₁.Adj a b ∨ G₂.Adj a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
⊢ (G₁ ⊓ G₂).Adj a b ↔ G₁.Adj a b ∧ G₂.Adj a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
⊢ Adj (G := G) ⊤ a b ↔ G.Adj a b

Tactic:
Iff.rfl

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

Tactic:
not_false

Premises used: not_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
⊢ (G₁ ⊔ G₂).verts = G₁.verts ∪ G₂.verts

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
⊢ (G₁ ⊓ G₂).verts = G₁.verts ∩ G₂.verts

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ Eq.{u + 1} (α := Set V) (verts (G := G) ⊤) Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ Eq.{u + 1} (α := Set V) (verts (G := G) ⊥) ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G' = ⊥ ↔ G'.verts = ∅

Tactic:
⟨(· ▸ verts_bot), fun h ↦ Subgraph.ext (h ▸ verts_bot (G := G)) <|
    funext₂ fun _ _ ↦ propext ⟨fun h' ↦ (h ▸ h'.fst_mem :), False.elim⟩⟩

Premises used: False.elim, Eq.rec, SimpleGraph.Subgraph.ext, funext₂, Iff.intro, propext, SimpleGraph.Subgraph.Adj.fst_mem, Eq.symm, SimpleGraph.Subgraph.verts_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G' ≠ ⊥ ↔ G'.verts.Nonempty

Tactic:
G'.eq_bot_iff_verts_eq_empty.not.trans <| Set.nonempty_iff_ne_empty.symm

Premises used: Iff.not, Set.nonempty_iff_ne_empty, Iff.trans, SimpleGraph.Subgraph.eq_bot_iff_verts_eq_empty, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
⊢ (sSup s).Adj a b ↔ ∃ G_1 ∈ s, G_1.Adj a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
⊢ (sInf s).Adj a b ↔ (∀ G' ∈ s, G'.Adj a b) ∧ G.Adj a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
f : ι → G.Subgraph
⊢ Adj (G := G) (⨆ (i : ι), f i) a b ↔ ∃ (i : ι), (f i).Adj a b

Tactic:
simp [iSup]

Premises used: iSup
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
f : ι → G.Subgraph
⊢ Adj (G := G) (⨅ (i : ι), f i) a b ↔ (∀ (i : ι), (f i).Adj a b) ∧ G.Adj a b

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
hs : s.Nonempty
obtain : ∀ (G' : G.Subgraph) (hG' : G' ∈ s), (∀ G' ∈ s, G'.Adj a b) → G.Adj a b
⊢ (∀ G' ∈ s, G'.Adj a b) → G.Adj a b

Tactic:
obtain ⟨G', hG'⟩ := hs
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
G' : G.Subgraph
hG' : G' ∈ s
⊢ (∀ G' ∈ s, G'.Adj a b) → G.Adj a b

Tactic:
fun h => G'.adj_sub (h _ hG')

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
G' : G.Subgraph
hG' : G' ∈ s
⊢ (∀ G' ∈ s, G'.Adj a b) → G.Adj a b

Tactic:
exact fun h => G'.adj_sub (h _ hG')

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst : Nonempty ι
f : ι → G.Subgraph
rw :
  (∀ (G' : G.Subgraph), Membership.mem (γ := Set G.Subgraph) (Set.range fun (i : ι) ↦ f i) G' → G'.Adj a b) ↔
    ∀ (i : ι), (f i).Adj a b
⊢ Adj (G := G) (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _)]

Premises used: iInf, SimpleGraph.Subgraph.sInf_adj_of_nonempty, Set.range_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst : Nonempty ι
f : ι → G.Subgraph
⊢ (∀ (G' : G.Subgraph), Membership.mem (γ := Set G.Subgraph) (Set.range fun (i : ι) ↦ f i) G' → G'.Adj a b) ↔
    ∀ (i : ι), (f i).Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
⊢ (sSup s).verts = ⋃ G' ∈ s, G'.verts

Tactic:
rfl

Premises used: iSup, Set.iUnion, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
⊢ (sInf s).verts = ⋂ G' ∈ s, G'.verts

Tactic:
rfl

Premises used: iInf, Set.iInter, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
⊢ Eq.{u + 1} (α := Set V) (verts (G := G) (⨆ (i : ι), f i)) (⋃ (i : ι), (f i).verts)

Tactic:
simp [iSup]

Premises used: iSup
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
⊢ Eq.{u + 1} (α := Set V) (verts (G := G) (⨅ (i : ι), f i)) (⋂ (i : ι), (f i).verts)

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ Eq.{u + 1} (α := SimpleGraph (↑(verts (G := G) ⊥) : Type u)) (Subgraph.coe ⊥) ⊥

Tactic:
rfl

Premises used: SimpleGraph.Subgraph.coe, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ IsInduced.{u} (V := V) (G := G) ⊤

Tactic:
fun _ _ _ _ ↦ id

Premises used: id, SimpleGraph.Subgraph.IsInduced