awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
Adj :
  ∀ (x y : (↑G'.verts : Type u)),
    s(x, y) ∈ s → ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) s(x, y) = s(v, w)
⊢ ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)

Tactic:
refine Sym2.ind ?_
-- 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
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
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 →
    ¬Sym2.Rel V (v', w') (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 →
    ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts))
          s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v' hv', Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w' hw') =
        s(v, w)

Tactic:
simp only [Sym2.map_mk, Sym2.eq]

Premises used: Sym2.eq, Sym2.map_mk
-- 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
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
Adj :
  Sym2.Rel V (v', w') (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 →
    ¬Sym2.Rel V (v', w') (v, w)

Tactic:
contrapose
-- 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
hv' : v ∈ G'.verts
hw' : w ∈ G'.verts
⊢ s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv', Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw') ∉ s

Tactic:
simpa only [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- 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
hw' : v ∈ G'.verts
hv' : w ∈ G'.verts
⊢ s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hv', Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hw') ∉ s

Tactic:
simpa only [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- 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
h' : ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(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
⊢ False

Tactic:
h' _ hs rfl

Premises used: rfl
-- 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
h' : ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(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
⊢ False

Tactic:
exact h' _ hs rfl

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

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

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
left : (G'.deleteEdges s).verts ⊆ G'.verts
right : ∀ ⦃v w : V⦄, (G'.deleteEdges s).Adj v w → G'.Adj v w
⊢ G'.deleteEdges s ≤ G'

Tactic:
constructor
-- 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:
simp +contextual
-- 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

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
left : (G'.deleteEdges s').verts ⊆ (G'.deleteEdges s).verts
right : ∀ ⦃v w : V⦄, (G'.deleteEdges s').Adj v w → (G'.deleteEdges s).Adj v w
⊢ G'.deleteEdges s' ≤ G'.deleteEdges s

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ (G'.deleteEdges s').verts ⊆ (G'.deleteEdges s).verts

Tactic:
simp +contextual only [deleteEdges_verts, deleteEdges_adj,
    true_and, and_imp, subset_rfl]

Premises used: and_imp, SimpleGraph.Subgraph.deleteEdges_adj, SimpleGraph.Subgraph.deleteEdges_verts, subset_rfl, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
right : ∀ ⦃v w : V⦄, G'.Adj v w → s(v, w) ∉ s' → s(v, w) ∉ s
⊢ ∀ ⦃v w : V⦄, (G'.deleteEdges s').Adj v w → (G'.deleteEdges s).Adj v w

Tactic:
simp +contextual only [deleteEdges_verts, deleteEdges_adj,
    true_and, and_imp, subset_rfl]

Premises used: and_imp, SimpleGraph.Subgraph.deleteEdges_adj, SimpleGraph.Subgraph.deleteEdges_verts, subset_rfl, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, G'.Adj v w → s(v, w) ∉ s' → s(v, w) ∉ s

Tactic:
fun _ _ _ hs' hs ↦ hs' (h hs)

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, G'.Adj v w → s(v, w) ∉ s' → s(v, w) ∉ s

Tactic:
exact fun _ _ _ hs' hs ↦ hs' (h hs)
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
verts : ∀ (x : V), x ∈ (G'.deleteEdges (G'.edgeSet ∩ s)).verts ↔ x ∈ (G'.deleteEdges s).verts
Adj : ∀ (x x_1 : V), (G'.deleteEdges (G'.edgeSet ∩ s)).Adj x x_1 ↔ (G'.deleteEdges s).Adj x x_1
⊢ G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s

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

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x x_1 : V
⊢ (G'.deleteEdges (G'.edgeSet ∩ s)).Adj x x_1 ↔ (G'.deleteEdges s).Adj x x_1

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

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

Tactic:
simp +contextual [imp_false]

Premises used: imp_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x x_1 : V
⊢ (G'.deleteEdges (s ∩ G'.edgeSet)).Adj x x_1 ↔ (G'.deleteEdges s).Adj x x_1

Tactic:
simp +contextual [imp_false]

Premises used: imp_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v w : (↑(G'.deleteEdges s).verts : Type u)
⊢ (G'.deleteEdges s).coe.Adj v w → G'.coe.Adj v w

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).spanningCoe ≤ G'.spanningCoe

Tactic:
spanningCoe_le_of_le (deleteEdges_le s)

Premises used: SimpleGraph.Subgraph.deleteEdges_le, SimpleGraph.Subgraph.spanningCoe_le_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
Adj : ∀ (x x_1 : (↑s : Type u)), (SimpleGraph.induce s G).Adj x x_1 ↔ SimpleGraph.Adj (Subgraph.coe (induce ⊤ s)) x x_1
⊢ SimpleGraph.induce s G = Subgraph.coe (induce ⊤ s)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
x x_1 : (↑s : Type u)
⊢ (SimpleGraph.induce s G).Adj x x_1 ↔ SimpleGraph.Adj (Subgraph.coe (induce ⊤ s)) x x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
rw :
  Subgraph.spanningCoe (G := G) (induce ⊤ s) =
    spanningCoe (s := s) (Subgraph.coe (induce ⊤ s) : SimpleGraph (↑(verts (G := G) (induce ⊤ s)) : Type u))
⊢ Subgraph.spanningCoe (G := G) (induce ⊤ s) = (SimpleGraph.induce s G).spanningCoe (s := s)

Tactic:
rw [induce_eq_coe_induce_top]

Premises used: SimpleGraph.induce_eq_coe_induce_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ Subgraph.spanningCoe (G := G) (induce ⊤ s) =
    spanningCoe (s := s) (Subgraph.coe (induce ⊤ s) : SimpleGraph (↑(verts (G := G) (induce ⊤ s)) : Type u))

Tactic:
(Subgraph.spanningCoe_coe _).symm

Premises used: Set.Mem, SimpleGraph.Subgraph.spanningCoe_coe, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ Subgraph.spanningCoe (G := G) (induce ⊤ s) =
    spanningCoe (s := s) (Subgraph.coe (induce ⊤ s) : SimpleGraph (↑(verts (G := G) (induce ⊤ s)) : Type u))

Tactic:
exact (Subgraph.spanningCoe_coe _).symm

Premises used: SimpleGraph.Subgraph.spanningCoe_coe, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h : G'.IsInduced
⊢ induce ⊤ G'.verts = G'

Tactic:
Subgraph.ext rfl <| funext₂ fun _ _ ↦ propext
    ⟨fun ⟨hu, hv, h'⟩ ↦ h hu hv h', fun h ↦ ⟨G'.edge_vert h, G'.edge_vert h.symm, h.adj_sub⟩⟩

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.Adj.symm, _private.0.SimpleGraph.Subgraph.IsInduced.induce_top_verts.match_1, SimpleGraph.Subgraph.ext, funext₂, SimpleGraph.Subgraph.Adj.adj_sub, And.intro, Iff.intro, propext, SimpleGraph.Subgraph.Adj, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.IsInduced ↔ ∃ (s : Set V), G' = induce ⊤ s

Tactic:
⟨fun h ↦ ⟨G'.verts, h.induce_top_verts.symm⟩, fun ⟨s, h⟩ _ hu _ hv hadj ↦ ?_⟩

Premises used: _private.0.SimpleGraph.Subgraph.isInduced_iff_exists_eq_induce_top.match_1, Iff.intro, Exists.intro, SimpleGraph.Subgraph.IsInduced.induce_top_verts, SimpleGraph.Subgraph.Adj, Eq.symm, SimpleGraph.Subgraph.verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
refine :
  (∃ (s : Set V), G' = induce ⊤ s) →
    ∀ (x : V) (hu : x ∈ G'.verts) (x_1 : V) (hv : x_1 ∈ G'.verts) (hadj : G.Adj x x_1) (s : Set V)
      (h : G' = induce ⊤ s), G'.Adj x x_1
⊢ G'.IsInduced ↔ ∃ (s : Set V), G' = induce ⊤ s

Tactic:
refine ⟨fun h ↦ ⟨G'.verts, h.induce_top_verts.symm⟩, fun ⟨s, h⟩ _ hu _ hv hadj ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : ∃ (s : Set V), G' = induce ⊤ s
x : V
hu : x ∈ G'.verts
x_1 : V
hv : x_1 ∈ G'.verts
hadj : G.Adj x x_1
s : Set V
h : G' = induce ⊤ s
rw : Adj (G := G) (induce ⊤ G'.verts) x x_1
⊢ G'.Adj x x_1

Tactic:
rw [h, (h ▸ rfl : s = G'.verts)]

Premises used: Eq.rec, Eq.symm, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : ∃ (s : Set V), G' = induce ⊤ s
x : V
hu : x ∈ G'.verts
x_1 : V
hv : x_1 ∈ G'.verts
hadj : G.Adj x x_1
s : Set V
h : G' = induce ⊤ s
⊢ Adj (G := G) (induce ⊤ G'.verts) x x_1

Tactic:
⟨hu, hv, hadj⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : ∃ (s : Set V), G' = induce ⊤ s
x : V
hu : x ∈ G'.verts
x_1 : V
hv : x_1 ∈ G'.verts
hadj : G.Adj x x_1
s : Set V
h : G' = induce ⊤ s
⊢ Adj (G := G) (induce ⊤ G'.verts) x x_1

Tactic:
exact ⟨hu, hv, hadj⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
left : (G'.induce s).verts ⊆ (G''.induce s').verts
right : ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w
⊢ G'.induce s ≤ G''.induce s'

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ (G'.induce s).verts ⊆ (G''.induce s').verts

Tactic:
simp [hs]
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
right : ∀ ⦃v w : V⦄, v ∈ s → w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w
⊢ ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w

Tactic:
simp +contextual only [induce_adj, and_imp]

Premises used: SimpleGraph.Subgraph.induce_adj, and_imp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
ha : G'.Adj v w
⊢ v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Tactic:
⟨hs hv, hs hw, hg.2 ha⟩

Premises used: And.right, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
ha : G'.Adj v w
⊢ v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Tactic:
exact ⟨hs hv, hs hw, hg.2 ha⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s : Set V
hg : G' ≤ G''
⊢ G'.induce s ≤ G''.induce s

Tactic:
induce_mono hg subset_rfl

Premises used: subset_rfl, SimpleGraph.Subgraph.induce_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
hs : s ⊆ s'
⊢ G'.induce s ≤ G'.induce s'

Tactic:
induce_mono le_rfl hs

Premises used: le_rfl, SimpleGraph.Subgraph.induce_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
verts : ∀ (x : V), x ∈ (G'.induce ∅).verts ↔ Membership.mem (γ := Set V) (Subgraph.verts (G := G) ⊥) x
Adj : ∀ (x x_1 : V), (G'.induce ∅).Adj x x_1 ↔ Subgraph.Adj (G := G) ⊥ x x_1
⊢ G'.induce ∅ = ⊥

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

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

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
verts : ∀ (x : V), x ∈ (G'.induce G'.verts).verts ↔ x ∈ G'.verts
Adj : ∀ (x x_1 : V), (G'.induce G'.verts).Adj x x_1 ↔ G'.Adj x x_1
⊢ G'.induce G'.verts = G'

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x : V
⊢ x ∈ (G'.induce G'.verts).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
Adj : (G'.induce G'.verts).Adj x x_1 → G'.Adj x x_1
Adj₁ : G'.Adj x x_1 → (G'.induce G'.verts).Adj x x_1
⊢ (G'.induce G'.verts).Adj x x_1 ↔ G'.Adj x x_1

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
⊢ (G'.induce G'.verts).Adj x x_1 → G'.Adj x x_1

Tactic:
simp +contextual only [induce_adj, imp_true_iff, and_true]

Premises used: SimpleGraph.Subgraph.induce_adj, and_true, imp_true_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
Adj : G'.Adj x x_1 → x ∈ G'.verts ∧ x_1 ∈ G'.verts
⊢ G'.Adj x x_1 → (G'.induce G'.verts).Adj x x_1

Tactic:
simp +contextual only [induce_adj, imp_true_iff, and_true]

Premises used: SimpleGraph.Subgraph.induce_adj, and_true, imp_true_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
⊢ G'.Adj x x_1 → x ∈ G'.verts ∧ x_1 ∈ G'.verts

Tactic:
fun ha ↦ ⟨G'.edge_vert ha, G'.edge_vert ha.symm⟩

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.Adj.symm, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
⊢ G'.Adj x x_1 → x ∈ G'.verts ∧ x_1 ∈ G'.verts

Tactic:
exact fun ha ↦ ⟨G'.edge_vert ha, G'.edge_vert ha.symm⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G' ≤ induce ⊤ G'.verts

Tactic:
calc G' = G'.induce G'.verts := Subgraph.induce_self_verts.symm
       _ ≤ (⊤ : G.Subgraph).induce G'.verts := Subgraph.induce_mono_left le_top

Premises used: Trans.trans, le_top, SimpleGraph.Subgraph.induce_self_verts, Eq.symm, SimpleGraph.Subgraph.induce_mono_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
left : (G'.induce s ⊔ G'.induce s').verts ⊆ (G'.induce (s ∪ s')).verts
right : ∀ ⦃v w : V⦄, (G'.induce s ⊔ G'.induce s').Adj v w → (G'.induce (s ∪ s')).Adj v w
⊢ G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ (G'.induce s ⊔ G'.induce s').verts ⊆ (G'.induce (s ∪ s')).verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
v w : V
h : v ∈ s ∧ w ∈ s ∧ G'.Adj v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
v w : V
h : v ∈ s' ∧ w ∈ s' ∧ G'.Adj v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s ≤ G'.induce (s ∪ s')

Tactic:
(sup_le_iff.mp le_induce_union).1

Premises used: sup_le_iff, And.left, Iff.mp, SimpleGraph.Subgraph.le_induce_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s ≤ G'.induce (s ∪ s')

Tactic:
exact (sup_le_iff.mp le_induce_union).1

Premises used: sup_le_iff, And.left, Iff.mp, SimpleGraph.Subgraph.le_induce_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s' ≤ G'.induce (s ∪ s')

Tactic:
(sup_le_iff.mp le_induce_union).2

Premises used: sup_le_iff, And.right, Iff.mp, SimpleGraph.Subgraph.le_induce_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s' ≤ G'.induce (s ∪ s')

Tactic:
exact (sup_le_iff.mp le_induce_union).2

Premises used: sup_le_iff, And.right, Iff.mp, SimpleGraph.Subgraph.le_induce_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
verts :
  ∀ (x : V), x ∈ (G.singletonSubgraph v).verts ↔ Membership.mem (γ := Set V) (Subgraph.verts (G := G) (induce ⊤ {v})) x
Adj : ∀ (x x_1 : V), (G.singletonSubgraph v).Adj x x_1 ↔ Subgraph.Adj (G := G) (induce ⊤ {v}) x x_1
⊢ G.singletonSubgraph v = induce ⊤ {v}

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v x : V
⊢ x ∈ (G.singletonSubgraph v).verts ↔ Membership.mem (γ := Set V) (verts (G := G) (induce ⊤ {v})) x

Tactic:
simp +contextual [-Set.bot_eq_empty, Prop.bot_eq_false]

Premises used: Prop.bot_eq_false, Set.bot_eq_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v x x_1 : V
⊢ (G.singletonSubgraph v).Adj x x_1 ↔ Adj (G := G) (induce ⊤ {v}) x x_1

Tactic:
simp +contextual [-Set.bot_eq_empty, Prop.bot_eq_false]

Premises used: Prop.bot_eq_false, Set.bot_eq_empty
-- 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 hvw).verts ↔ Membership.mem (γ := Set V) (Subgraph.verts (G := G) (induce ⊤ {v, w})) x
Adj : ∀ (x x_1 : V), (G.subgraphOfAdj hvw).Adj x x_1 ↔ Subgraph.Adj (G := G) (induce ⊤ {v, w}) x x_1
⊢ G.subgraphOfAdj hvw = induce ⊤ {v, w}

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 hvw).verts ↔ Membership.mem (γ := Set V) (verts (G := G) (induce ⊤ {v, w})) x

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
Adj : (G.subgraphOfAdj hvw).Adj x x_1 → Subgraph.Adj (G := G) (induce ⊤ {v, w}) x x_1
Adj₁ : Subgraph.Adj (G := G) (induce ⊤ {v, w}) x x_1 → (G.subgraphOfAdj hvw).Adj x x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1 ↔ Subgraph.Adj (G := G) (induce ⊤ {v, w}) x x_1

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : (G.subgraphOfAdj hvw).Adj x x_1
⊢ v = x ∧ w = x_1 ∨ v = x_1 ∧ w = x

Tactic:
simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff] at h

Premises used: Sym2.eq, SimpleGraph.subgraphOfAdj_adj, Sym2.rel_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : v = x ∧ w = x_1 ∨ v = x_1 ∧ w = x
Adj : Subgraph.Adj (G := G) (induce ⊤ {v, w}) v w
Adj₁ : Subgraph.Adj (G := G) (induce ⊤ {v, w}) w v
⊢ Subgraph.Adj (G := G) (induce ⊤ {v, w}) x x_1

Tactic:
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h

Premises used: rfl