awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ e ∈ (G.subgraphOfAdj hvw).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) {s(v, w)} e

Tactic:
e.ind ?_

Premises used: Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
h : ∀ (x y : V), s(x, y) ∈ (G.subgraphOfAdj hvw).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) {s(v, w)} s(x, y)
⊢ e ∈ (G.subgraphOfAdj hvw).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) {s(v, w)} e

Tactic:
refine e.ind ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ ∀ (x y : V), s(x, y) ∈ (G.subgraphOfAdj hvw).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) {s(v, w)} s(x, y)

Tactic:
simp only [eq_comm, Set.mem_singleton_iff, Subgraph.mem_edgeSet, subgraphOfAdj_adj,
    forall₂_true_iff]

Premises used: SimpleGraph.subgraphOfAdj_adj, SimpleGraph.Subgraph.mem_edgeSet, eq_comm, Set.mem_singleton_iff, forall₂_true_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
left : (G.subgraphOfAdj ⋯).verts ⊆ H.verts
right : ∀ ⦃v_1 w_1 : V⦄, (G.subgraphOfAdj ⋯).Adj v_1 w_1 → H.Adj v_1 w_1
⊢ G.subgraphOfAdj ⋯ ≤ H

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ (G.subgraphOfAdj ⋯).verts ⊆ H.verts

Tactic:
grind [subgraphOfAdj_verts, h.fst_mem, h.snd_mem]

Premises used: SimpleGraph.Subgraph.Adj.snd_mem, SimpleGraph.subgraphOfAdj_verts, SimpleGraph.Subgraph.Adj.fst_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ ∀ ⦃v_1 w_1 : V⦄, (G.subgraphOfAdj ⋯).Adj v_1 w_1 → H.Adj v_1 w_1

Tactic:
grind [subgraphOfAdj_adj, h.symm]

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

Tactic:
⟨fun hle ↦ hle.right <| subgraphOfAdj_adj_self h, subgraphOfAdj_le_of_adj H⟩

Premises used: And.right, SimpleGraph.subgraphOfAdj_le_of_adj, Iff.intro, SimpleGraph.subgraphOfAdj_adj_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
verts : ∀ (x : V), x ∈ (G.subgraphOfAdj ⋯).verts ↔ x ∈ (G.subgraphOfAdj hvw).verts
Adj : ∀ (x x_1 : V), (G.subgraphOfAdj ⋯).Adj x x_1 ↔ (G.subgraphOfAdj hvw).Adj x x_1
⊢ G.subgraphOfAdj ⋯ = G.subgraphOfAdj hvw

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x : V
⊢ x ∈ (G.subgraphOfAdj ⋯).verts ↔ x ∈ (G.subgraphOfAdj hvw).verts

Tactic:
simp [or_comm, and_comm]

Premises used: and_comm, or_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
⊢ (G.subgraphOfAdj ⋯).Adj x x_1 ↔ (G.subgraphOfAdj hvw).Adj x x_1

Tactic:
simp [or_comm, and_comm]

