awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
w a b : V
hvw : G.Adj a w
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb_1 : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = a ∨ b = w
inl :
  ∀ (hvw : G.Adj b w) (ha hb : b ∈ (G.subgraphOfAdj hvw).verts),
    (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
inl₁ :
  ∀ (hvw : G.Adj a b) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts),
    (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb_1)

Tactic:
obtain rfl | rfl := hb

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v a b : V
hvw : G.Adj v a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb_1 : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = v ∨ b = a
inr :
  ∀ (hvw : G.Adj b a) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts),
    (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
inr₁ :
  ∀ (hvw : G.Adj v b) (ha hb : b ∈ (G.subgraphOfAdj hvw).verts),
    (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb_1)

Tactic:
obtain rfl | rfl := hb

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
w b : V
hvw : G.Adj b w
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
w b : V
hvw : G.Adj b w
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)

Tactic:
first | rfl | (apply Adj.reachable; simp)

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
inl :
  (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)

Tactic:
apply Adj.reachable

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
inl inl₁ :
  (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)

Tactic:
first | rfl | (apply Adj.reachable; simp)

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
inr :
  (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)

Tactic:
apply Adj.reachable

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
inr inr₁ :
  (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)

Tactic:
first | rfl | (apply Adj.reachable; simp)

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v b : V
hvw : G.Adj v b
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v b : V
hvw : G.Adj v b
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)

Tactic:
first | rfl | (apply Adj.reachable; simp)

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
rw : (G.subgraphOfAdj huv).Connected
⊢ Subgraph.Connected (V := V) (G := G) (induce ⊤ {u, v})

Tactic:
rw [← subgraphOfAdj_eq_induce huv]

Premises used: SimpleGraph.Subgraph.subgraphOfAdj_eq_induce
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (G.subgraphOfAdj huv).Connected

Tactic:
subgraphOfAdj_connected huv

Premises used: SimpleGraph.Subgraph.subgraphOfAdj_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (G.subgraphOfAdj huv).Connected

Tactic:
exact subgraphOfAdj_connected huv

Premises used: SimpleGraph.Subgraph.subgraphOfAdj_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
rw : (H'.copy H.verts hv H'.Adj ⋯).Connected
⊢ H'.Connected

Tactic:
rw [← Subgraph.copy_eq H' H.verts hv H'.Adj rfl]

Premises used: SimpleGraph.Subgraph.copy_eq, SimpleGraph.Subgraph.Adj, SimpleGraph.Subgraph.verts, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ (H'.copy H.verts hv H'.Adj ⋯).Connected

Tactic:
⟨h.coe.mono ?_⟩

Premises used: SimpleGraph.Subgraph.Connected.mk, SimpleGraph.Connected.mono, SimpleGraph.Subgraph.Connected.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
refine : H.coe ≤ (H'.copy H.verts hv H'.Adj ⋯).coe
⊢ (H'.copy H.verts hv H'.Adj ⋯).Connected

Tactic:
refine ⟨h.coe.mono ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv_1 : H.verts = H'.verts
h : H.Connected
v : V
hv : v ∈ H.verts
w : V
hw : w ∈ H.verts
hvw : H.coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw)
⊢ (H'.copy H.verts hv_1 H'.Adj ⋯).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw)

Tactic:
hle.2 hvw

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv_1 : H.verts = H'.verts
h : H.Connected
v : V
hv : v ∈ H.verts
w : V
hw : w ∈ H.verts
hvw : H.coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw)
⊢ (H'.copy H.verts hv_1 H'.Adj ⋯).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw)

Tactic:
exact hle.2 hvw

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : ∀ (v w : V), H.Adj v w → H'.Adj v w
hv : H.verts = H'.verts
h : H.Connected
⊢ H'.Connected

Tactic:
h.mono ⟨hv.le, hle⟩ hv

Premises used: Eq.le, SimpleGraph.Subgraph.Connected.mono, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : ∀ (v w : V), H.Adj v w → H'.Adj v w
hv : H.verts = H'.verts
h : H.Connected
⊢ H'.Connected

