α : Type u_1
β : Type u_2
γ : Type ?u.83059
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this : Nonempty α
⊢ Connected G
α : Type u_1
β : Type u_2
γ : Type ?u.83059
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
⊢ Connected G
haveI := (nonempty_prod.1 h.nonempty).1
α : Type u_1
β : Type u_2
γ : Type ?u.83059
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this✝ : Nonempty α
this : Nonempty β
⊢ Connected G
α : Type u_1
β : Type u_2
γ : Type ?u.83059
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this : Nonempty α
⊢ Connected G
haveI := (nonempty_prod.1 h.nonempty).2
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.83059
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this✝ : Nonempty α
this : Nonempty β
⊢ Connected G
exact ⟨h.preconnected.ofBoxProdLeft⟩