[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ : SimpleGraph α
H✝ : SimpleGraph β
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (fun x y => Adj G x.fst y.fst ∧ x.snd = y.snd ∨ Adj H x.snd y.snd ∧ x.fst = y.fst) x y →
    (fun x y => Adj G x.fst y.fst ∧ x.snd = y.snd ∨ Adj H x.snd y.snd ∧ x.fst = y.fst) y x
[PROOFSTEP]
simp [and_comm, or_comm, eq_comm, adj_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ : SimpleGraph α
H✝ : SimpleGraph β
G : SimpleGraph α
H : SimpleGraph β
x : α × β
⊢ ¬(fun x y => Adj G x.fst y.fst ∧ x.snd = y.snd ∨ Adj H x.snd y.snd ∧ x.fst = y.fst) x x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a₁ : α
b : β
a₂ : α
⊢ Adj (G □ H) (a₁, b) (a₂, b) ↔ Adj G a₁ a₂
[PROOFSTEP]
simp only [boxProd_adj, and_true, SimpleGraph.irrefl, false_and, or_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a : α
b₁ b₂ : β
⊢ Adj (G □ H) (a, b₁) (a, b₂) ↔ Adj H b₁ b₂
[PROOFSTEP]
simp only [boxProd_adj, SimpleGraph.irrefl, false_and, and_true, false_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
⊢ neighborSet (G □ H) x = neighborSet G x.fst ×ˢ {x.snd} ∪ {x.fst} ×ˢ neighborSet H x.snd
[PROOFSTEP]
ext ⟨a', b'⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ (a', b') ∈ neighborSet (G □ H) x ↔ (a', b') ∈ neighborSet G x.fst ×ˢ {x.snd} ∪ {x.fst} ×ˢ neighborSet H x.snd
[PROOFSTEP]
simp only [mem_neighborSet, Set.mem_union, boxProd_adj, Set.mem_prod, Set.mem_singleton_iff]
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ Adj G x.fst a' ∧ x.snd = b' ∨ Adj H x.snd b' ∧ x.fst = a' ↔ Adj G x.fst a' ∧ b' = x.snd ∨ a' = x.fst ∧ Adj H x.snd b'
[PROOFSTEP]
simp only [eq_comm, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
x y : (α × β) × γ
⊢ Adj (G □ (H □ I)) (↑(Equiv.prodAssoc α β γ) x) (↑(Equiv.prodAssoc α β γ) y) ↔ Adj (G □ H □ I) x y
[PROOFSTEP]
simp only [boxProd_adj, Equiv.prodAssoc_apply, or_and_right, or_assoc, Prod.ext_iff, and_assoc,
  @and_comm (x.fst.fst = _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
b : β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ ofBoxProdLeft (Walk.boxProdLeft H b (cons' x y z h w)) = cons' x y z h w
[PROOFSTEP]
rw [Walk.boxProdLeft, map_cons, ofBoxProdLeft, Or.by_cases, dif_pos, ← Walk.boxProdLeft]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
b : β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ cons (_ : Adj G (x, b).fst (↑(Embedding.toHom (boxProdLeft G H b)) y).fst) (ofBoxProdLeft (Walk.boxProdLeft H b w)) =
    cons' x y z h w
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
b : β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (x, b).fst (↑(Embedding.toHom (boxProdLeft G H b)) y).fst ∧
    (x, b).snd = (↑(Embedding.toHom (boxProdLeft G H b)) y).snd
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
b : β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (x, b).fst (↑(Embedding.toHom (boxProdLeft G H b)) y).fst ∧
    (x, b).snd = (↑(Embedding.toHom (boxProdLeft G H b)) y).snd
[PROOFSTEP]
simp [ofBoxProdLeft_boxProdLeft]
[GOAL]
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
b : β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (x, b).fst (↑(Embedding.toHom (boxProdLeft G H b)) y).fst ∧
    (x, b).snd = (↑(Embedding.toHom (boxProdLeft G H b)) y).snd
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
b : β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (x, b).fst (↑(Embedding.toHom (boxProdLeft G H b)) y).fst ∧
    (x, b).snd = (↑(Embedding.toHom (boxProdLeft G H b)) y).snd
[PROOFSTEP]
exact ⟨h, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ ofBoxProdRight (Walk.boxProdRight G a (cons' x y z h w)) = cons' x y z h w
[PROOFSTEP]
rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ← Walk.boxProdRight]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ cons (_ : Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd)
      (ofBoxProdRight (Walk.boxProdRight G a w)) =
    cons' x y z h w
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst
[PROOFSTEP]
simp [ofBoxProdLeft_boxProdRight]
[GOAL]
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst
[PROOFSTEP]
exact ⟨h, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
⊢ Preconnected (G □ H)
[PROOFSTEP]
rintro x y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
x y : α × β
⊢ Reachable (G □ H) x y
[PROOFSTEP]
obtain ⟨w₁⟩ := hG x.1 y.1
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
x y : α × β
w₁ : Walk G x.fst y.fst
⊢ Reachable (G □ H) x y
[PROOFSTEP]
obtain ⟨w₂⟩ := hH x.2 y.2
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
x y : α × β
w₁ : Walk G x.fst y.fst
w₂ : Walk H x.snd y.snd
⊢ Reachable (G □ H) x y
[PROOFSTEP]
rw [← @Prod.mk.eta _ _ x, ← @Prod.mk.eta _ _ y]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
x y : α × β
w₁ : Walk G x.fst y.fst
w₂ : Walk H x.snd y.snd
⊢ Reachable (G □ H) (x.fst, x.snd) (y.fst, y.snd)
[PROOFSTEP]
exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : Preconnected (G □ H)
⊢ Preconnected G
[PROOFSTEP]
classical
rintro a₁ a₂
obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
exact ⟨w.ofBoxProdLeft⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : Preconnected (G □ H)
⊢ Preconnected G
[PROOFSTEP]
rintro a₁ a₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : Preconnected (G □ H)
a₁ a₂ : α
⊢ Reachable G a₁ a₂
[PROOFSTEP]
obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : Preconnected (G □ H)
a₁ a₂ : α
w : Walk (G □ H) (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)
⊢ Reachable G a₁ a₂
[PROOFSTEP]
exact ⟨w.ofBoxProdLeft⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
⊢ Preconnected H
[PROOFSTEP]
classical
rintro b₁ b₂
obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
exact ⟨w.ofBoxProdRight⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
⊢ Preconnected H
[PROOFSTEP]
rintro b₁ b₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
b₁ b₂ : β
⊢ Reachable H b₁ b₂
[PROOFSTEP]
obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
b₁ b₂ : β
w : Walk (G □ H) (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)
⊢ Reachable H b₁ b₂
[PROOFSTEP]
exact ⟨w.ofBoxProdRight⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
⊢ Connected (G □ H)
[PROOFSTEP]
haveI := hG.nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
this : Nonempty α
⊢ Connected (G □ H)
[PROOFSTEP]
haveI := hH.nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
this✝ : Nonempty α
this : Nonempty β
⊢ Connected (G □ H)
[PROOFSTEP]
exact ⟨hG.preconnected.boxProd hH.preconnected⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
⊢ Connected G
[PROOFSTEP]
haveI := (nonempty_prod.1 h.nonempty).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this : Nonempty α
⊢ Connected G
[PROOFSTEP]
haveI := (nonempty_prod.1 h.nonempty).2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this✝ : Nonempty α
this : Nonempty β
⊢ Connected G
[PROOFSTEP]
exact ⟨h.preconnected.ofBoxProdLeft⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
⊢ Connected H
[PROOFSTEP]
haveI := (nonempty_prod.1 h.nonempty).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this : Nonempty α
⊢ Connected H
[PROOFSTEP]
haveI := (nonempty_prod.1 h.nonempty).2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this✝ : Nonempty α
this : Nonempty β
⊢ Connected H
[PROOFSTEP]
exact ⟨h.preconnected.ofBoxProdRight⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(neighborSet G x.fst)
inst✝ : Fintype ↑(neighborSet H x.snd)
y : α × β
⊢ y ∈
      Finset.disjUnion (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)
        (_ : Disjoint (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)) ↔
    ↑(Equiv.refl (α × β)) y ∈ neighborSet (G □ H) x
[PROOFSTEP]
simp_rw [Finset.mem_disjUnion, Finset.mem_product, Finset.mem_singleton, mem_neighborFinset, mem_neighborSet,
  Equiv.refl_apply, boxProd_adj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(neighborSet G x.fst)
inst✝ : Fintype ↑(neighborSet H x.snd)
y : α × β
⊢ Adj G x.fst y.fst ∧ y.snd = x.snd ∨ y.fst = x.fst ∧ Adj H x.snd y.snd ↔
    Adj G x.fst y.fst ∧ x.snd = y.snd ∨ Adj H x.snd y.snd ∧ x.fst = y.fst
[PROOFSTEP]
simp only [eq_comm, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
⊢ neighborFinset (G □ H) x =
    Finset.disjUnion (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)
      (_ : Disjoint (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd))
[PROOFSTEP]
letI : Fintype ((G □ H).neighborSet x) := SimpleGraph.boxProdFintypeNeighborSet _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
this : Fintype ↑(neighborSet (G □ H) x) := boxProdFintypeNeighborSet x
⊢ neighborFinset (G □ H) x =
    Finset.disjUnion (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)
      (_ : Disjoint (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd))
[PROOFSTEP]
convert_to (G □ H).neighborFinset x = _ using 2
[GOAL]
case convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
this : Fintype ↑(neighborSet (G □ H) x) := boxProdFintypeNeighborSet x
⊢ neighborFinset (G □ H) x =
    Finset.disjUnion (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)
      (_ : Disjoint (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd))
[PROOFSTEP]
exact Eq.trans (Finset.map_map _ _ _) Finset.attach_map_val
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
⊢ degree (G □ H) x = degree G x.fst + degree H x.snd
[PROOFSTEP]
rw [degree, degree, degree, boxProd_neighborFinset, Finset.card_disjUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
⊢ Finset.card (neighborFinset G x.fst ×ˢ {x.snd}) + Finset.card ({x.fst} ×ˢ neighborFinset H x.snd) =
    Finset.card (neighborFinset G x.fst) + Finset.card (neighborFinset H x.snd)
[PROOFSTEP]
simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]


[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ Subgraph.Connected H ↔ Subgraph.Preconnected H ∧ Set.Nonempty H.verts
[PROOFSTEP]
rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ Subgraph.Preconnected H
[PROOFSTEP]
rw [H.connected_iff] at h
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Preconnected H ∧ Set.Nonempty H.verts
⊢ Subgraph.Preconnected H
[PROOFSTEP]
exact h.1
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ Set.Nonempty H.verts
[PROOFSTEP]
rw [H.connected_iff] at h
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Preconnected H ∧ Set.Nonempty H.verts
⊢ Set.Nonempty H.verts
[PROOFSTEP]
exact h.2
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v : V
⊢ Subgraph.Connected (SimpleGraph.singletonSubgraph G v)
[PROOFSTEP]
refine ⟨⟨?_⟩⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v : V
⊢ Preconnected (Subgraph.coe (SimpleGraph.singletonSubgraph G v))
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v a : V
ha : a ∈ (SimpleGraph.singletonSubgraph G v).verts
b : V
hb : b ∈ (SimpleGraph.singletonSubgraph G v).verts
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G v)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
simp only [singletonSubgraph_verts, Set.mem_singleton_iff] at ha hb
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v a : V
ha✝ : a ∈ (SimpleGraph.singletonSubgraph G v).verts
b : V
hb✝ : b ∈ (SimpleGraph.singletonSubgraph G v).verts
ha : a = v
hb : b = v
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G v)) { val := a, property := ha✝ }
    { val := b, property := hb✝ }
[PROOFSTEP]
subst_vars
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
b : V
ha hb : b = b
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G b)) { val := b, property := (_ : b = b) }
    { val := b, property := (_ : b = b) }
[PROOFSTEP]
rfl
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
hvw : SimpleGraph.Adj G v w
⊢ Subgraph.Connected (subgraphOfAdj G hvw)
[PROOFSTEP]
refine ⟨⟨?_⟩⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
hvw : SimpleGraph.Adj G v w
⊢ Preconnected (Subgraph.coe (subgraphOfAdj G hvw))
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
hvw : SimpleGraph.Adj G v w
a : V
ha : a ∈ (subgraphOfAdj G hvw).verts
b : V
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
simp only [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
hvw : SimpleGraph.Adj G v w
a : V
ha✝ : a ∈ (subgraphOfAdj G hvw).verts
b : V
hb✝ : b ∈ (subgraphOfAdj G hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha✝ } { val := b, property := hb✝ }
[PROOFSTEP]
obtain rfl | rfl := ha
[GOAL]
case mk.mk.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
w a b : V
hvw : SimpleGraph.Adj G a w
ha : a ∈ (subgraphOfAdj G hvw).verts
hb✝ : b ∈ (subgraphOfAdj G hvw).verts
hb : b = a ∨ b = w
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb✝ }
[PROOFSTEP]
obtain rfl | rfl := hb
[GOAL]
case mk.mk.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v a b : V
hvw : SimpleGraph.Adj G v a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb✝ : b ∈ (subgraphOfAdj G hvw).verts
hb : b = v ∨ b = a
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb✝ }
[PROOFSTEP]
obtain rfl | rfl := hb
[GOAL]
case mk.mk.inl.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
w b : V
hvw : SimpleGraph.Adj G b w
ha hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := b, property := ha } { val := b, property := hb }
[PROOFSTEP]
first
| rfl
| (apply Adj.reachable; simp)
[GOAL]
case mk.mk.inl.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
w b : V
hvw : SimpleGraph.Adj G b w
ha hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := b, property := ha } { val := b, property := hb }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inl.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G a b
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
first
| rfl
| (apply Adj.reachable; simp)
[GOAL]
case mk.mk.inl.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G a b
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inl.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G a b
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
apply Adj.reachable
[GOAL]
case mk.mk.inl.inr.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G a b
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ SimpleGraph.Adj (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inr.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
first
| rfl
| (apply Adj.reachable; simp)
[GOAL]
case mk.mk.inr.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inr.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
apply Adj.reachable
[GOAL]
case mk.mk.inr.inl.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ SimpleGraph.Adj (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inr.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v b : V
hvw : SimpleGraph.Adj G v b
ha hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := b, property := ha } { val := b, property := hb }
[PROOFSTEP]
first
| rfl
| (apply Adj.reachable; simp)
[GOAL]
case mk.mk.inr.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v b : V
hvw : SimpleGraph.Adj G v b
ha hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := b, property := ha } { val := b, property := hb }
[PROOFSTEP]
rfl
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
huv : SimpleGraph.Adj G u v
⊢ Subgraph.Connected (induce ⊤ {u, v})
[PROOFSTEP]
rw [← subgraphOfAdj_eq_induce huv]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
huv : SimpleGraph.Adj G u v
⊢ Subgraph.Connected (subgraphOfAdj G huv)
[PROOFSTEP]
exact subgraphOfAdj_connected huv
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : H ≤ H'
hv : H.verts = H'.verts
h : Subgraph.Connected H
⊢ Subgraph.Connected H'
[PROOFSTEP]
rw [← Subgraph.copy_eq H' H.verts hv H'.Adj rfl]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : H ≤ H'
hv : H.verts = H'.verts
h : Subgraph.Connected H
⊢ Subgraph.Connected (copy H' H.verts hv H'.Adj (_ : H'.Adj = H'.Adj))
[PROOFSTEP]
refine ⟨h.coe.mono ?_⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : H ≤ H'
hv : H.verts = H'.verts
h : Subgraph.Connected H
⊢ Subgraph.coe H ≤ Subgraph.coe (copy H' H.verts hv H'.Adj (_ : H'.Adj = H'.Adj))
[PROOFSTEP]
rintro ⟨v, hv⟩ ⟨w, hw⟩ hvw
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : H ≤ H'
hv✝ : H.verts = H'.verts
h : Subgraph.Connected H
v : V
hv : v ∈ H.verts
w : V
hw : w ∈ H.verts
hvw : SimpleGraph.Adj (Subgraph.coe H) { val := v, property := hv } { val := w, property := hw }
⊢ SimpleGraph.Adj (Subgraph.coe (copy H' H.verts hv✝ H'.Adj (_ : H'.Adj = H'.Adj))) { val := v, property := hv }
    { val := w, property := hw }
[PROOFSTEP]
exact hle.2 hvw
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : ∀ (v w : V), Adj H v w → Adj H' v w
hv : H.verts = H'.verts
h : Subgraph.Connected H
⊢ Subgraph.Connected H'
[PROOFSTEP]
exact h.mono ⟨hv.le, hle⟩ hv
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
hn : Set.Nonempty (H ⊓ K).verts
⊢ Subgraph.Connected (H ⊔ K)
[PROOFSTEP]
rw [Subgraph.connected_iff', connected_iff_exists_forall_reachable]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
hn : Set.Nonempty (H ⊓ K).verts
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), Reachable (Subgraph.coe (H ⊔ K)) v w
[PROOFSTEP]
obtain ⟨u, hu, hu'⟩ := hn
[GOAL]
case intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), Reachable (Subgraph.coe (H ⊔ K)) v w
[PROOFSTEP]
exists ⟨u, Or.inl hu⟩
[GOAL]
case intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
⊢ ∀ (w : ↑(H ⊔ K).verts), Reachable (Subgraph.coe (H ⊔ K)) { val := u, property := (_ : u ∈ H.verts ∨ u ∈ K.verts) } w
[PROOFSTEP]
rintro ⟨v, (hv | hv)⟩
[GOAL]
case intro.intro.mk.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ H.verts
⊢ Reachable (Subgraph.coe (H ⊔ K)) { val := u, property := (_ : u ∈ H.verts ∨ u ∈ K.verts) }
    { val := v, property := (_ : v ∈ H.verts ∨ v ∈ K.verts) }
[PROOFSTEP]
exact Reachable.map (Subgraph.inclusion (le_sup_left : H ≤ H ⊔ K)) (hH ⟨u, hu⟩ ⟨v, hv⟩)
[GOAL]
case intro.intro.mk.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ K.verts
⊢ Reachable (Subgraph.coe (H ⊔ K)) { val := u, property := (_ : u ∈ H.verts ∨ u ∈ K.verts) }
    { val := v, property := (_ : v ∈ H.verts ∨ v ∈ K.verts) }
[PROOFSTEP]
exact Reachable.map (Subgraph.inclusion (le_sup_right : K ≤ H ⊔ K)) (hK ⟨u, hu'⟩ ⟨v, hv⟩)
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : Walk G u v
⊢ Subgraph.Connected (Walk.toSubgraph p)
[PROOFSTEP]
induction p with
| nil => apply singletonSubgraph_connected
| cons h p ih =>
  apply (subgraphOfAdj_connected h).sup ih
  rename_i w _
  exists w
  simp
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : Walk G u v
⊢ Subgraph.Connected (Walk.toSubgraph p)
[PROOFSTEP]
induction p with
| nil => apply singletonSubgraph_connected
| cons h p ih =>
  apply (subgraphOfAdj_connected h).sup ih
  rename_i w _
  exists w
  simp
[GOAL]
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ : V
⊢ Subgraph.Connected (Walk.toSubgraph Walk.nil)
[PROOFSTEP]

| nil => apply singletonSubgraph_connected
[GOAL]
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ : V
⊢ Subgraph.Connected (Walk.toSubgraph Walk.nil)
[PROOFSTEP]
apply singletonSubgraph_connected
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ v✝ w✝ : V
h : SimpleGraph.Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ Subgraph.Connected (Walk.toSubgraph (Walk.cons h p))
[PROOFSTEP]

| cons h p ih =>
  apply (subgraphOfAdj_connected h).sup ih
  rename_i w _
  exists w
  simp
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ v✝ w✝ : V
h : SimpleGraph.Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ Subgraph.Connected (Walk.toSubgraph (Walk.cons h p))
[PROOFSTEP]
apply (subgraphOfAdj_connected h).sup ih
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ v✝ w✝ : V
h : SimpleGraph.Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ Set.Nonempty (subgraphOfAdj G h ⊓ Walk.toSubgraph p).verts
[PROOFSTEP]
rename_i w _
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ w w✝ : V
h : SimpleGraph.Adj G u✝ w
p : Walk G w w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ Set.Nonempty (subgraphOfAdj G h ⊓ Walk.toSubgraph p).verts
[PROOFSTEP]
exists w
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ w w✝ : V
h : SimpleGraph.Adj G u✝ w
p : Walk G w w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ w ∈ (subgraphOfAdj G h ⊓ Walk.toSubgraph p).verts
[PROOFSTEP]
simp
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
s t : Set V
sconn : Subgraph.Connected (induce H s)
tconn : Subgraph.Connected (induce H t)
sintert : Set.Nonempty (s ⊓ t)
⊢ Subgraph.Connected (induce H (s ∪ t))
[PROOFSTEP]
refine (sconn.sup tconn sintert).mono ?_ ?_
[GOAL]
case refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
s t : Set V
sconn : Subgraph.Connected (induce H s)
tconn : Subgraph.Connected (induce H t)
sintert : Set.Nonempty (s ⊓ t)
⊢ induce H s ⊔ induce H t ≤ induce H (s ∪ t)
[PROOFSTEP]
apply le_induce_union
[GOAL]
case refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
s t : Set V
sconn : Subgraph.Connected (induce H s)
tconn : Subgraph.Connected (induce H t)
sintert : Set.Nonempty (s ⊓ t)
⊢ (induce H s ⊔ induce H t).verts = (induce H (s ∪ t)).verts
[PROOFSTEP]
simp
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ Subgraph.Connected (induce ⊤ {u, v} ⊔ H ⊔ K)
[PROOFSTEP]
refine ((top_induce_pair_connected_of_adj huv).sup Hconn ?_).sup Kconn ?_
[GOAL]
case refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ Set.Nonempty (induce ⊤ {u, v} ⊓ H).verts
[PROOFSTEP]
exact ⟨u, by simp [uH]⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ u ∈ (induce ⊤ {u, v} ⊓ H).verts
[PROOFSTEP]
simp [uH]
[GOAL]
case refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ Set.Nonempty ((induce ⊤ {u, v} ⊔ H) ⊓ K).verts
[PROOFSTEP]
exact ⟨v, by simp [vK]⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ v ∈ ((induce ⊤ {u, v} ⊔ H) ⊓ K).verts
[PROOFSTEP]
simp [vK]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ Subgraph.Preconnected H ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ Subgraph.Preconnected H → ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
intro hc u v hu hv
[GOAL]
case mp
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hc : Subgraph.Preconnected H
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
⊢ ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
refine (hc ⟨_, hu⟩ ⟨_, hv⟩).elim fun p => ?_
[GOAL]
case mp
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hc : Subgraph.Preconnected H
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : Walk (Subgraph.coe H) { val := u, property := hu } { val := v, property := hv }
⊢ ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
exists p.map (Subgraph.hom _)
[GOAL]
case mp
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hc : Subgraph.Preconnected H
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : Walk (Subgraph.coe H) { val := u, property := hu } { val := v, property := hv }
⊢ Walk.toSubgraph (Walk.map (Subgraph.hom H) p) ≤ H
[PROOFSTEP]
simp [coeSubgraph_le]
[GOAL]
case mpr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H) → Subgraph.Preconnected H
[PROOFSTEP]
intro hw
[GOAL]
case mpr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
⊢ Subgraph.Preconnected H
[PROOFSTEP]
rw [Subgraph.preconnected_iff]
[GOAL]
case mpr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
⊢ Preconnected (Subgraph.coe H)
[PROOFSTEP]
rintro ⟨u, hu⟩ ⟨v, hv⟩
[GOAL]
case mpr.mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
⊢ Reachable (Subgraph.coe H) { val := u, property := hu } { val := v, property := hv }
[PROOFSTEP]
obtain ⟨p, h⟩ := hw hu hv
[GOAL]
case mpr.mk.mk.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
p : Walk G u v
h : Walk.toSubgraph p ≤ H
⊢ Reachable (Subgraph.coe H) { val := u, property := hu } { val := v, property := hv }
[PROOFSTEP]
exact
  Reachable.map (Subgraph.inclusion h)
    (p.toSubgraph_connected ⟨_, p.start_mem_verts_toSubgraph⟩ ⟨_, p.end_mem_verts_toSubgraph⟩)
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ Subgraph.Connected H ↔ Set.Nonempty H.verts ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
rw [H.connected_iff, preconnected_iff_forall_exists_walk_subgraph, and_comm]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
⊢ Connected (induce s G) ↔ Subgraph.Connected (Subgraph.induce ⊤ s)
[PROOFSTEP]
rw [induce_eq_coe_induce_top, ← Subgraph.connected_iff']
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s t : Set V
sconn : Connected (induce s G)
tconn : Connected (induce t G)
sintert : Set.Nonempty (s ∩ t)
⊢ Connected (induce (s ∪ t) G)
[PROOFSTEP]
rw [connected_induce_iff] at sconn tconn ⊢
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
sintert : Set.Nonempty (s ∩ t)
⊢ Subgraph.Connected (Subgraph.induce ⊤ (s ∪ t))
[PROOFSTEP]
exact Subgraph.induce_union_connected sconn tconn sintert
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
huv : Adj G u v
⊢ Connected (induce {u, v} G)
[PROOFSTEP]
rw [connected_induce_iff]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
huv : Adj G u v
⊢ Subgraph.Connected (Subgraph.induce ⊤ {u, v})
[PROOFSTEP]
exact Subgraph.top_induce_pair_connected_of_adj huv
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ Connected (SimpleGraph.induce H.verts G)
[PROOFSTEP]
rw [connected_induce_iff]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ Subgraph.Connected (induce ⊤ H.verts)
[PROOFSTEP]
exact h.mono le_induce_top_verts (by exact rfl)
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ H.verts = (induce ⊤ H.verts).verts
[PROOFSTEP]
exact rfl
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : Walk G u v
⊢ Connected (induce {v_1 | v_1 ∈ support p} G)
[PROOFSTEP]
rw [← p.verts_toSubgraph]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : Walk G u v
⊢ Connected (induce (Walk.toSubgraph p).verts G)
[PROOFSTEP]
exact p.toSubgraph_connected.induce_verts
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Connected (induce s G)
tconn : Connected (induce t G)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ Connected (induce (s ∪ t) G)
[PROOFSTEP]
rw [connected_induce_iff] at sconn tconn ⊢
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ Subgraph.Connected (Subgraph.induce ⊤ (s ∪ t))
[PROOFSTEP]
apply (sconn.adj_union tconn hv hw ha).mono
[GOAL]
case hle
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t ≤ Subgraph.induce ⊤ (s ∪ t)
[PROOFSTEP]
simp only [Set.mem_singleton_iff, sup_le_iff, Subgraph.le_induce_union_left, Subgraph.le_induce_union_right, and_true, ←
  Subgraph.subgraphOfAdj_eq_induce ha]
[GOAL]
case hle
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ subgraphOfAdj G ha ≤ Subgraph.induce ⊤ (s ∪ t)
[PROOFSTEP]
apply subgraphOfAdj_le_of_adj
[GOAL]
case hle.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ Subgraph.Adj (Subgraph.induce ⊤ (s ∪ t)) v w
[PROOFSTEP]
simp [hv, hw, ha]
[GOAL]
case hv
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t).verts = (Subgraph.induce ⊤ (s ∪ t)).verts
[PROOFSTEP]
simp only [Set.mem_singleton_iff, sup_le_iff, Subgraph.verts_sup, Subgraph.induce_verts]
[GOAL]
case hv
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ {v, w} ∪ s ∪ t = s ∪ t
[PROOFSTEP]
rw [Set.union_assoc]
[GOAL]
case hv
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ {v, w} ∪ (s ∪ t) = s ∪ t
[PROOFSTEP]
simp [Set.insert_subset_iff, Set.singleton_subset_iff, hv, hw]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
⊢ Connected (induce s G)
[PROOFSTEP]
rw [connected_iff_exists_forall_reachable]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
⊢ ∃ v, ∀ (w : ↑s), Reachable (induce s G) v w
[PROOFSTEP]
refine ⟨⟨u, hu⟩, ?_⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
⊢ ∀ (w : ↑s), Reachable (induce s G) { val := u, property := hu } w
[PROOFSTEP]
rintro ⟨v, hv⟩
[GOAL]
case mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
v : V
hv : v ∈ s
⊢ Reachable (induce s G) { val := u, property := hu } { val := v, property := hv }
[PROOFSTEP]
obtain ⟨sv, svs, hu', hv', uv⟩ := patches hv
[GOAL]
case mk.intro.intro.intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
v : V
hv : v ∈ s
sv : Set V
svs : sv ⊆ s
hu' : u ∈ sv
hv' : v ∈ sv
uv : Reachable (induce sv G) { val := u, property := hu' } { val := v, property := hv' }
⊢ Reachable (induce s G) { val := u, property := hu } { val := v, property := hv }
[PROOFSTEP]
exact uv.map (induceHomOfLE _ svs).toHom
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Sn : Set.Nonempty S
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
⊢ Connected (induce (⋃₀ S) G)
[PROOFSTEP]
obtain ⟨s, sS⟩ := Sn
[GOAL]
case intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
⊢ Connected (induce (⋃₀ S) G)
[PROOFSTEP]
obtain ⟨v, vs⟩ := (Sc sS).nonempty
[GOAL]
case intro.intro.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ Connected (induce (⋃₀ S) G)
[PROOFSTEP]
apply G.induce_connected_of_patches _ (Set.subset_sUnion_of_mem sS vs)
[GOAL]
case intro.intro.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ ∀ {v_1 : V},
    v_1 ∈ ⋃₀ S → ∃ s' x hu' hv', Reachable (induce s' G) { val := v, property := hu' } { val := v_1, property := hv' }
[PROOFSTEP]
rintro w hw
[GOAL]
case intro.intro.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : w ∈ ⋃₀ S
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := v, property := hu' } { val := w, property := hv' }
[PROOFSTEP]
simp only [Set.mem_sUnion, exists_prop] at hw
[GOAL]
case intro.intro.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : ∃ t, t ∈ S ∧ w ∈ t
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := v, property := hu' } { val := w, property := hv' }
[PROOFSTEP]
obtain ⟨t, tS, wt⟩ := hw
[GOAL]
case intro.intro.mk.intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
t : Set V
tS : t ∈ S
wt : w ∈ t
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := v, property := hu' } { val := w, property := hv' }
[PROOFSTEP]
refine
  ⟨s ∪ t, Set.union_subset (Set.subset_sUnion_of_mem sS) (Set.subset_sUnion_of_mem tS), Or.inl vs, Or.inr wt,
    induce_union_connected (Sc sS) (Sc tS) (Snd sS tS) _ _⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
