α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z' : Sym2 α
⊢ map f z = map f z' → z = z'
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
⊢ Injective (map f)
intro z z'
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z✝ z'✝ : Sym2 α
z z' : α × α
⊢ map f (Quotient.mk (Rel.setoid α) z) = map f (Quotient.mk (Rel.setoid α) z') →
    Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) z'
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z' : Sym2 α
⊢ map f z = map f z' → z = z'
refine' Quotient.ind₂ (fun z z' => _) z z'
case mk
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z'✝ : Sym2 α
z' : α × α
x y : α
⊢ map f (Quotient.mk (Rel.setoid α) (x, y)) = map f (Quotient.mk (Rel.setoid α) z') →
    Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) z'
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z✝ z'✝ : Sym2 α
z z' : α × α
⊢ map f (Quotient.mk (Rel.setoid α) z) = map f (Quotient.mk (Rel.setoid α) z') →
    Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) z'
cases' z with x y
case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ map f (Quotient.mk (Rel.setoid α) (x, y)) = map f (Quotient.mk (Rel.setoid α) (x', y')) →
    Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
case mk
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z'✝ : Sym2 α
z' : α × α
x y : α
⊢ map f (Quotient.mk (Rel.setoid α) (x, y)) = map f (Quotient.mk (Rel.setoid α) z') →
    Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) z'
cases' z' with x' y'
case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ f x = f x' ∧ f y = f y' ∨ f x = f y' ∧ f y = f x' → x = x' ∧ y = y' ∨ x = y' ∧ y = x'
case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ map f (Quotient.mk (Rel.setoid α) (x, y)) = map f (Quotient.mk (Rel.setoid α) (x', y')) →
    Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
repeat' rw [map_pair_eq, eq_iff]
no goals
case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ f x = f x' ∧ f y = f y' ∨ f x = f y' ∧ f y = f x' → x = x' ∧ y = y' ∨ x = y' ∧ y = x'
rintro (h | h) <;> simp [hinj h.1, hinj h.2]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ f x = f x' ∧ f y = f y' ∨ f x = f y' ∧ f y = f x' → x = x' ∧ y = y' ∨ x = y' ∧ y = x'
case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.17037
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ f x = f x' ∧ f y = f y' ∨ f x = f y' ∧ f y = f x' → x = x' ∧ y = y' ∨ x = y' ∧ y = x'
rw [map_pair_eq, eq_iff]