awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
h : v ∉ G'.verts
w : V
hw : w ∈ G'.neighborSet v
⊢ False

Tactic:
h hw.fst_mem

Premises used: SimpleGraph.Subgraph.Adj.fst_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
h : v ∉ G'.verts
w : V
hw : w ∈ G'.neighborSet v
⊢ False

Tactic:
exact h hw.fst_mem

Premises used: SimpleGraph.Subgraph.Adj.fst_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
inst_1 : Fintype (↑(G.neighborSet v) : Type u)
rw : G'.degree v ≤ Fintype.card.{u} (↑(G.neighborSet v) : Type u)
⊢ G'.degree v ≤ G.degree v

Tactic:
rw [← card_neighborSet_eq_degree]

Premises used: SimpleGraph.card_neighborSet_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
inst_1 : Fintype (↑(G.neighborSet v) : Type u)
⊢ G'.degree v ≤ Fintype.card.{u} (↑(G.neighborSet v) : Type u)

Tactic:
Set.card_le_card (G'.neighborSet_subset v)

Premises used: SimpleGraph.Subgraph.degree, Set.card_le_card, SimpleGraph.Subgraph.neighborSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
inst_1 : Fintype (↑(G.neighborSet v) : Type u)
⊢ G'.degree v ≤ Fintype.card.{u} (↑(G.neighborSet v) : Type u)

Tactic:
exact Set.card_le_card (G'.neighborSet_subset v)

Premises used: Set.card_le_card, SimpleGraph.Subgraph.neighborSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
h : G' ≤ G''
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
inst_1 : Fintype (↑(G''.neighborSet v) : Type u)
⊢ G'.degree v ≤ G''.degree v

Tactic:
Set.card_le_card (neighborSet_subset_of_subgraph h v)

Premises used: SimpleGraph.Subgraph.degree, Set.card_le_card, SimpleGraph.Subgraph.neighborSet_subset_of_subgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : (↑G'.verts : Type u)
inst : Fintype (↑(G'.coe.neighborSet v) : Type u)
inst_1 : Fintype (↑(G'.neighborSet (↑v : V)) : Type u)
rw : Fintype.card.{u} (↑(G'.coe.neighborSet v) : Type u) = G'.degree (↑v : V)
⊢ G'.coe.degree v = G'.degree (↑v : V)

Tactic:
rw [← card_neighborSet_eq_degree]

Premises used: SimpleGraph.card_neighborSet_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : (↑G'.verts : Type u)
inst : Fintype (↑(G'.coe.neighborSet v) : Type u)
inst_1 : Fintype (↑(G'.neighborSet (↑v : V)) : Type u)
⊢ Fintype.card.{u} (↑(G'.coe.neighborSet v) : Type u) = G'.degree (↑v : V)

Tactic:
Fintype.card_congr (coeNeighborSetEquiv v)

Premises used: Fintype.card_congr, SimpleGraph.Subgraph.coeNeighborSetEquiv, SimpleGraph.Subgraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : (↑G'.verts : Type u)
inst : Fintype (↑(G'.coe.neighborSet v) : Type u)
inst_1 : Fintype (↑(G'.neighborSet (↑v : V)) : Type u)
⊢ Fintype.card.{u} (↑(G'.coe.neighborSet v) : Type u) = G'.degree (↑v : V)

Tactic:
exact Fintype.card_congr (coeNeighborSetEquiv v)

Premises used: Fintype.card_congr, SimpleGraph.Subgraph.coeNeighborSetEquiv
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
inst_1 : Fintype (↑(G'.spanningCoe.neighborSet v) : Type u)
rw : Fintype.card.{u} (↑(G'.spanningCoe.neighborSet v) : Type u) = Fintype.card.{u} (↑(G'.neighborSet v) : Type u)
⊢ G'.spanningCoe.degree v = G'.degree v

Tactic:
rw [← card_neighborSet_eq_degree, Subgraph.degree]

Premises used: SimpleGraph.card_neighborSet_eq_degree, SimpleGraph.Subgraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
inst_1 : Fintype (↑(G'.spanningCoe.neighborSet v) : Type u)
⊢ Fintype.card.{u} (↑(G'.spanningCoe.neighborSet v) : Type u) = Fintype.card.{u} (↑(G'.neighborSet v) : Type u)

Tactic:
congr!
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
⊢ 0 < G'.degree v ↔ ∃ (w : V), G'.Adj v w

Tactic:
simp only [degree, Fintype.card_pos_iff, nonempty_subtype, mem_neighborSet]

Premises used: SimpleGraph.Subgraph.mem_neighborSet, SimpleGraph.Subgraph.degree, nonempty_subtype, Fintype.card_pos_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
pos : ∀ (hv : v ∈ G'.verts), G'.degree v = 0
neg : ∀ (hv : v ∉ G'.verts), G'.degree v = 0
⊢ G'.degree v = 0

Tactic:
by_cases hv : v ∈ G'.verts

Premises used: SimpleGraph.Subgraph.verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
pos : G'.coe.degree (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) = 0
⊢ G'.degree v = 0

Tactic:
rw [← G'.coe_degree ⟨v, hv⟩]

Premises used: SimpleGraph.Subgraph.coe_degree, Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
⊢ Subsingleton.{u + 1} (↑G'.verts : Type u)

Tactic:
have := (Set.subsingleton_coe _).mpr hG
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
this : Subsingleton.{u + 1} (↑G'.verts : Type u)
⊢ G'.coe.degree (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) = 0

Tactic:
G'.coe.degree_eq_zero_of_subsingleton ⟨v, hv⟩

Premises used: Subtype.mk, SimpleGraph.degree_eq_zero_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
this : Subsingleton.{u + 1} (↑G'.verts : Type u)
⊢ G'.coe.degree (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) = 0

Tactic:
exact G'.coe.degree_eq_zero_of_subsingleton ⟨v, hv⟩

Premises used: Subtype.mk, SimpleGraph.degree_eq_zero_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
hv : v ∉ G'.verts
⊢ G'.degree v = 0

Tactic:
degree_of_notMem_verts hv

Premises used: SimpleGraph.Subgraph.degree_of_notMem_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
hv : v ∉ G'.verts
⊢ G'.degree v = 0

Tactic:
exact degree_of_notMem_verts hv

Premises used: SimpleGraph.Subgraph.degree_of_notMem_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
rw : (∃! a : V, a ∈ (G'.neighborSet v).toFinset) ↔ ∃! w : V, G'.Adj v w
⊢ G'.degree v = 1 ↔ ∃! w : V, G'.Adj v w

Tactic:
rw [← finset_card_neighborSet_eq_degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]

Premises used: Finset.card_eq_one, SimpleGraph.Subgraph.finset_card_neighborSet_eq_degree, Finset.singleton_iff_unique_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
⊢ (∃! a : V, a ∈ (G'.neighborSet v).toFinset) ↔ ∃! w : V, G'.Adj v w

Tactic:
simp only [Set.mem_toFinset, mem_neighborSet]

Premises used: SimpleGraph.Subgraph.mem_neighborSet, Set.mem_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
h : G'.degree v ≠ 0
by_contra : ∀ (this : ¬Nontrivial.{u} (↑G'.verts : Type u)), False
⊢ Nontrivial.{u} (↑G'.verts : Type u)

Tactic:
by_contra
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
h : G'.degree v ≠ 0
this : ¬Nontrivial.{u} (↑G'.verts : Type u)
⊢ False

Tactic:
simp_all [G'.degree_eq_zero_of_subsingleton v]

Premises used: SimpleGraph.Subgraph.degree_eq_zero_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : (↑(G.neighborSet v) : Type u) ≃ (↑(H.neighborSet v) : Type u)
hfin : (G.neighborSet v).Finite
⊢ (H.neighborSet v).Finite

Tactic:
h.set_finite_iff.mp hfin

Premises used: Equiv.set_finite_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : (↑(G.neighborSet v) : Type u) ≃ (↑(H.neighborSet v) : Type u)
hfin : (G.neighborSet v).Finite
lift :
  ∀ (s : Finset V) (hs : (↑s : Set V) = H.neighborSet v) (h : (↑(G.neighborSet v) : Type u) ≃ (↑(↑s : Set V) : Type u)),
    (↑s : Set V) = G.neighborSet v
⊢ H.neighborSet v = G.neighborSet v

Tactic:
lift H.neighborSet v to Finset V using h.set_finite_iff.mp hfin with s hs

Premises used: Finset, Equiv.set_finite_iff, SimpleGraph.Subgraph.neighborSet, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
hfin : (G.neighborSet v).Finite
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
h : (↑(G.neighborSet v) : Type u) ≃ (↑(↑s : Set V) : Type u)
⊢ (G.neighborSet v).Finite

Tactic:
hfin
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
hfin : (G.neighborSet v).Finite
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
h : (↑(G.neighborSet v) : Type u) ≃ (↑(↑s : Set V) : Type u)
lift :
  ∀ (t : Finset V) (ht : (↑t : Set V) = G.neighborSet v) (h : (↑(↑t : Set V) : Type u) ≃ (↑(↑s : Set V) : Type u)),
    (↑s : Set V) = (↑t : Set V)
⊢ (↑s : Set V) = G.neighborSet v

Tactic:
lift G.neighborSet v to Finset V using hfin with t ht

Premises used: Finset, SimpleGraph.neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
t : Finset V
ht : (↑t : Set V) = G.neighborSet v
h : (↑(↑t : Set V) : Type u) ≃ (↑(↑s : Set V) : Type u)
⊢ (↑s : Set V) = (↑t : Set V)

Tactic:
congrArg _ <| Finset.eq_of_subset_of_card_le ?_ (Finset.card_eq_of_equiv h).le

Premises used: congrArg, Eq.le, Finset.eq_of_subset_of_card_le, Finset.card_eq_of_equiv
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
t : Finset V
ht : (↑t : Set V) = G.neighborSet v
h : (↑(↑t : Set V) : Type u) ≃ (↑(↑s : Set V) : Type u)
refine : s ⊆ t
⊢ (↑s : Set V) = (↑t : Set V)

Tactic:
refine congrArg _ <| Finset.eq_of_subset_of_card_le ?_ (Finset.card_eq_of_equiv h).le

Premises used: congrArg, Eq.le, Finset.eq_of_subset_of_card_le, Finset.card_eq_of_equiv
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
t : Finset V
ht : (↑t : Set V) = G.neighborSet v
h : (↑(↑t : Set V) : Type u) ≃ (↑(↑s : Set V) : Type u)
rw : H.neighborSet v ⊆ G.neighborSet v
⊢ s ⊆ t

Tactic:
rw [← Finset.coe_subset, hs, ht]

Premises used: Finset.coe_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
t : Finset V
ht : (↑t : Set V) = G.neighborSet v
h : (↑(↑t : Set V) : Type u) ≃ (↑(↑s : Set V) : Type u)
⊢ H.neighborSet v ⊆ G.neighborSet v

Tactic:
H.neighborSet_subset _

Premises used: SimpleGraph.Subgraph.neighborSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
t : Finset V
ht : (↑t : Set V) = G.neighborSet v
h : (↑(↑t : Set V) : Type u) ≃ (↑(↑s : Set V) : Type u)
⊢ H.neighborSet v ⊆ G.neighborSet v

Tactic:
exact H.neighborSet_subset _

Premises used: SimpleGraph.Subgraph.neighborSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : (↑(G.neighborSet v) : Type u) ≃ (↑(H.neighborSet v) : Type u)
hfin : (G.neighborSet v).Finite
w : V
⊢ H.Adj v w ↔ G.Adj v w

Tactic:
Set.ext_iff.mp (neighborSet_eq_of_equiv h hfin) _

Premises used: Set.Mem, setOf, SimpleGraph.neighborSet, SimpleGraph.Subgraph.neighborSet, SimpleGraph.Subgraph.neighborSet_eq_of_equiv, Iff.mp, Set.ext_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst : Fintype (↑((toSubgraph H h).neighborSet v) : Type u)
inst_1 : Fintype (↑(H.neighborSet v) : Type u)
⊢ Fintype.card.{u} (↑((toSubgraph H h).neighborSet v) : Type u) = H.degree v

Tactic:
(Finset.card_eq_of_equiv_fintype ?_).symm

Premises used: Finset.card_eq_of_equiv_fintype, SimpleGraph.degree, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst : Fintype (↑((toSubgraph H h).neighborSet v) : Type u)
inst_1 : Fintype (↑(H.neighborSet v) : Type u)
refine : ↥(H.neighborFinset v) ≃ (↑((toSubgraph H h).neighborSet v) : Type u)
⊢ Fintype.card.{u} (↑((toSubgraph H h).neighborSet v) : Type u) = H.degree v

Tactic:
refine (Finset.card_eq_of_equiv_fintype ?_).symm

Premises used: Finset.card_eq_of_equiv_fintype, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst : Fintype (↑((toSubgraph H h).neighborSet v) : Type u)
inst_1 : Fintype (↑(H.neighborSet v) : Type u)
simp : { x : V // H.Adj v x } ≃ { x : V // H.Adj v x }
⊢ ↥(H.neighborFinset v) ≃ (↑((toSubgraph H h).neighborSet v) : Type u)

Tactic:
simp only [mem_neighborFinset]

Premises used: SimpleGraph.mem_neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst : Fintype (↑((toSubgraph H h).neighborSet v) : Type u)
inst_1 : Fintype (↑(H.neighborSet v) : Type u)
⊢ { x : V // H.Adj v x } ≃ { x : V // H.Adj v x }

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst : Fintype (↑((toSubgraph H h).neighborSet v) : Type u)
inst_1 : Fintype (↑(H.neighborSet v) : Type u)
⊢ (toSubgraph H h).degree v = H.degree v

Tactic:
simp [Subgraph.degree, card_neighborSet_toSubgraph]

Premises used: SimpleGraph.card_neighborSet_toSubgraph, SimpleGraph.Subgraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
⊢ G.singletonSubgraph v ≤ H ↔ v ∈ H.verts

Tactic:
⟨fun h ↦ h.1 (Set.mem_singleton v), ?_⟩

Premises used: Set.mem_singleton, And.left, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
refine : v ∈ H.verts → G.singletonSubgraph v ≤ H
⊢ G.singletonSubgraph v ≤ H ↔ v ∈ H.verts

Tactic:
refine ⟨fun h ↦ h.1 (Set.mem_singleton v), ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
left : (G.singletonSubgraph v).verts ⊆ H.verts
right : ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w
⊢ G.singletonSubgraph v ≤ H

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
left : {v} ⊆ H.verts
left₁ left₂ left₃ left₄ : v ∈ H.verts
⊢ (G.singletonSubgraph v).verts ⊆ H.verts

Tactic:
rwa [singletonSubgraph_verts, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, SimpleGraph.singletonSubgraph_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w

Tactic:
fun _ _ ↦ False.elim

Premises used: False.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w

Tactic:
exact fun _ _ ↦ False.elim

Premises used: False.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
verts :
  ∀ (x : W), x ∈ (Subgraph.map f (G.singletonSubgraph v)).verts ↔ x ∈ (G'.singletonSubgraph ((f : (a : V) → W) v)).verts
Adj :
  ∀ (x x_1 : W),
    (Subgraph.map f (G.singletonSubgraph v)).Adj x x_1 ↔ (G'.singletonSubgraph ((f : (a : V) → W) v)).Adj x x_1
⊢ Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph ((f : (a : V) → W) v)

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 : V
x : W
⊢ x ∈ (Subgraph.map f (G.singletonSubgraph v)).verts ↔ x ∈ (G'.singletonSubgraph ((f : (a : V) → W) v)).verts

Tactic:
simp only [Relation.Map, Subgraph.map_adj, singletonSubgraph_adj, Pi.bot_apply,
    exists_and_left, and_iff_left_iff_imp, Subgraph.map_verts,
    singletonSubgraph_verts, Set.image_singleton]

Premises used: Set.image_singleton, SimpleGraph.singletonSubgraph_adj, exists_and_left, SimpleGraph.singletonSubgraph_verts, Pi.bot_apply, SimpleGraph.Subgraph.map_verts, SimpleGraph.Subgraph.map_adj, and_iff_left_iff_imp, 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 : V
x x_1 : W
Adj : ⊥ → ∃ (x_2 : V), (f : (a : V) → W) x_2 = x ∧ ∃ (x : V), (f : (a : V) → W) x = x_1
⊢ (Subgraph.map f (G.singletonSubgraph v)).Adj x x_1 ↔ (G'.singletonSubgraph ((f : (a : V) → W) v)).Adj x x_1

Tactic:
simp only [Relation.Map, Subgraph.map_adj, singletonSubgraph_adj, Pi.bot_apply,
    exists_and_left, and_iff_left_iff_imp, Subgraph.map_verts,
    singletonSubgraph_verts, Set.image_singleton]

Premises used: Set.image_singleton, SimpleGraph.singletonSubgraph_adj, exists_and_left, SimpleGraph.singletonSubgraph_verts, Pi.bot_apply, SimpleGraph.Subgraph.map_verts, SimpleGraph.Subgraph.map_adj, and_iff_left_iff_imp, 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 : V
x x_1 : W
⊢ ⊥ → ∃ (x_2 : V), (f : (a : V) → W) x_2 = x ∧ ∃ (x : V), (f : (a : V) → W) x = x_1

Tactic:
False.elim

Premises used: False.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x x_1 : W
⊢ ⊥ → ∃ (x_2 : V), (f : (a : V) → W) x_2 = x ∧ ∃ (x : V), (f : (a : V) → W) x = x_1

Tactic:
exact False.elim

Premises used: False.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.singletonSubgraph v).neighborSet w = ∅

Tactic:
rfl

Premises used: setOf, SimpleGraph.Subgraph.neighborSet, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ (G.singletonSubgraph v).edgeSet = ∅

Tactic:
Sym2.fromRel_bot

Premises used: Sym2.fromRel_bot, SimpleGraph.Subgraph.edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H = G.singletonSubgraph v
rw : (G.singletonSubgraph v).verts = {v}
rw₁ rw₂ : Eq (α := Set V) {v} {v}
⊢ H.verts = {v}

Tactic:
rw [h, singletonSubgraph_verts]

Premises used: SimpleGraph.singletonSubgraph_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
refine : ∀ (h : H.verts = {v}), H = G.singletonSubgraph v
⊢ H = G.singletonSubgraph v ↔ H.verts = {v}

Tactic:
refine ⟨fun h ↦ by rw [h, singletonSubgraph_verts], fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
verts : ∀ (x : V), x ∈ H.verts ↔ x ∈ (G.singletonSubgraph v).verts
Adj : ∀ (x x_1 : V), H.Adj x x_1 ↔ (G.singletonSubgraph v).Adj x x_1
⊢ H = G.singletonSubgraph v

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

Tactic:
rw [h, singletonSubgraph_verts]

Premises used: SimpleGraph.singletonSubgraph_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
Adj : ¬H.Adj x x_1
⊢ H.Adj x x_1 ↔ (G.singletonSubgraph v).Adj x x_1

Tactic:
simp only [Prop.bot_eq_false, singletonSubgraph_adj, Pi.bot_apply, iff_false]

Premises used: iff_false, SimpleGraph.singletonSubgraph_adj, Prop.bot_eq_false, Pi.bot_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
⊢ x ∈ H.verts

Tactic:
have ha1 := ha.fst_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x ∈ H.verts
⊢ x_1 ∈ H.verts

Tactic:
have ha2 := ha.snd_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x ∈ H.verts
ha2 : x_1 ∈ H.verts
⊢ x = v

Tactic:
rw [h, Set.mem_singleton_iff] at ha1 ha2

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x ∈ H.verts
ha2 : x_1 ∈ H.verts
ha1₁ : x = v
⊢ x_1 = v

Tactic:
rw [h, Set.mem_singleton_iff] at ha1 ha2

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x = v
ha2 : x_1 = v
⊢ H.Adj x_1 x_1

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x = v
ha2 : x_1 = v
ha₁ : H.Adj x_1 x_1
⊢ H.verts = {x_1}

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
x : V
ha : H.Adj x x
h : H.verts = {x}
⊢ False

Tactic:
ha.ne rfl

Premises used: SimpleGraph.Subgraph.Adj.ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
x : V
ha : H.Adj x x
h : H.verts = {x}
⊢ False

Tactic:
exact ha.ne rfl

Premises used: SimpleGraph.Subgraph.Adj.ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : G.Adj v w
⊢ v ∈ (G.subgraphOfAdj hvw).verts

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

Tactic:
rfl

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

Tactic:
ext e