Premises used: and_comm, or_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
verts : ∀ (x : W), x ∈ (Subgraph.map f (G.subgraphOfAdj hvw)).verts ↔ x ∈ (G'.subgraphOfAdj ⋯).verts
Adj : ∀ (x x_1 : W), (Subgraph.map f (G.subgraphOfAdj hvw)).Adj x x_1 ↔ (G'.subgraphOfAdj ⋯).Adj x x_1
⊢ Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj ⋯

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x : W
⊢ x ∈ (Subgraph.map f (G.subgraphOfAdj hvw)).verts ↔ x ∈ (G'.subgraphOfAdj ⋯).verts

Tactic:
grind [Subgraph.map_verts, subgraphOfAdj_verts, Relation.Map, Subgraph.map_adj,
    subgraphOfAdj_adj]

Premises used: SimpleGraph.subgraphOfAdj_adj, SimpleGraph.Subgraph.map_verts, SimpleGraph.Subgraph.map_adj, SimpleGraph.subgraphOfAdj_verts, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x x_1 : W
⊢ (Subgraph.map f (G.subgraphOfAdj hvw)).Adj x x_1 ↔ (G'.subgraphOfAdj ⋯).Adj x x_1

Tactic:
grind [Subgraph.map_verts, subgraphOfAdj_verts, Relation.Map, Subgraph.map_adj,
    subgraphOfAdj_adj]

Premises used: SimpleGraph.subgraphOfAdj_adj, SimpleGraph.Subgraph.map_verts, SimpleGraph.Subgraph.map_adj, SimpleGraph.subgraphOfAdj_verts, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet u ⊆ {v, w}

Tactic:
(G.subgraphOfAdj hvw).neighborSet_subset_verts _

Premises used: SimpleGraph.Subgraph.neighborSet_subset_verts, SimpleGraph.subgraphOfAdj
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
h : ∀ (u : V), u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ Membership.mem (γ := Set V) {w} u
⊢ (G.subgraphOfAdj hvw).neighborSet v = {w}

Tactic:
ext u
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
this : w = u ↔ u = w
⊢ u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ Membership.mem (γ := Set V) {w} u

Tactic:
simpa [hvw.ne.symm] using this

Premises used: SimpleGraph.Adj.ne, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
h : w = u ↔ u = w
⊢ u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ Membership.mem (γ := Set V) {w} u

Tactic:
suffices w = u ↔ u = w by simpa [hvw.ne.symm] using this
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
h h₁ : u = w ↔ u = w
⊢ w = u ↔ u = w

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
rw : (G.subgraphOfAdj ⋯).neighborSet w = {v}
⊢ (G.subgraphOfAdj hvw).neighborSet w = {v}

Tactic:
rw [subgraphOfAdj_symm hvw.symm]

Premises used: SimpleGraph.Adj.symm, SimpleGraph.subgraphOfAdj_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj ⋯).neighborSet w = {v}

Tactic:
neighborSet_fst_subgraphOfAdj hvw.symm

Premises used: SimpleGraph.Adj.symm, SimpleGraph.neighborSet_fst_subgraphOfAdj
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj ⋯).neighborSet w = {v}

Tactic:
exact neighborSet_fst_subgraphOfAdj hvw.symm

Premises used: SimpleGraph.Adj.symm, SimpleGraph.neighborSet_fst_subgraphOfAdj
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
hv : u ≠ v
hw : u ≠ w
h : ∀ (x : V), x ∈ (G.subgraphOfAdj hvw).neighborSet u ↔ Membership.mem (γ := Set V) ∅ x
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
hv : u ≠ v
hw : u ≠ w
x : V
⊢ x ∈ (G.subgraphOfAdj hvw).neighborSet u ↔ Membership.mem (γ := Set V) ∅ x

Tactic:
simp [hv.symm, hw.symm]

Premises used: Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
pos : u = v → u = w → (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}
neg : u = v → ¬u = w → (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ ∅
pos₁ : ¬u = v → u = w → (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ {v}
neg₁ : ¬u = v → ¬u = w → (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ ∅
⊢ (G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
h : u = v
h_1 : u = w
pos : ∀ (hvw : G.Adj w w), (G.subgraphOfAdj hvw).neighborSet w = {w} ∪ {w}
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
h : u = v
h_1 : ¬u = w
neg : ¬v = w → (G.subgraphOfAdj hvw).neighborSet v = {w} ∪ ∅
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ ∅

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
h : ¬u = v
h_1 : u = w
pos : ¬w = v → (G.subgraphOfAdj hvw).neighborSet w = ∅ ∪ {v}
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ {v}

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
w : V
hvw : G.Adj w w
⊢ (G.subgraphOfAdj hvw).neighborSet w = {w} ∪ {w}

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v w : V
hvw : G.Adj v w
h : ¬v = w
⊢ (G.subgraphOfAdj hvw).neighborSet v = {w} ∪ ∅

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v w : V
hvw : G.Adj v w
h : ¬w = v
⊢ (G.subgraphOfAdj hvw).neighborSet w = ∅ ∪ {v}

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
h : ¬u = v
h_1 : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ ∅

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.singletonSubgraph u ≤ G.subgraphOfAdj h

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.singletonSubgraph v ≤ G.subgraphOfAdj h

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
h₁ : ∀ (x : V), x ∈ (G.subgraphOfAdj h).support ↔ Membership.mem (γ := Set V) {u, v} x
⊢ (G.subgraphOfAdj h).support = {u, v}

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x : V
h₁ : (∃ (w : V), u = x ∧ v = w ∨ u = w ∧ v = x) ↔ Membership.mem (γ := Set V) {u, v} x
⊢ (∃ (w : V), (G.subgraphOfAdj h).Adj x w) ↔ Membership.mem (γ := Set V) {u, v} x

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

Premises used: Sym2.eq, SimpleGraph.subgraphOfAdj_adj, Prod.swap_prod_mk, Sym2.rel_iff', Prod.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x : V
⊢ (∃ (w : V), u = x ∧ v = w ∨ u = w ∧ v = x) ↔ Membership.mem (γ := Set V) {u, v} x

Tactic:
⟨?_, fun h ↦ h.elim (fun hl ↦ ⟨v, .inl ⟨hl.symm, rfl⟩⟩) fun hr ↦ ⟨u, .inr ⟨rfl, hr.symm⟩⟩⟩

Premises used: And.intro, Iff.intro, Exists.intro, Or.inl, Or.elim, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x : V
h₁ : (∃ (w : V), u = x ∧ v = w ∨ u = w ∧ v = x) → Membership.mem (γ := Set V) {u, v} x
⊢ (∃ (w : V), u = x ∧ v = w ∨ u = w ∧ v = x) ↔ Membership.mem (γ := Set V) {u, v} x

Tactic:
refine ⟨?_, fun h ↦ h.elim (fun hl ↦ ⟨v, .inl ⟨hl.symm, rfl⟩⟩) fun hr ↦ ⟨u, .inr ⟨rfl, hr.symm⟩⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x w : V
hw : u = x ∧ v = w ∨ u = w ∧ v = x
⊢ Membership.mem (γ := Set V) {u, v} x

Tactic:
hw.elim (fun h1 ↦ .inl h1.1.symm) fun hr ↦ .inr hr.2.symm

Premises used: And.right, And.left, Or.inl, Or.elim, Eq.symm, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x w : V
hw : u = x ∧ v = w ∨ u = w ∧ v = x
⊢ Membership.mem (γ := Set V) {u, v} x

Tactic:
exact hw.elim (fun h1 ↦ .inl h1.1.symm) fun hr ↦ .inr hr.2.symm

Premises used: Or.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
⊢ (Subgraph.coeSubgraph G'').verts = Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts) '' G''.verts

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
v w : V
⊢ (Subgraph.coeSubgraph G'').Adj v w ↔
    ∃ (hv : v ∈ G'.verts) (hw : w ∈ G'.verts),
      G''.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw)

Tactic:
simp [Relation.Map]

Premises used: Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
v w : (↑G'.verts : Type u)
⊢ Adj (Subgraph.restrict G'') v w ↔ G'.Adj (↑v : V) (↑w : V) ∧ G''.Adj (↑v : V) (↑w : V)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
verts :
  ∀ (x : (↑G'.verts : Type u)),
    Membership.mem (γ := Set (↑G'.verts : Type u)) (Subgraph.verts (Subgraph.restrict (Subgraph.coeSubgraph G''))) x ↔
      x ∈ G''.verts
Adj :
  ∀ (x x_1 : (↑G'.verts : Type u)), Subgraph.Adj (Subgraph.restrict (Subgraph.coeSubgraph G'')) x x_1 ↔ G''.Adj x x_1
⊢ Subgraph.restrict (Subgraph.coeSubgraph G'') = G''

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x : (↑G'.verts : Type u)
⊢ Membership.mem (γ := Set (↑G'.verts : Type u)) (verts (Subgraph.restrict (Subgraph.coeSubgraph G''))) x ↔
    x ∈ G''.verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x x_1 : (↑G'.verts : Type u)
Adj :
  (G'.Adj (↑x : V) (↑x_1 : V) ∧
      ∃ (hv : (↑x : V) ∈ G'.verts) (hw : (↑x_1 : V) ∈ G'.verts),
        G''.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) (↑x : V) hv)
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) (↑x_1 : V) hw)) ↔
    G''.Adj x x_1
⊢ Subgraph.Adj (Subgraph.restrict (Subgraph.coeSubgraph G'')) x x_1 ↔ G''.Adj x x_1

Tactic:
rw [restrict_adj, coeSubgraph_adj]

Premises used: SimpleGraph.Subgraph.coeSubgraph_adj, SimpleGraph.Subgraph.restrict_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x x_1 : (↑G'.verts : Type u)
⊢ (G'.Adj (↑x : V) (↑x_1 : V) ∧
      ∃ (hv : (↑x : V) ∈ G'.verts) (hw : (↑x_1 : V) ∈ G'.verts),
        G''.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) (↑x : V) hv)
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) (↑x_1 : V) hw)) ↔
    G''.Adj x x_1

Tactic:
simpa using G''.adj_sub

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Function.Injective.{u + 1, u + 1} (α := G'.coe.Subgraph) Subgraph.coeSubgraph

Tactic:
Function.LeftInverse.injective restrict_coeSubgraph

Premises used: Function.LeftInverse.injective, SimpleGraph.Subgraph.restrict_coeSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
left : (Subgraph.coeSubgraph H').verts ⊆ H.verts
right : ∀ ⦃v w : V⦄, (Subgraph.coeSubgraph H').Adj v w → H.Adj v w
⊢ Subgraph.coeSubgraph H' ≤ H

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ (Subgraph.coeSubgraph H').verts ⊆ H.verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
w w_1 : (↑H.verts : Type u)
h : H'.Adj w w_1
⊢ H.Adj ((H.hom : (a : (↑H.verts : Type u)) → V) w) ((H.hom : (a : (↑H.verts : Type u)) → V) w_1)

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
H' : H.coe.Subgraph
w w_1 : (↑H.verts : Type u)
h : H'.Adj w w_1
⊢ H.Adj ((H.hom : (a : (↑H.verts : Type u)) → V) w) ((H.hom : (a : (↑H.verts : Type u)) → V) w_1)

Tactic:
exact H'.adj_sub h

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
verts : ∀ (x : V), x ∈ (Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H')).verts ↔ x ∈ (H ⊓ H').verts
Adj : ∀ (x x_1 : V), (Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H')).Adj x x_1 ↔ (H ⊓ H').Adj x x_1
⊢ Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H') = H ⊓ H'

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x : V
⊢ x ∈ (Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H')).verts ↔ x ∈ (H ⊓ H').verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x x_1 : V
Adj : (∃ (_ : x ∈ H.verts) (_ : x_1 ∈ H.verts), H.Adj x x_1 ∧ H'.Adj x x_1) ↔ (H ⊓ H').Adj x x_1
⊢ (Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H')).Adj x x_1 ↔ (H ⊓ H').Adj x x_1

Tactic:
simp_rw [coeSubgraph_adj, restrict_adj]

Premises used: SimpleGraph.Subgraph.coeSubgraph_adj, SimpleGraph.Subgraph.restrict_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x x_1 : V
Adj : H.Adj x x_1 → (x_1 ∈ H.verts ∧ x ∈ H.verts ∧ H'.Adj x x_1 ↔ H'.Adj x x_1)
⊢ (∃ (_ : x ∈ H.verts) (_ : x_1 ∈ H.verts), H.Adj x x_1 ∧ H'.Adj x x_1) ↔ (H ⊓ H').Adj x x_1

Tactic:
simp only [exists_and_left, exists_prop, inf_adj, and_congr_right_iff]

Premises used: SimpleGraph.Subgraph.inf_adj, exists_and_left, and_congr_right_iff, exists_prop
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x x_1 : V
h : H.Adj x x_1
⊢ x_1 ∈ H.verts ∧ x ∈ H.verts ∧ H'.Adj x x_1 ↔ H'.Adj x x_1

Tactic:
simp [H.edge_vert h, H.edge_vert h.symm]

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
a b : V
⊢ (G'.Adj \ Sym2.ToRel s) a b → (G'.Adj \ Sym2.ToRel s) b a

Tactic:
simp [G'.adj_comm, Sym2.eq_swap]

Premises used: SimpleGraph.Subgraph.adj_comm, Sym2.eq_swap
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).verts = G'.verts

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v w : V
⊢ (G'.deleteEdges s).Adj v w ↔ G'.Adj v w ∧ s(v, w) ∉ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Sym2.ToRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
verts : ∀ (x : V), x ∈ ((G'.deleteEdges s).deleteEdges s').verts ↔ x ∈ (G'.deleteEdges (s ∪ s')).verts
Adj : ∀ (x x_1 : V), ((G'.deleteEdges s).deleteEdges s').Adj x x_1 ↔ (G'.deleteEdges (s ∪ s')).Adj x x_1
⊢ (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
x : V
⊢ x ∈ ((G'.deleteEdges s).deleteEdges s').verts ↔ x ∈ (G'.deleteEdges (s ∪ s')).verts

Tactic:
simp [and_assoc, not_or]

Premises used: not_or, and_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
x x_1 : V
⊢ ((G'.deleteEdges s).deleteEdges s').Adj x x_1 ↔ (G'.deleteEdges (s ∪ s')).Adj x x_1

Tactic:
simp [and_assoc, not_or]

Premises used: not_or, and_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
verts : ∀ (x : V), x ∈ (G'.deleteEdges ∅).verts ↔ x ∈ G'.verts
Adj : ∀ (x x_1 : V), (G'.deleteEdges ∅).Adj x x_1 ↔ G'.Adj x x_1
⊢ G'.deleteEdges ∅ = G'

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x : V
⊢ x ∈ (G'.deleteEdges ∅).verts ↔ x ∈ G'.verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
⊢ (G'.deleteEdges ∅).Adj x x_1 ↔ G'.Adj x x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
Adj : ∀ (x x_1 : V), (G'.spanningCoe.deleteEdges s).Adj x x_1 ↔ (G'.deleteEdges s).spanningCoe.Adj x x_1
⊢ G'.spanningCoe.deleteEdges s = (G'.deleteEdges s).spanningCoe

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x x_1 : V
⊢ (G'.spanningCoe.deleteEdges s).Adj x x_1 ↔ (G'.deleteEdges s).spanningCoe.Adj x x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
Adj :
  ∀ (v : V) (hv : v ∈ G'.verts) (w : V) (hw : w ∈ G'.verts),
    (G'.coe.deleteEdges s).Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ↔
      (G'.deleteEdges (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' s)).coe.Adj
        (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw)
⊢ G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' s)).coe

Tactic:
ext ⟨v, hv⟩ ⟨w, hw⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
Adj :
  G'.Adj v w →
    (s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s ↔
      ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w))
⊢ (G'.coe.deleteEdges s).Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ↔
    (G'.deleteEdges (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' s)).coe.Adj
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw)

Tactic:
simp only [SimpleGraph.deleteEdges_adj, coe_adj, deleteEdges_adj, Set.mem_image, not_exists,
    not_and, and_congr_right_iff]

Premises used: SimpleGraph.Subgraph.coe_adj, Set.mem_image, not_exists, and_congr_right_iff, SimpleGraph.deleteEdges_adj, SimpleGraph.Subgraph.deleteEdges_adj, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
h : G'.Adj v w
Adj :
  s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s →
    ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)
Adj₁ :
  (∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)) →
    s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s
⊢ s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s ↔
    ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
h : G'.Adj v w
hs : s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s
⊢ ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)

Tactic:
Sym2.ind ?_

Premises used: Sym2.ind