Tactic:
exact h.mono ⟨hv.le, hle⟩ hv

Premises used: Eq.le, SimpleGraph.Subgraph.Connected.mono, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
hn : (H ⊓ K).verts.Nonempty
rw : ∃ (v : (↑(H ⊔ K).verts : Type u)), ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable v w
⊢ (H ⊔ K).Connected

Tactic:
rw [Subgraph.connected_iff', connected_iff_exists_forall_reachable]

Premises used: SimpleGraph.Subgraph.connected_iff', SimpleGraph.connected_iff_exists_forall_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
hn : (H ⊓ K).verts.Nonempty
obtain :
  ∀ (u : V) (hu : u ∈ H.verts) (hu' : u ∈ K.verts),
    ∃ (v : (↑(H ⊔ K).verts : Type u)), ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable v w
⊢ ∃ (v : (↑(H ⊔ K).verts : Type u)), ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable v w

Tactic:
obtain ⟨u, hu, hu'⟩ := hn
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
exists :
  ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) u ⋯) w
⊢ ∃ (v : (↑(H ⊔ K).verts : Type u)), ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable v w

Tactic:
exists ⟨u, Or.inl hu⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ H.verts
⊢ (H ⊔ K).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) u ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) v ⋯)

Tactic:
Reachable.map (Subgraph.inclusion (le_sup_left : H ≤ H ⊔ K)) (hH ⟨u, hu⟩ ⟨v, hv⟩)

Premises used: le_sup_left, Set.Mem, SimpleGraph.Subgraph.Preconnected.coe, SimpleGraph.Subgraph.inclusion, Subtype.mk, SimpleGraph.Reachable.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ H.verts
⊢ (H ⊔ K).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) u ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) v ⋯)

Tactic:
exact Reachable.map (Subgraph.inclusion (le_sup_left : H ≤ H ⊔ K)) (hH ⟨u, hu⟩ ⟨v, hv⟩)

Premises used: le_sup_left, SimpleGraph.Subgraph.Preconnected.coe, SimpleGraph.Subgraph.inclusion, Subtype.mk, SimpleGraph.Reachable.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ K.verts
⊢ (H ⊔ K).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) u ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) v ⋯)

Tactic:
Reachable.map (Subgraph.inclusion (le_sup_right : K ≤ H ⊔ K)) (hK ⟨u, hu'⟩ ⟨v, hv⟩)

Premises used: Set.Mem, le_sup_right, SimpleGraph.Subgraph.Preconnected.coe, SimpleGraph.Subgraph.inclusion, Subtype.mk, SimpleGraph.Reachable.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ K.verts
⊢ (H ⊔ K).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) u ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) v ⋯)

