α : Type u_1
β : Type u_2
γ : Type ?u.3467
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))
a₁ a₂ : α
b₁ b₂ : β
⊢ f (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))
α : Type u_1
β : Type u_2
γ : Type ?u.3467
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))
⊢ ∀ (a : α × α) (b : β × β), f (Quotient.mk (Rel.setoid α) a) (Quotient.mk (Rel.setoid β) b)
intro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.3467
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))
a₁ a₂ : α
b₁ b₂ : β
⊢ f (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))
exact hf _ _ _ _