tn : Finset.Nonempty t
⊢ ∃ t', t ⊆ t' ∧ Connected (induce (↑t') G)
[PROOFSTEP]
classical
obtain ⟨u, ut⟩ := tn
refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
· simp only [Finset.mem_biUnion, List.mem_toFinset, exists_prop]
  refine ⟨v, vt, Walk.end_mem_support _⟩
· apply G.induce_connected_of_patches u
  · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion, Set.mem_setOf_eq,
      Walk.start_mem_support, exists_prop, and_true]
    exact ⟨u, ut⟩
  intros v hv
  simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset, exists_prop] at hv
  obtain ⟨w, wt, hw⟩ := hv
  refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
  · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
    exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
  · simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
    refine ⟨hw, Walk.connected_induce_support _ _ _⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
tn : Finset.Nonempty t
⊢ ∃ t', t ⊆ t' ∧ Connected (induce (↑t') G)
[PROOFSTEP]
obtain ⟨u, ut⟩ := tn
[GOAL]
case intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ t', t ⊆ t' ∧ Connected (induce (↑t') G)
[PROOFSTEP]
refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
[GOAL]
case intro.refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ v ∈ Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v)))
[PROOFSTEP]
simp only [Finset.mem_biUnion, List.mem_toFinset, exists_prop]
[GOAL]
case intro.refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ ∃ a, a ∈ t ∧ v ∈ Walk.support (Nonempty.some (_ : Reachable G u a))
[PROOFSTEP]
refine ⟨v, vt, Walk.end_mem_support _⟩
[GOAL]
case intro.refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ Connected (induce (↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v))))) G)
[PROOFSTEP]
apply G.induce_connected_of_patches u
[GOAL]
case intro.refine_2.hu
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ u ∈ ↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v))))
[PROOFSTEP]
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion, Set.mem_setOf_eq,
  Walk.start_mem_support, exists_prop, and_true]
