[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α × α
⊢ Rel α x y → Rel α y x
[PROOFSTEP]
aesop (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : α × α
a : Rel α x y
b : Rel α y z
⊢ Rel α x z
[PROOFSTEP]
aesop (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y z w : α
⊢ Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
[PROOFSTEP]
aesop (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
intro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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₂))
[PROOFSTEP]
exact hf _ _ _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (b, a)
[PROOFSTEP]
rw [Quotient.eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ (a, b) ≈ (b, a)
[PROOFSTEP]
apply Rel.swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α × α
⊢ Quotient.mk (Rel.setoid α) (Prod.swap p) = Quotient.mk (Rel.setoid α) p
[PROOFSTEP]
cases p
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (Prod.swap (fst✝, snd✝)) = Quotient.mk (Rel.setoid α) (fst✝, snd✝)
[PROOFSTEP]
exact eq_swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c) ↔ b = c
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c) → b = c
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ b = c → Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c)
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c)
⊢ b = c
[PROOFSTEP]
rw [Quotient.eq] at h 
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : (a, b) ≈ (a, c)
⊢ b = c
[PROOFSTEP]
cases h
[GOAL]
case mp.refl
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ b = b
[PROOFSTEP]
rfl
[GOAL]
case mp.swap
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : b = c
⊢ Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c)
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a) ↔ b = c
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a) → b = c
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ b = c → Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
⊢ b = c
[PROOFSTEP]
rw [Quotient.eq] at h 
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : (b, a) ≈ (c, a)
⊢ b = c
[PROOFSTEP]
cases h
[GOAL]
case mp.refl
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ b = b
[PROOFSTEP]
rfl
[GOAL]
case mp.swap
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : b = c
⊢ Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y z w : α
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α × α
⊢ Quotient.mk (Rel.setoid α) p = Quotient.mk (Rel.setoid α) q ↔ p = q ∨ p = Prod.swap q
[PROOFSTEP]
cases p
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
q : α × α
fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (fst✝, snd✝) = Quotient.mk (Rel.setoid α) q ↔ (fst✝, snd✝) = q ∨ (fst✝, snd✝) = Prod.swap q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (fst✝¹, snd✝¹) = Quotient.mk (Rel.setoid α) (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹) = (fst✝, snd✝) ∨ (fst✝¹, snd✝¹) = Prod.swap (fst✝, snd✝)
[PROOFSTEP]
simp only [eq_iff, Prod.mk.inj_iff, Prod.swap_prod_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
⊢ ∀ (a b : α × α), a ≈ b → uncurry (↑f) a = uncurry (↑f) b
[PROOFSTEP]
rintro _ _ ⟨⟩
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
x✝ y✝ : α
⊢ uncurry ↑f (x✝, y✝) = uncurry ↑f (x✝, y✝)
case swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
x✝ y✝ : α
⊢ uncurry ↑f (x✝, y✝) = uncurry ↑f (y✝, x✝)
[PROOFSTEP]
exacts [rfl, f.prop _ _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
⊢ ∀ (a₁ : α × α) (b₁ : β × β) (a₂ : α × α) (b₂ : β × β),
    a₁ ≈ a₂ → b₁ ≈ b₂ → (fun a b => ↑f a.fst a.snd b.fst b.snd) a₁ b₁ = (fun a b => ↑f a.fst a.snd b.fst b.snd) a₂ b₂
[PROOFSTEP]
rintro _ _ _ _ ⟨⟩ ⟨⟩
[GOAL]
case refl.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝) =
    (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝)
case refl.swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝) =
    (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (y✝, x✝)
case swap.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝) =
    (fun a b => ↑f a.fst a.snd b.fst b.snd) (y✝¹, x✝¹) (x✝, y✝)
case swap.swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝) =
    (fun a b => ↑f a.fst a.snd b.fst b.snd) (y✝¹, x✝¹) (y✝, x✝)