Tactic:
exact Reachable.map (Subgraph.inclusion (le_sup_right : K ≤ H ⊔ K)) (hK ⟨u, hu'⟩ ⟨v, hv⟩)

Premises used: le_sup_right, SimpleGraph.Subgraph.Preconnected.coe, SimpleGraph.Subgraph.inclusion, Subtype.mk, SimpleGraph.Reachable.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : (↑H.verts : Type u)
inst : Fintype (↑(H.neighborSet (↑v : V)) : Type u)
⊢ H.degree (↑v : V) = 0 ↔ H.verts.Subsingleton

Tactic:
⟨fun hv ↦ Set.not_nontrivial_iff.mp fun hn ↦ ?_, (degree_eq_zero_of_subsingleton H _ ·)⟩

Premises used: SimpleGraph.Subgraph.degree_eq_zero_of_subsingleton, Set.not_nontrivial_iff, Iff.intro, Iff.mp, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : (↑H.verts : Type u)
inst : Fintype (↑(H.neighborSet (↑v : V)) : Type u)
refine : ∀ (hv : H.degree (↑v : V) = 0) (hn : H.verts.Nontrivial), False
⊢ H.degree (↑v : V) = 0 ↔ H.verts.Subsingleton

Tactic:
refine ⟨fun hv ↦ Set.not_nontrivial_iff.mp fun hn ↦ ?_, (degree_eq_zero_of_subsingleton H _ ·)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : (↑H.verts : Type u)
inst : Fintype (↑(H.neighborSet (↑v : V)) : Type u)
hv : H.degree (↑v : V) = 0
hn : H.verts.Nontrivial
⊢ Nontrivial.{u} (↑H.verts : Type u)

Tactic:
have := hn.coe_sort
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : (↑H.verts : Type u)
inst : Fintype (↑(H.neighborSet (↑v : V)) : Type u)
hv : H.degree (↑v : V) = 0
hn : H.verts.Nontrivial
this : Nontrivial.{u} (↑H.verts : Type u)
⊢ False

Tactic:
simpa [hv] using h.coe.degree_pos_of_nontrivial v

Premises used: SimpleGraph.Preconnected.degree_pos_of_nontrivial, SimpleGraph.Subgraph.Preconnected.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
inst : Nontrivial.{u} (↑H.verts : Type u)
h : H.Preconnected
v : (↑H.verts : Type u)
⊢ ∃ (u : (↑H.verts : Type u)), H.coe.Adj v u

Tactic:
have := h.coe.exists_adj_of_nontrivial v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
inst : Nontrivial.{u} (↑H.verts : Type u)
h : H.Preconnected
v : (↑H.verts : Type u)
this : ∃ (u : (↑H.verts : Type u)), H.coe.Adj v u
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : (↑H.verts : Type u)), H.coe.Adj v w → ∃ (u : V), H.Adj (↑v : V) u
h₁ : ∀ (w : (↑H.verts : Type u)), H.coe.Adj v w → H.Adj (↑v : V) (↑w : V)
w : (w : (↑H.verts : Type u)) → H.coe.Adj v w → V
h₂ : ∀ (w : (↑H.verts : Type u)), H.coe.Adj v w → H.Adj (↑v : V) (↑w : V)
w₁ : (w : (↑H.verts : Type u)) → H.coe.Adj v w → V
⊢ ∃ (u : V), H.Adj (↑v : V) u

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
rw : ∃ (v : V), H.verts = (G.connectedComponentMk v).supp
⊢ ∃ (c : G.ConnectedComponent), H.verts = c.supp

Tactic:
rw [SimpleGraph.ConnectedComponent.exists]

Premises used: SimpleGraph.ConnectedComponent.exists
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
obtain : ∀ (v : V) (hv : v ∈ H.verts), ∃ (v : V), H.verts = (G.connectedComponentMk v).supp
⊢ ∃ (v : V), H.verts = (G.connectedComponentMk v).supp

Tactic:
obtain ⟨v, hv⟩ := hc.nonempty

Premises used: SimpleGraph.Subgraph.Connected.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
h₁ : H.verts = (G.connectedComponentMk v).supp
⊢ ∃ (v : V), H.verts = (G.connectedComponentMk v).supp

Tactic:
use v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
h₁ : ∀ (w : V), w ∈ H.verts ↔ w ∈ (G.connectedComponentMk v).supp
⊢ H.verts = (G.connectedComponentMk v).supp

Tactic:
ext w
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
h₁ : w ∈ H.verts ↔ G.Reachable w v
⊢ w ∈ H.verts ↔ w ∈ (G.connectedComponentMk v).supp

Tactic:
simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff, SimpleGraph.ConnectedComponent.eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
hw : w ∈ H.verts
⊢ G.Reachable w v

Tactic:
simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom

Premises used: SimpleGraph.Subgraph.hom, SimpleGraph.Subgraph.instCoeFunConnectedForallForallReachableElemVertsCoe._proof_1, Subtype.mk, SimpleGraph.Reachable.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
⊢ w ∈ H.verts ↔ G.Reachable w v

Tactic:
exact ⟨fun hw ↦ by simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom,
    fun a ↦ a.symm.mem_subgraphVerts h hv⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ C.toSubgraph.coe = C.toSimpleGraph

