case verts
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
⊢ (Subgraph.map f (H ⊔ H')).verts = (Subgraph.map f H ⊔ Subgraph.map f H').verts

case Adj
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
⊢ (Subgraph.map f (H ⊔ H')).Adj = (Subgraph.map f H ⊔ Subgraph.map f H').Adj
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
⊢ Subgraph.map f (H ⊔ H') = Subgraph.map f H ⊔ Subgraph.map f H'
ext1
no goals
case verts
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
⊢ (Subgraph.map f (H ⊔ H')).verts = (Subgraph.map f H ⊔ Subgraph.map f H').verts
simp only [Set.image_union, map_verts, verts_sup]
case Adj.h.h.a
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ Adj (Subgraph.map f (H ⊔ H')) x✝¹ x✝ ↔ Adj (Subgraph.map f H ⊔ Subgraph.map f H') x✝¹ x✝
case Adj
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
⊢ (Subgraph.map f (H ⊔ H')).Adj = (Subgraph.map f H ⊔ Subgraph.map f H').Adj
ext
case Adj.h.h.a
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ (∃ a b, (Adj H a b ∨ Adj H' a b) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ↔
    (∃ a b, Adj H a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ∨ ∃ a b, Adj H' a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
case Adj.h.h.a
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ Adj (Subgraph.map f (H ⊔ H')) x✝¹ x✝ ↔ Adj (Subgraph.map f H ⊔ Subgraph.map f H') x✝¹ x✝
simp only [Relation.Map, map_Adj, sup_adj]
case Adj.h.h.a.mp
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ (∃ a b, (Adj H a b ∨ Adj H' a b) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) →
    (∃ a b, Adj H a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ∨ ∃ a b, Adj H' a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝

case Adj.h.h.a.mpr
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ ((∃ a b, Adj H a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ∨ ∃ a b, Adj H' a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) →
    ∃ a b, (Adj H a b ∨ Adj H' a b) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
case Adj.h.h.a
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ (∃ a b, (Adj H a b ∨ Adj H' a b) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ↔
    (∃ a b, Adj H a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ∨ ∃ a b, Adj H' a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
constructor
case Adj.h.h.a.mp.intro.intro.intro.inl.intro
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H a b
⊢ (∃ a_1 b_1, Adj H a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b) ∨ ∃ a_1 b_1, Adj H' a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b

case Adj.h.h.a.mp.intro.intro.intro.inr.intro
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H' a b
⊢ (∃ a_1 b_1, Adj H a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b) ∨ ∃ a_1 b_1, Adj H' a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
case Adj.h.h.a.mp
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ (∃ a b, (Adj H a b ∨ Adj H' a b) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) →
    (∃ a b, Adj H a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ∨ ∃ a b, Adj H' a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
rintro ⟨a, b, h | h, rfl, rfl⟩
no goals
case Adj.h.h.a.mp.intro.intro.intro.inl.intro
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H a b
⊢ (∃ a_1 b_1, Adj H a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b) ∨ ∃ a_1 b_1, Adj H' a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
exact Or.inl ⟨_, _, h, rfl, rfl⟩
no goals
case Adj.h.h.a.mp.intro.intro.intro.inr.intro
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H' a b
⊢ (∃ a_1 b_1, Adj H a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b) ∨ ∃ a_1 b_1, Adj H' a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
exact Or.inr ⟨_, _, h, rfl, rfl⟩
case Adj.h.h.a.mpr.inl.intro.intro.intro.intro
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H a b
⊢ ∃ a_1 b_1, (Adj H a_1 b_1 ∨ Adj H' a_1 b_1) ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b

case Adj.h.h.a.mpr.inr.intro.intro.intro.intro
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H' a b
⊢ ∃ a_1 b_1, (Adj H a_1 b_1 ∨ Adj H' a_1 b_1) ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
case Adj.h.h.a.mpr
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ ((∃ a b, Adj H a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ∨ ∃ a b, Adj H' a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) →
    ∃ a b, (Adj H a b ∨ Adj H' a b) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
rintro (⟨a, b, h, rfl, rfl⟩ | ⟨a, b, h, rfl, rfl⟩)
no goals
case Adj.h.h.a.mpr.inl.intro.intro.intro.intro
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H a b
⊢ ∃ a_1 b_1, (Adj H a_1 b_1 ∨ Adj H' a_1 b_1) ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
exact ⟨_, _, Or.inl h, rfl, rfl⟩
no goals
case Adj.h.h.a.mpr.inr.intro.intro.intro.intro
ι : Sort ?u.147638
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H' a b
⊢ ∃ a_1 b_1, (Adj H a_1 b_1 ∨ Adj H' a_1 b_1) ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
exact ⟨_, _, Or.inr h, rfl, rfl⟩