[PROOFSTEP]
exacts [rfl, (f.2 _ _ _ _).2, (f.2 _ _ _ _).1, (f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₁ b₂ =
      (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₂ a₁ b₁ b₂ ∧
    (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₁ b₂ =
      (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₂ b₁
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₁ b₂ =
    (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₂ a₁ b₁ b₂
case right
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₁ b₂ =
    (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₂ b₁
[PROOFSTEP]
exacts [congr_arg₂ F eq_swap rfl, congr_arg₂ F rfl eq_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
⊢ ((fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) (Prod.map f f) (Prod.map f f)
[PROOFSTEP]
intro _ _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ b✝ : α × α
h : a✝ ≈ b✝
⊢ Prod.map f f a✝ ≈ Prod.map f f b✝
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Prod.map f f (x✝, y✝) ≈ Prod.map f f (x✝, y✝)
[PROOFSTEP]
constructor
[GOAL]
case swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Prod.map f f (x✝, y✝) ≈ Prod.map f f (y✝, x✝)
[PROOFSTEP]
apply Rel.swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ map id = id
[PROOFSTEP]
ext ⟨⟨x, y⟩⟩
[GOAL]
case h.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym2 α
x y : α
⊢ map id (Quot.mk Setoid.r (x, y)) = id (Quot.mk Setoid.r (x, y))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ map (g ∘ f) = map g ∘ map f
[PROOFSTEP]
ext ⟨⟨x, y⟩⟩
[GOAL]
case h.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝ : Sym2 α
x y : α
⊢ map (g ∘ f) (Quot.mk Setoid.r (x, y)) = (map g ∘ map f) (Quot.mk Setoid.r (x, y))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x : Sym2 α
⊢ map g (map f x) = map (g ∘ f) x
[PROOFSTEP]
revert x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ ∀ (x : Sym2 α), map g (map f x) = map (g ∘ f) x
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ ∀ (x y : α), map g (map f (Quotient.mk (Rel.setoid α) (x, y))) = map (g ∘ f) (Quotient.mk (Rel.setoid α) (x, y))
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
⊢ Injective (map f)
[PROOFSTEP]
intro z z'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
⊢ map f z = map f z' → z = z'
[PROOFSTEP]
refine' Quotient.ind₂ (fun z z' => _) z z'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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'
[PROOFSTEP]
cases' z with x y
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
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'
[PROOFSTEP]
cases' z' with x' y'
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
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')
[PROOFSTEP]
repeat' rw [map_pair_eq, eq_iff]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
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')
[PROOFSTEP]
rw [map_pair_eq, eq_iff]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ Quotient.mk (Rel.setoid β) (f x, f y) = map f (Quotient.mk (Rel.setoid α) (x', y')) →
    x = x' ∧ y = y' ∨ x = y' ∧ y = x'
[PROOFSTEP]
rw [map_pair_eq, eq_iff]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
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'
[PROOFSTEP]
rw [map_pair_eq, eq_iff]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
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'
[PROOFSTEP]
rintro (h | h)
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
h : f x = f x' ∧ f y = f y'
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
[PROOFSTEP]
simp [hinj h.1, hinj h.2]
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
h : f x = f y' ∧ f y = f x'
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
[PROOFSTEP]
simp [hinj h.1, hinj h.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, c)) → a = b ∨ a = c
[PROOFSTEP]
rintro ⟨_, h⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b c w✝ : α
h : Quotient.mk (Rel.setoid α) (b, c) = Quotient.mk (Rel.setoid α) (a, w✝)
⊢ a = b ∨ a = c
[PROOFSTEP]
rw [eq_iff] at h 
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b c w✝ : α
h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a
⊢ a = b ∨ a = c
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ a = b ∨ a = c → Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, c))
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a c : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (a, c))
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, a))
[PROOFSTEP]
rw [eq_swap]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (a, b))
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h : (fun z => {x | Sym2.Mem x z}) z = (fun z => {x | Sym2.Mem x z}) z'
⊢ z = z'
[PROOFSTEP]
simp only [Set.ext_iff, Set.mem_setOf_eq] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
⊢ z = z'
[PROOFSTEP]
induction' z using Sym2.ind with x y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
⊢ Quotient.mk (Rel.setoid α) (x, y) = z'
[PROOFSTEP]
induction' z' using Sym2.ind with x' y'
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
have hx := h x
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : Sym2.Mem x (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
have hy := h y
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : Sym2.Mem x (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
hy : Sym2.Mem y (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem y (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
have hx' := h x'
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : Sym2.Mem x (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
hy : Sym2.Mem y (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem y (Quotient.mk (Rel.setoid α) (x', y'))
hx' : Sym2.Mem x' (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x' (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
have hy' := h y'
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : Sym2.Mem x (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
hy : Sym2.Mem y (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem y (Quotient.mk (Rel.setoid α) (x', y'))
hx' : Sym2.Mem x' (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x' (Quotient.mk (Rel.setoid α) (x', y'))
hy' : Sym2.Mem y' (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem y' (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
simp only [mem_iff', eq_self_iff_true, or_true_iff, iff_true_iff, true_or_iff, true_iff_iff] at hx hy hx' hy' 
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : x = x' ∨ x = y'
hy : y = x' ∨ y = y'
hx' : x' = x ∨ x' = y
hy' : y' = x ∨ y' = y
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Sym2 α
⊢ e = Quotient.mk (Rel.setoid α) ((Quotient.out e).fst, (Quotient.out e).snd)
[PROOFSTEP]
rw [Prod.mk.eta, e.out_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Sym2 α
⊢ e = Quotient.mk (Rel.setoid α) ((Quotient.out e).snd, (Quotient.out e).fst)
[PROOFSTEP]
rw [eq_swap, Prod.mk.eta, e.out_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
a b : α
⊢ (∀ (c : α), c ∈ Quotient.mk (Rel.setoid α) (a, b) → p c) ↔ p a ∧ p b
[PROOFSTEP]
refine' ⟨fun h => ⟨h _ <| mem_mk''_left _ _, h _ <| mem_mk''_right _ _⟩, fun h c hc => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
a b : α
h : p a ∧ p b
c : α
hc : c ∈ Quotient.mk (Rel.setoid α) (a, b)
⊢ p c
[PROOFSTEP]
obtain rfl | rfl := Sym2.mem_iff.1 hc
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
b c : α
h : p c ∧ p b
hc : c ∈ Quotient.mk (Rel.setoid α) (c, b)
⊢ p c
[PROOFSTEP]
exact h.1
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
a c : α
h : p a ∧ p c
hc : c ∈ Quotient.mk (Rel.setoid α) (a, c)
⊢ p c
[PROOFSTEP]
exact h.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other h) = z
[PROOFSTEP]
erw [← Classical.choose_spec h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
[PROOFSTEP]
convert mem_mk''_right a <| Mem.other h
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
⊢ z = Quotient.mk (Rel.setoid α) (a, Mem.other h)
[PROOFSTEP]
rw [other_spec h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z ↔ z = Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z → z = Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
induction' z using Sym2.ind with x' y'
[GOAL]
case mp.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
hne : x ≠ y
x' y' : α
⊢ x ∈ Quotient.mk (Rel.setoid α) (x', y') ∧ y ∈ Quotient.mk (Rel.setoid α) (x', y') →
    Quotient.mk (Rel.setoid α) (x', y') = Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
rw [mem_iff, mem_iff]
[GOAL]
case mp.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
hne : x ≠ y
x' y' : α
⊢ (x = x' ∨ x = y') ∧ (y = x' ∨ y = y') → Quotient.mk (Rel.setoid α) (x', y') = Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
aesop
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
z : Sym2 α
hne : x ≠ y
⊢ z = Quotient.mk (Rel.setoid α) (x, y) → x ∈ z ∧ y ∈ z
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
hne : x ≠ y
⊢ x ∈ Quotient.mk (Rel.setoid α) (x, y) ∧ y ∈ Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
z : Sym2 α
⊢ b ∈ map f z ↔ ∃ a, a ∈ z ∧ f a = b
[PROOFSTEP]
induction' z using Sym2.ind with x y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
x y : α
⊢ b ∈ map f (Quotient.mk (Rel.setoid α) (x, y)) ↔ ∃ a, a ∈ Quotient.mk (Rel.setoid α) (x, y) ∧ f a = b
[PROOFSTEP]
simp only [map, Quotient.map_mk, Prod.map_mk, mem_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y ↔ ∃ a, (a = x ∨ a = y) ∧ f a = b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y → ∃ a, (a = x ∨ a = y) ∧ f a = b
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case h.mp.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ ∃ a, (a = x ∨ a = y) ∧ f a = f x
[PROOFSTEP]
exact ⟨x, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ (x = x ∨ x = y) ∧ f x = f x
[PROOFSTEP]
simp
[GOAL]
case h.mp.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ ∃ a, (a = x ∨ a = y) ∧ f a = f y
[PROOFSTEP]
exact ⟨y, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ (y = x ∨ y = y) ∧ f y = f y
[PROOFSTEP]
simp
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
x y : α
⊢ (∃ a, (a = x ∨ a = y) ∧ f a = b) → b = f x ∨ b = f y
[PROOFSTEP]
rintro ⟨w, rfl | rfl, rfl⟩
[GOAL]
case h.mpr.intro.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
y w : α
⊢ f w = f w ∨ f w = f y
[PROOFSTEP]
simp
[GOAL]
case h.mpr.intro.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x w : α
⊢ f w = f x ∨ f w = f w
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
⊢ map f s = map g s
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ y ∈ map f s ↔ y ∈ map g s
[PROOFSTEP]
simp only [mem_map]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ (∃ a, a ∈ s ∧ f a = y) ↔ ∃ a, a ∈ s ∧ g a = y
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ (∃ a, a ∈ s ∧ f a = y) → ∃ a, a ∈ s ∧ g a = y
[PROOFSTEP]
rintro ⟨w, hw, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ ∃ a, a ∈ s ∧ g a = f w
[PROOFSTEP]
exact ⟨w, hw, by simp [hw, h]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ g w = f w
[PROOFSTEP]
simp [hw, h]
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ (∃ a, a ∈ s ∧ g a = y) → ∃ a, a ∈ s ∧ f a = y
[PROOFSTEP]
rintro ⟨w, hw, rfl⟩
[GOAL]
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ ∃ a, a ∈ s ∧ f a = g w
[PROOFSTEP]
exact ⟨w, hw, by simp [hw, h]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ f w = g w
[PROOFSTEP]
simp [hw, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
h : diag x = diag y
⊢ x = y
[PROOFSTEP]
cases Quotient.exact h
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
h : diag x = diag x
⊢ x = x
[PROOFSTEP]
rfl
[GOAL]
case swap
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
h : diag x = diag x
⊢ x = x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
⊢ IsDiag z → z ∈ Set.range diag
[PROOFSTEP]
induction' z using Sym2.ind with x y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
⊢ IsDiag (Quotient.mk (Rel.setoid α) (x, y)) → Quotient.mk (Rel.setoid α) (x, y) ∈ Set.range diag
[PROOFSTEP]
rintro (rfl : x = y)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
⊢ Quotient.mk (Rel.setoid α) (x, x) ∈ Set.range diag
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝ : DecidableEq α
⊢ DecidablePred IsDiag
[PROOFSTEP]
refine' fun z => Quotient.recOnSubsingleton z fun a => _
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝ : DecidableEq α
z : Sym2 α
a : α × α
⊢ Decidable (IsDiag (Quotient.mk (Rel.setoid α) a))
[PROOFSTEP]
erw [isDiag_iff_proj_eq]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝ : DecidableEq α
z : Sym2 α
a : α × α
⊢ Decidable (a.fst = a.snd)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
hd : ¬IsDiag z
h : a ∈ z
⊢ Mem.other h ≠ a
[PROOFSTEP]
contrapose! hd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
⊢ IsDiag z
[PROOFSTEP]
have h' := Sym2.other_spec h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, Mem.other h) = z
⊢ IsDiag z
[PROOFSTEP]
rw [hd] at h' 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, a) = z
⊢ IsDiag z
[PROOFSTEP]
rw [← h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, a) = z
⊢ IsDiag (Quotient.mk (Rel.setoid α) (a, a))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ fromRel (_ : ∀ (x y : α), ⊥ x y → ⊥ x y) = ∅
[PROOFSTEP]
apply Set.eq_empty_of_forall_not_mem fun e => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ ∀ (e : Sym2 α), ¬e ∈ fromRel (_ : ∀ (x y : α), ⊥ x y → ⊥ x y)
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ ∀ (x y : α), ¬Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel (_ : ∀ (x y : α), ⊥ x y → ⊥ x y)
[PROOFSTEP]
simp [-Set.bot_eq_empty, Prop.bot_eq_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y) = Set.univ
[PROOFSTEP]
apply Set.eq_univ_of_forall fun e => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ ∀ (e : Sym2 α), e ∈ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y)
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ ∀ (x y : α), Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y)
[PROOFSTEP]
simp [-Set.top_eq_univ, Prop.top_eq_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
sym : Symmetric r
⊢ Irreflexive r → ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬IsDiag z
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬IsDiag z
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ (x y : α), Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel sym → ¬IsDiag (Quotient.mk (Rel.setoid α) (x, y))
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : Set (Sym2 α)
x y : α
⊢ ToRel s x y → ToRel s y x
[PROOFSTEP]
simp [eq_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
⊢ [a₁, b₁] ~ [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
[PROOFSTEP]
simp [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.cons_eq_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ [a₁, b₁] ~ [a₂, b₂]
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]

[PROOFSTEP]
first
| done
| apply List.Perm.swap'; rfl
[GOAL]

[PROOFSTEP]
done
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [a₁, b₁] ~ [a₂, b₂]
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
[PROOFSTEP]
first
| done
| apply List.Perm.swap'; rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
[PROOFSTEP]
done
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
[PROOFSTEP]
apply List.Perm.swap'
[GOAL]
case p
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [] ~ []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ((fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1)
    (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
    fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) }
[PROOFSTEP]
rintro _ _ ⟨_⟩
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ y✝ : α
⊢ (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (x✝, y✝) ≈
    (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (x✝, y✝)
[PROOFSTEP]
constructor
[GOAL]
case refl.a
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ y✝ : α
⊢ [(x✝, y✝).snd] ~ [(x✝, y✝).snd]
[PROOFSTEP]
apply List.Perm.refl
[GOAL]
case swap
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ y✝ : α
⊢ (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (x✝, y✝) ≈
    (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (y✝, x✝)
[PROOFSTEP]
apply List.Perm.swap'
[GOAL]
case swap.p
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ y✝ : α
⊢ [] ~ []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ((fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) Sym2.fromVector Sym2.fromVector
[PROOFSTEP]
rintro ⟨x, hx⟩ ⟨y, hy⟩ h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
x : List α
hx : List.length x = 2
y : List α
hy : List.length y = 2
h : { val := x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := x, property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.mk.nil
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
hx : List.length [] = 2
h : { val := [], property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := [], property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
simp at hx 
[GOAL]
case mk.mk.cons
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝ : α
x : List α
hx : List.length (head✝ :: x) = 2
h : { val := head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := head✝ :: x, property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.mk.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝ : α
hx : List.length [head✝] = 2
h : { val := [head✝], property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := [head✝], property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
simp at hx 
[GOAL]
case mk.mk.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝¹ head✝ : α
x : List α
hx : List.length (head✝¹ :: head✝ :: x) = 2
h : { val := head✝¹ :: head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := head✝¹ :: head✝ :: x, property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.mk.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈ Sym2.fromVector { val := y, property := hy }
case mk.mk.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
h : { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈
    Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
swap
[GOAL]
case mk.mk.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
h : { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈
    Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
exfalso
[GOAL]
case mk.mk.cons.cons.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
h : { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ False
[PROOFSTEP]
simp at hx 
[GOAL]
case mk.mk.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
cases' y with _ y
[GOAL]
case mk.mk.cons.cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
hy : List.length [] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := [], property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈ Sym2.fromVector { val := [], property := hy }
[PROOFSTEP]
simp at hy 
[GOAL]
case mk.mk.cons.cons.nil.cons
α : Type u_1
β : Type u_2
γ : Type u_3
head✝² head✝¹ : α
hx : List.length [head✝², head✝¹] = 2
head✝ : α
y : List α
hy : List.length (head✝ :: y) = 2
h : { val := [head✝², head✝¹], property := hx } ≈ { val := head✝ :: y, property := hy }
⊢ Sym2.fromVector { val := [head✝², head✝¹], property := hx } ≈ Sym2.fromVector { val := head✝ :: y, property := hy }
[PROOFSTEP]
cases' y with _ y
[GOAL]
case mk.mk.cons.cons.nil.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
head✝² head✝¹ : α
hx : List.length [head✝², head✝¹] = 2
head✝ : α
hy : List.length [head✝] = 2
h : { val := [head✝², head✝¹], property := hx } ≈ { val := [head✝], property := hy }
⊢ Sym2.fromVector { val := [head✝², head✝¹], property := hx } ≈ Sym2.fromVector { val := [head✝], property := hy }
[PROOFSTEP]
simp at hy 
[GOAL]
case mk.mk.cons.cons.nil.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
head✝³ head✝² : α
hx : List.length [head✝³, head✝²] = 2
head✝¹ head✝ : α
y : List α
hy : List.length (head✝¹ :: head✝ :: y) = 2
h : { val := [head✝³, head✝²], property := hx } ≈ { val := head✝¹ :: head✝ :: y, property := hy }
⊢ Sym2.fromVector { val := [head✝³, head✝²], property := hx } ≈
    Sym2.fromVector { val := head✝¹ :: head✝ :: y, property := hy }
[PROOFSTEP]
cases' y with _ y
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
head✝³ head✝² : α
hx : List.length [head✝³, head✝²] = 2
head✝¹ head✝ : α
hy : List.length [head✝¹, head✝] = 2
h : { val := [head✝³, head✝²], property := hx } ≈ { val := [head✝¹, head✝], property := hy }
⊢ Sym2.fromVector { val := [head✝³, head✝²], property := hx } ≈
    Sym2.fromVector { val := [head✝¹, head✝], property := hy }
case mk.mk.cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
head✝⁴ head✝³ : α
hx : List.length [head✝⁴, head✝³] = 2
head✝² head✝¹ head✝ : α
y : List α
hy : List.length (head✝² :: head✝¹ :: head✝ :: y) = 2
h : { val := [head✝⁴, head✝³], property := hx } ≈ { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
⊢ Sym2.fromVector { val := [head✝⁴, head✝³], property := hx } ≈
    Sym2.fromVector { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
[PROOFSTEP]
swap
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
head✝⁴ head✝³ : α
hx : List.length [head✝⁴, head✝³] = 2
head✝² head✝¹ head✝ : α
y : List α
hy : List.length (head✝² :: head✝¹ :: head✝ :: y) = 2
h : { val := [head✝⁴, head✝³], property := hx } ≈ { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
⊢ Sym2.fromVector { val := [head✝⁴, head✝³], property := hx } ≈
    Sym2.fromVector { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
[PROOFSTEP]
exfalso
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
head✝⁴ head✝³ : α
hx : List.length [head✝⁴, head✝³] = 2
head✝² head✝¹ head✝ : α
y : List α
hy : List.length (head✝² :: head✝¹ :: head✝ :: y) = 2
h : { val := [head✝⁴, head✝³], property := hx } ≈ { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
⊢ False
[PROOFSTEP]
simp at hy 
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
head✝³ head✝² : α
hx : List.length [head✝³, head✝²] = 2
head✝¹ head✝ : α
hy : List.length [head✝¹, head✝] = 2
h : { val := [head✝³, head✝²], property := hx } ≈ { val := [head✝¹, head✝], property := hy }
⊢ Sym2.fromVector { val := [head✝³, head✝²], property := hx } ≈
    Sym2.fromVector { val := [head✝¹, head✝], property := hy }
[PROOFSTEP]
rcases perm_card_two_iff.mp h with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.nil.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
head✝¹ head✝ : α
hx hy : List.length [head✝¹, head✝] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := [head✝¹, head✝], property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈
    Sym2.fromVector { val := [head✝¹, head✝], property := hy }
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.nil.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
hy : List.length [head✝, head✝¹] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := [head✝, head✝¹], property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈
    Sym2.fromVector { val := [head✝, head✝¹], property := hy }
[PROOFSTEP]
apply Sym2.Rel.swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ LeftInverse
    (Quotient.map Sym2.fromVector
      (_ :
        ∀ ⦃a b : Vector α 2⦄,
          (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b)))
    (Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b))
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (x y : α),
    Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.map
          (fun x =>
            { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
          (_ :
            ∀ ⦃a b : α × α⦄,
              a ≈ b →
                (fun x =>
                      { val := [x.fst, x.snd],
                        property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                    a ≈
                  (fun x =>
                      { val := [x.fst, x.snd],
                        property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                    b)
          (Quotient.mk (Rel.setoid α) (x, y))) =
      Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
aesop (add norm unfold [Sym2.fromVector])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        x) =
    x
[PROOFSTEP]
refine' Quotient.recOnSubsingleton x fun x => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
x : Vector α 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) x)) =
    Quotient.mk (Vector.Perm.isSetoid α 2) x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
x : List α
hx : List.length x = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := x, property := hx }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
hx : List.length [] = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := [], property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := [], property := hx }
[PROOFSTEP]
simp at hx 
[GOAL]
case mk.cons
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝ : α
x : List α
hx : List.length (head✝ :: x) = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝ :: x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝ :: x, property := hx }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
head✝ : α
hx : List.length [head✝] = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝], property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝], property := hx }
[PROOFSTEP]
simp at hx 
[GOAL]
case mk.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝¹ head✝ : α
x : List α
hx : List.length (head✝¹ :: head✝ :: x) = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝¹ :: head✝ :: x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝¹ :: head✝ :: x, property := hx }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝¹, head✝], property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝¹, head✝], property := hx }
case mk.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝² :: head✝¹ :: head✝ :: x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝² :: head✝¹ :: head✝ :: x, property := hx }
[PROOFSTEP]
swap
[GOAL]
case mk.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝² :: head✝¹ :: head✝ :: x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝² :: head✝¹ :: head✝ :: x, property := hx }
[PROOFSTEP]
exfalso
[GOAL]
case mk.cons.cons.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
⊢ False
[PROOFSTEP]
simp at hx 
[GOAL]
case mk.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝¹, head✝], property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝¹, head✝], property := hx }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
x y : α × α
⊢ relBool x y = true ↔ Rel α x y
[PROOFSTEP]
cases' x with x₁ x₂
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
y : α × α
x₁ x₂ : α
⊢ relBool (x₁, x₂) y = true ↔ Rel α (x₁, x₂) y
[PROOFSTEP]
cases' y with y₁ y₂
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
x₁ x₂ y₁ y₂ : α
⊢ relBool (x₁, x₂) (y₁, y₂) = true ↔ Rel α (x₁, x₂) (y₁, y₂)
[PROOFSTEP]
aesop (rule_sets [Sym2]) (add norm unfold [relBool])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
⊢ ∀ (a₁ a₂ b₁ b₂ : α),
    (fun x₁ x₂ y₁ y₂ => relBool (x₁, x₂) (y₁, y₂)) a₁ a₂ b₁ b₂ =
        (fun x₁ x₂ y₁ y₂ => relBool (x₁, x₂) (y₁, y₂)) a₂ a₁ b₁ b₂ ∧
      (fun x₁ x₂ y₁ y₂ => relBool (x₁, x₂) (y₁, y₂)) a₁ a₂ b₁ b₂ =
        (fun x₁ x₂ y₁ y₂ => relBool (x₁, x₂) (y₁, y₂)) a₁ a₂ b₂ b₁
[PROOFSTEP]
aesop (add norm unfold [relBool])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : Sym2 α
⊢ ∀ (a₁ a₂ b₁ b₂ : α),
    eqBool (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid α) (b₁, b₂)) = true ↔
      Quotient.mk (Rel.setoid α) (a₁, a₂) = Quotient.mk (Rel.setoid α) (b₁, b₂)
[PROOFSTEP]
aesop (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ ∀ (a_1 b : α × α) (p : a_1 ≈ b),
    Eq.ndrec (motive := fun x => a ∈ x → α) (fun x => Sym2.pairOther a a_1)
        (_ : Quotient.mk (Rel.setoid α) a_1 = Quotient.mk (Rel.setoid α) b) =
      fun x => Sym2.pairOther a b
[PROOFSTEP]
clear h z
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ∀ (a_1 b : α × α) (p : a_1 ≈ b),
    Eq.ndrec (motive := fun x => a ∈ x → α) (fun x => Sym2.pairOther a a_1)
        (_ : Quotient.mk (Rel.setoid α) a_1 = Quotient.mk (Rel.setoid α) b) =
      fun x => Sym2.pairOther a b
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) y) =
    fun x => Sym2.pairOther a y
[PROOFSTEP]
ext hy
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) y) hy =
    Sym2.pairOther a y
[PROOFSTEP]
convert_to Sym2.pairOther a x = _
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) y) hy =
    Sym2.pairOther a x
[PROOFSTEP]
have :
  ∀ {c e h},
    @Eq.ndrec (Quotient (Rel.setoid α)) (Quotient.mk (Rel.setoid α) x) (fun x => a ∈ x → α)
        (fun _ => Sym2.pairOther a x) c e h =
      Sym2.pairOther a x :=
  by intro _ e _; subst e; rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
⊢ ∀ {c : Quotient (Rel.setoid α)} {e : Quotient.mk (Rel.setoid α) x = c} {h : a ∈ c},
    Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x) e h = Sym2.pairOther a x
[PROOFSTEP]
intro _ e _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
c✝ : Quotient (Rel.setoid α)
e : Quotient.mk (Rel.setoid α) x = c✝
h✝ : a ∈ c✝
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x) e h✝ = Sym2.pairOther a x
[PROOFSTEP]
subst e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
h✝ : a ∈ Quotient.mk (Rel.setoid α) x
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) x) h✝ =
    Sym2.pairOther a x
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
this :
  ∀ {c : Quotient (Rel.setoid α)} {e : Quotient.mk (Rel.setoid α) x = c} {h : a ∈ c},
    Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x) e h = Sym2.pairOther a x
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) y) hy =
    Sym2.pairOther a x
[PROOFSTEP]
apply this
[GOAL]
case h.convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
⊢ Sym2.pairOther a x = Sym2.pairOther a y
[PROOFSTEP]
rw [mem_iff] at hy 
[GOAL]
case h.convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a = y.fst ∨ a = y.snd
⊢ Sym2.pairOther a x = Sym2.pairOther a y
[PROOFSTEP]
have : relBool x y := (relBool_spec x y).mpr h
[GOAL]
case h.convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a = y.fst ∨ a = y.snd
this : relBool x y = true
⊢ Sym2.pairOther a x = Sym2.pairOther a y
[PROOFSTEP]
aesop (add norm unfold [pairOther, relBool])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = z
[PROOFSTEP]
induction z using Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
have h' := mem_iff.mp h
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
h' : a = x✝ ∨ a = y✝
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
aesop (add norm unfold [Quotient.rec, Quot.rec]) (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h = Mem.other' h
[PROOFSTEP]
rw [← congr_right, other_spec' h, other_spec]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other' h ∈ z
[PROOFSTEP]
rw [← other_eq_other']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
[PROOFSTEP]
exact other_mem h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb = a
[PROOFSTEP]
induction z using Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a x✝ y✝ : α
ha : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
hb : Mem.other' ha ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ Mem.other' hb = a
[PROOFSTEP]
aesop (rule_sets [Sym2]) (add norm unfold [Quotient.rec, Quot.rec])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a
[PROOFSTEP]
classical
rw [other_eq_other'] at hb ⊢
convert other_invol' ha hb using 2
apply other_eq_other'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a
[PROOFSTEP]
rw [other_eq_other'] at hb ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb✝ = a
[PROOFSTEP]
convert other_invol' ha hb using 2
[GOAL]
case h.e'_2.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other ha = Mem.other' ha
[PROOFSTEP]
apply other_eq_other'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
⊢ filter IsDiag (image Quotient.mk'' (s ×ˢ s)) = image Quotient.mk'' (Finset.diag s)
[PROOFSTEP]
ext z
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
z : Sym2 α
⊢ z ∈ filter IsDiag (image Quotient.mk'' (s ×ˢ s)) ↔ z ∈ image Quotient.mk'' (Finset.diag s)
[PROOFSTEP]
induction' z using Sym2.inductionOn
[GOAL]
case a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ filter IsDiag (image Quotient.mk'' (s ×ˢ s)) ↔
    Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ image Quotient.mk'' (Finset.diag s)
[PROOFSTEP]
simp only [mem_image, mem_diag, exists_prop, mem_filter, Prod.exists, mem_product]
[GOAL]
case a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) ↔
    ∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
constructor
[GOAL]
case a.hf.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    ∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
rintro ⟨⟨a, b, ⟨ha, hb⟩, (h : Quotient.mk _ _ = _)⟩, hab⟩
[GOAL]
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
hab : IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
rw [← h, Sym2.mk''_isDiag_iff] at hab 
[GOAL]
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
hab : a = b
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
exact ⟨a, b, ⟨ha, hab⟩, h⟩
[GOAL]
case a.hf.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
rintro ⟨a, b, ⟨ha, rfl⟩, h⟩
[GOAL]
case a.hf.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a : α
ha : a ∈ s
h : Quotient.mk'' (a, a) = Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
rw [← h]
[GOAL]
case a.hf.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a : α
ha : a ∈ s
h : Quotient.mk'' (a, a) = Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ (∃ a_1 b, (a_1 ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a_1, b) = Quotient.mk'' (a, a)) ∧ IsDiag (Quotient.mk'' (a, a))
[PROOFSTEP]
exact ⟨⟨a, a, ⟨ha, ha⟩, rfl⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) = image Quotient.mk'' (offDiag s)
[PROOFSTEP]
ext z
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
z : Sym2 α
⊢ z ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) ↔ z ∈ image Quotient.mk'' (offDiag s)
[PROOFSTEP]
induction z using Sym2.inductionOn
[GOAL]
case a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) ↔
    Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ image Quotient.mk'' (offDiag s)
[PROOFSTEP]
simp only [mem_image, mem_offDiag, mem_filter, Prod.exists, mem_product]
[GOAL]
case a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) ↔
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
constructor
[GOAL]
case a.hf.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
rintro ⟨⟨a, b, ⟨ha, hb⟩, (h : Quotient.mk _ _ = _)⟩, hab⟩
[GOAL]
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
hab : ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
rw [← h, Sym2.mk''_isDiag_iff] at hab 
[GOAL]
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
hab : ¬a = b
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
exact ⟨a, b, ⟨ha, hb, hab⟩, h⟩
[GOAL]
case a.hf.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
rintro ⟨a, b, ⟨ha, hb, hab⟩, (h : Quotient.mk _ _ = _)⟩
[GOAL]
case a.hf.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
rw [Ne.def, ← Sym2.mk''_isDiag_iff, h] at hab 
[GOAL]
case a.hf.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
exact ⟨⟨a, b, ⟨ha, hb⟩, h⟩, hab⟩