Tactic:
induce_eq_coe_induce_top C.supp |>.symm

Premises used: SimpleGraph.induce_eq_coe_induce_top, setOf, SimpleGraph.ConnectedComponent.toSimpleGraph, Eq.symm, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ C.toSubgraph.spanningCoe = C.toSimpleGraph.spanningCoe (s := (↑C : Set V))

Tactic:
spanningCoe_induce_top _

Premises used: SimpleGraph.spanningCoe_induce_top, Set.Mem, SimpleGraph.ConnectedComponent.toSimpleGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ C.toSubgraph.Connected

Tactic:
⟨C.coe_toSubgraph ▸ C.connected_toSimpleGraph⟩

Premises used: SimpleGraph.ConnectedComponent.coe_toSubgraph, Eq.rec, SimpleGraph.Subgraph.Connected.mk, SimpleGraph.ConnectedComponent.connected_toSimpleGraph, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ Maximal Subgraph.Connected C.toSubgraph

Tactic:
C.ind fun v ↦ ⟨connected_toSubgraph _, fun G' hconn hle ↦ ?_⟩

Premises used: SimpleGraph.ConnectedComponent.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
refine :
  ∀ (v : V) (G' : G.Subgraph) (hconn : G'.Connected) (hle : (G.connectedComponentMk v).toSubgraph ≤ G'),
    G' ≤ (G.connectedComponentMk v).toSubgraph
⊢ Maximal Subgraph.Connected C.toSubgraph

Tactic:
refine C.ind fun v ↦ ⟨connected_toSubgraph _, fun G' hconn hle ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
G' : G.Subgraph
hconn : G'.Connected
hle : (G.connectedComponentMk v).toSubgraph ≤ G'
⊢ G' ≤ (G.connectedComponentMk v).toSubgraph

Tactic:
le_trans Subgraph.le_induce_top_verts <| Subgraph.induce_mono_right fun u hu ↦ ?_

Premises used: SimpleGraph.Subgraph.le_induce_top_verts, SimpleGraph.Subgraph.induce_mono_right, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
G' : G.Subgraph
hconn : G'.Connected
hle : (G.connectedComponentMk v).toSubgraph ≤ G'
refine : ∀ (u : V) (hu : u ∈ G'.verts), u ∈ (G.connectedComponentMk v).supp
⊢ G' ≤ (G.connectedComponentMk v).toSubgraph

Tactic:
refine le_trans Subgraph.le_induce_top_verts <| Subgraph.induce_mono_right fun u hu ↦ ?_

Premises used: SimpleGraph.Subgraph.le_induce_top_verts, SimpleGraph.Subgraph.induce_mono_right, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
G' : G.Subgraph
hconn : G'.Connected
hle : (G.connectedComponentMk v).toSubgraph ≤ G'
u : V
hu : u ∈ G'.verts
⊢ u ∈ (G.connectedComponentMk v).supp

Tactic:
ConnectedComponent.sound <| hconn.coe.preconnected ⟨u, hu⟩ ⟨v, hle.left rfl⟩ |>.map G'.hom

Premises used: SimpleGraph.Connected.preconnected, Set.Mem, setOf, SimpleGraph.Subgraph.hom, Subtype.mk, SimpleGraph.Reachable.map, And.left, SimpleGraph.ConnectedComponent.sound, rfl, SimpleGraph.ConnectedComponent.supp, SimpleGraph.Subgraph.Connected.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
G' : G.Subgraph
hconn : G'.Connected
hle : (G.connectedComponentMk v).toSubgraph ≤ G'
u : V
hu : u ∈ G'.verts
⊢ u ∈ (G.connectedComponentMk v).supp

Tactic:
exact ConnectedComponent.sound <| hconn.coe.preconnected ⟨u, hu⟩ ⟨v, hle.left rfl⟩ |>.map G'.hom

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Subgraph.hom, Subtype.mk, SimpleGraph.Reachable.map, And.left, SimpleGraph.ConnectedComponent.sound, rfl, SimpleGraph.Subgraph.Connected.coe