[GOAL]
case intro.refine_2.hu
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ i, i ∈ t
[PROOFSTEP]
exact ⟨u, ut⟩
[GOAL]
case intro.refine_2.patches
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ ∀ {v : V},
    v ∈ ↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v)))) →
      ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
[PROOFSTEP]
intros v hv
[GOAL]
case intro.refine_2.patches
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v : V
hv : v ∈ ↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v))))
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
[PROOFSTEP]
simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset, exists_prop] at hv
[GOAL]
case intro.refine_2.patches
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v : V
hv : ∃ a, a ∈ t ∧ v ∈ Walk.support (Nonempty.some (_ : Reachable G u a))
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
[PROOFSTEP]
obtain ⟨w, wt, hw⟩ := hv
[GOAL]
case intro.refine_2.patches.intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
[PROOFSTEP]
refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
[GOAL]
case intro.refine_2.patches.intro.intro.refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))} ⊆
    ↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v))))
[PROOFSTEP]
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
[GOAL]
case intro.refine_2.patches.intro.intro.refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))} ⊆
    ⋃ (x : V) (_ : x ∈ t), {a | a ∈ Walk.support (Nonempty.some (_ : Reachable G u x))}
[PROOFSTEP]
exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
[GOAL]
case intro.refine_2.patches.intro.intro.refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ ∃ hu' hv',
    Reachable (induce {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))} G) { val := u, property := hu' }
      { val := v, property := hv' }
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
[GOAL]
case intro.refine_2.patches.intro.intro.refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ ∃ hv',
    Reachable (induce {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))} G)
      { val := u, property := (_ : u ∈ {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))}) }
      { val := v, property := hv' }
[PROOFSTEP]
refine ⟨hw, Walk.connected_induce_support _ _ _⟩