Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case e'_1
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)

pp: case e'_2
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝

pp: case e'_4.e'_3
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝¹ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
e_3✝ : (fun x ↦ V') ≍ fun x ↦ V'
e_1✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (G.connectedComponentMk b✝).toSimpleGraph.Adj ≍ (G.connectedComponentMk a✝).toSimpleGraph.Adj

pp: case e'_5
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
⊢ G.connectedComponentMk b✝ = G.connectedComponentMk a✝

pp: case e'_6
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝

Tactic:
<;>

Goal state after:
case e'_1
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)

case e'_2
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝

case e'_4.e'_3
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝¹ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
e_3✝ : (fun x ↦ V') ≍ fun x ↦ V'
e_1✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (G.connectedComponentMk b✝).toSimpleGraph.Adj ≍ (G.connectedComponentMk a✝).toSimpleGraph.Adj

case e'_5
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
⊢ G.connectedComponentMk b✝ = G.connectedComponentMk a✝

case e'_6
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