no goals
α : Type u_1
β : Type u_2
γ : Type ?u.82447
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
⊢ Preconnected H
classical
rintro b₁ b₂
obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
exact ⟨w.ofBoxProdRight⟩
α : Type u_1
β : Type u_2
γ : Type ?u.82447
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
b₁ b₂ : β
⊢ Reachable H b₁ b₂
α : Type u_1
β : Type u_2
γ : Type ?u.82447
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
⊢ Preconnected H
rintro b₁ b₂
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.82447
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₂
α : Type u_1
β : Type u_2
γ : Type ?u.82447
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
b₁ b₂ : β
⊢ Reachable H b₁ b₂
obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.82447
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₂
exact ⟨w.ofBoxProdRight⟩