[GOAL]
α : Type u_1
β : Type u_2
s : Set (Setoid α)
⊢ Rel (sInf s) = sInf (Rel '' s)
[PROOFSTEP]
ext
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ Rel (sInf s) x✝¹ x✝ ↔ sInf (Rel '' s) x✝¹ x✝
[PROOFSTEP]
simp only [sInf_image, iInf_apply, iInf_Prop_eq]
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ Rel (sInf s) x✝¹ x✝ ↔ ∀ (i : Setoid α), i ∈ s → Rel i x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
⊢ s = ⊤ ↔ ∀ (x y : α), Rel s x y
[PROOFSTEP]
rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → Rel s x y) ↔ ∀ (x y : α), Rel s x y
[PROOFSTEP]
simp only [Pi.top_apply, Prop.top_eq_true, forall_true_left]
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ r ⊔ s = EqvGen.Setoid fun x y => Rel r x y ∨ Rel s x y
[PROOFSTEP]
rw [eqvGen_eq]
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, Rel r x y ∨ Rel s x y → Rel s_1 x y}
[PROOFSTEP]
apply congr_arg sInf
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ {x | r ≤ x ∧ s ≤ x} = {s_1 | ∀ ⦃x y : α⦄, Rel r x y ∨ Rel s x y → Rel s_1 x y}
[PROOFSTEP]
simp only [le_def, or_imp, ← forall_and]
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ r ⊔ s = EqvGen.Setoid (Rel r ⊔ Rel s)
[PROOFSTEP]
rw [sup_eq_eqvGen]
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ (EqvGen.Setoid fun x y => Rel r x y ∨ Rel s x y) = EqvGen.Setoid (Rel r ⊔ Rel s)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
S : Set (Setoid α)
⊢ sSup S = EqvGen.Setoid fun x y => ∃ r, r ∈ S ∧ Rel r x y
[PROOFSTEP]
rw [eqvGen_eq]
[GOAL]
α : Type u_1
β : Type u_2
S : Set (Setoid α)
⊢ sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r, r ∈ S ∧ Rel r x y) → Rel s x y}
[PROOFSTEP]
apply congr_arg sInf
[GOAL]
α : Type u_1
β : Type u_2
S : Set (Setoid α)
⊢ upperBounds S = {s | ∀ ⦃x y : α⦄, (∃ r, r ∈ S ∧ Rel r x y) → Rel s x y}
[PROOFSTEP]
simp only [upperBounds, le_def, and_imp, exists_imp]
[GOAL]
α : Type u_1
β : Type u_2
S : Set (Setoid α)
⊢ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, Rel a x_1 y → Rel x x_1 y} =
    {s | ∀ ⦃x y : α⦄ (x_1 : Setoid α), x_1 ∈ S → Rel x_1 x y → Rel s x y}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
S : Set (Setoid α)
x✝ : Setoid α
⊢ x✝ ∈ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, Rel a x_1 y → Rel x x_1 y} ↔
    x✝ ∈ {s | ∀ ⦃x y : α⦄ (x_1 : Setoid α), x_1 ∈ S → Rel x_1 x y → Rel s x y}
[PROOFSTEP]
exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set (Setoid α)
⊢ sSup s = EqvGen.Setoid (sSup (Rel '' s))
[PROOFSTEP]
rw [sSup_eq_eqvGen, sSup_image]
[GOAL]
α : Type u_1
β : Type u_2
s : Set (Setoid α)
⊢ (EqvGen.Setoid fun x y => ∃ r, r ∈ s ∧ Rel r x y) = EqvGen.Setoid (⨆ (a : Setoid α) (_ : a ∈ s), Rel a)
[PROOFSTEP]
congr with (x y)
[GOAL]
case e_r.h.h.a
α : Type u_1
β : Type u_2
s : Set (Setoid α)
x y : α
⊢ (∃ r, r ∈ s ∧ Rel r x y) ↔ iSup (fun a => ⨆ (_ : a ∈ s), Rel a) x y
[PROOFSTEP]
simp only [iSup_apply, iSup_Prop_eq, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
⊢ EqvGen.Setoid Setoid.r ≤ r
[PROOFSTEP]
rw [eqvGen_eq]
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
⊢ sInf {s | ∀ ⦃x y : α⦄, Setoid.r x y → Rel s x y} ≤ r
[PROOFSTEP]
exact sInf_le fun _ _ => id
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → Rel s x y
⊢ EqvGen.Setoid r ≤ s
[PROOFSTEP]
rw [eqvGen_eq]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → Rel s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → Rel s x y} ≤ s
[PROOFSTEP]
exact sInf_le h
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : Quotient r → β
x y : α
h : Rel r x y
⊢ Rel (ker (f ∘ Quotient.mk'')) x y
[PROOFSTEP]
simp [ker_def, Quotient.sound' h]
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
⊢ Quotient.lift f H = g
[PROOFSTEP]
ext ⟨x⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ Quotient.lift f H (Quot.mk Setoid.r x) = g (Quot.mk Setoid.r x)
[PROOFSTEP]
erw [Quotient.lift_mk f H, Hg]
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ (g ∘ Quotient.mk'') x = g (Quot.mk Setoid.r x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
x y : Quotient (ker f)
h :
  Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      x =
    Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      y
⊢ Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) x = Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) y
[PROOFSTEP]
rcases x with ⟨⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
x y : Quotient (ker f)
a✝ : α
h :
  Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      (Quot.mk Setoid.r a✝) =
    Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      y
⊢ Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) (Quot.mk Setoid.r a✝) =
    Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) y
[PROOFSTEP]
rcases y with ⟨⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
x y : Quotient (ker f)
a✝¹ a✝ : α
h :
  Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      (Quot.mk Setoid.r a✝¹) =
    Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      (Quot.mk Setoid.r a✝)
⊢ Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) (Quot.mk Setoid.r a✝¹) =
    Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) (Quot.mk Setoid.r a✝)
[PROOFSTEP]
injections
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f✝ : α → β
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
x✝² y✝ z✝ : β
x✝¹ : ∃ a b, f a = x✝² ∧ f b = y✝ ∧ Rel r a b
x✝ : ∃ a b, f a = y✝ ∧ f b = z✝ ∧ Rel r a b
x y : α
hx : f x = x✝²
hy : f y = y✝
h₁ : Rel r x y
y' z : α
hy' : f y' = y✝
hz : f z = z✝
h₂ : Rel r y' z
⊢ Rel (ker f) y y'
[PROOFSTEP]
rwa [← hy'] at hy 
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ map r f = mapOfSurjective r f h hf
[PROOFSTEP]
rw [← eqvGen_of_setoid (mapOfSurjective r f h hf)]
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ map r f = EqvGen.Setoid Setoid.r
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f✝ f : α → β
r : Setoid β
x y : α
⊢ Setoid.r x y ↔ Quotient.mk r (f x) = Quotient.mk r (f y)
[PROOFSTEP]
rw [Quotient.eq]
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f✝ f : α → β
r : Setoid β
x y : α
⊢ Setoid.r x y ↔ f x ≈ f y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient (ker (Quot.mapRight h))
y : Quot fun a₁ a₂ => Rel r a₁ a₂
w : α
⊢ (fun x =>
        Quotient.liftOn' x (fun w => Quotient.mk'' (Quotient.mk'' w))
          (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk'' (Quotient.mk'' x) = Quotient.mk'' (Quotient.mk'' y)))
      ((fun x =>
          Quotient.liftOn' x
            (fun w =>
              Quotient.liftOn' w Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y))
            (_ :
              ∀ (x y : Quot fun a₁ a₂ => Rel r a₁ a₂),
                Setoid.r x y →
                  Quotient.liftOn' x Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y) =
                    Quotient.liftOn' y Quotient.mk''
                      (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y)))
        (Quotient.mk'' (Quotient.mk'' w))) =
    Quotient.mk'' (Quotient.mk'' w)
[PROOFSTEP]
show ⟦_⟧ = _
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient (ker (Quot.mapRight h))
y : Quot fun a₁ a₂ => Rel r a₁ a₂
w : α
⊢ Quotient.mk (ker (Quot.mapRight h)) (Quotient.mk'' w) = Quotient.mk'' (Quotient.mk'' w)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient s
y : α
⊢ (fun x =>
        Quotient.liftOn' x
          (fun w =>
            Quotient.liftOn' w Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y))
          (_ :
            ∀ (x y : Quot fun a₁ a₂ => Rel r a₁ a₂),
              Setoid.r x y →
                Quotient.liftOn' x Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y) =
                  Quotient.liftOn' y Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y)))
      ((fun x =>
          Quotient.liftOn' x (fun w => Quotient.mk'' (Quotient.mk'' w))
            (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk'' (Quotient.mk'' x) = Quotient.mk'' (Quotient.mk'' y)))
        (Quotient.mk'' y)) =
    Quotient.mk'' y
[PROOFSTEP]
show ⟦_⟧ = _
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient s
y : α
⊢ Quotient.mk s y = Quotient.mk'' y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : Rel r x y
⊢ Rel (comap Quotient.mk' s) x y
[PROOFSTEP]
rw [comap_rel, eq_rel.2 h]
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : { s // r ≤ s }
⊢ (fun s => { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
      ((fun s =>
          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
        s) =
    s
[PROOFSTEP]
ext
[GOAL]
case a.H
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : { s // r ≤ s }
a✝ b✝ : α
⊢ Rel
      (↑((fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
          ((fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
            s)))
      a✝ b✝ ↔
    Rel (↑s) a✝ b✝
[PROOFSTEP]
refine ⟨?_, fun h => ⟨_, _, rfl, rfl, h⟩⟩
[GOAL]
case a.H
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : { s // r ≤ s }
a✝ b✝ : α
⊢ Rel
      (↑((fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
          ((fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
            s)))
      a✝ b✝ →
    Rel (↑s) a✝ b✝
[PROOFSTEP]
intro ⟨a, b, hx, hy, H⟩
[GOAL]
case a.H
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : { s // r ≤ s }
a✝ b✝ a b : α
hx : Quotient.mk'' a = Quotient.mk' a✝
hy : Quotient.mk'' b = Quotient.mk' b✝
H : Rel (↑s) a b
⊢ Rel (↑s) a✝ b✝
[PROOFSTEP]
refine s.1.trans' (s.1.symm' <| s.2 <| eq_rel.1 hx) (s.1.trans' H <| s.2 <| (eq_rel.1 hy))
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
⊢ ∀ {a b : { s // r ≤ s }},
    ↑{
              toFun := fun s =>
                mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                  (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
              invFun := fun s =>
                { val := comap Quotient.mk' s,
                  property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
              left_inv :=
                (_ :
                  ∀ (s : { s // r ≤ s }),
                    (fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        ((fun s =>
                            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                          s) =
                      s),
              right_inv :=
                (_ :
                  ∀ (s : Setoid (Quotient r)),
                    (fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        ((fun s =>
                            { val := comap Quotient.mk' s,
                              property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                          s) =
                      s) }
          a ≤
        ↑{
              toFun := fun s =>
                mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                  (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
              invFun := fun s =>
                { val := comap Quotient.mk' s,
                  property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
              left_inv :=
                (_ :
                  ∀ (s : { s // r ≤ s }),
                    (fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        ((fun s =>
                            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                          s) =
                      s),
              right_inv :=
                (_ :
                  ∀ (s : Setoid (Quotient r)),
                    (fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        ((fun s =>
                            { val := comap Quotient.mk' s,
                              property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                          s) =
                      s) }
          b ↔
      a ≤ b
[PROOFSTEP]
intro s t
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
⊢ ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        s ≤
      ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        t ↔
    s ≤ t
[PROOFSTEP]
refine ⟨?_, ?_⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
⊢ ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        s ≤
      ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        t →
    s ≤ t
[PROOFSTEP]
intro h x y hs
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
h :
  ↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      s ≤
    ↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      t
x y : α
hs : Rel (↑s) x y
⊢ Rel (↑t) x y
[PROOFSTEP]
let ⟨a, b, hx, hy, ht⟩ := h ⟨x, y, rfl, rfl, hs⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
h :
  ↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      s ≤
    ↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      t
x y : α
hs : Rel (↑s) x y
a b : α
hx : Quotient.mk'' a = Quotient.mk'' x
hy : Quotient.mk'' b = Quotient.mk'' y
ht : Rel (↑t) a b
⊢ Rel (↑t) x y
[PROOFSTEP]
exact t.1.trans' (t.1.symm' <| t.2 <| eq_rel.1 hx) <| t.1.trans' ht <| t.2 <| eq_rel.1 hy
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
⊢ s ≤ t →
    ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        s ≤
      ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        t
[PROOFSTEP]
intro h x y hs
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
h : s ≤ t
x y : Quotient r
hs :
  Rel
    (↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      s)
    x y
⊢ Rel
    (↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      t)
    x y
[PROOFSTEP]
let ⟨a, b, hx, hy, Hs⟩ := hs
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
h : s ≤ t
x y : Quotient r
hs :
  Rel
    (↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      s)
    x y
a b : α
hx : Quotient.mk'' a = x
hy : Quotient.mk'' b = y
Hs : Rel (↑s) a b
⊢ Rel
    (↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      t)
    x y
[PROOFSTEP]
exact ⟨a, b, hx, hy, h Hs⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
⊢ Subsingleton (Quotient s) ↔ s = ⊤
[PROOFSTEP]
simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply, forall_const]
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → Setoid.Rel s x y
[PROOFSTEP]
refine' (surjective_quotient_mk _).forall.trans (forall_congr' fun a => _)
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk s a = y) ↔ ∀ {y : α}, ⊤ → Setoid.Rel s a y
[PROOFSTEP]
refine' (surjective_quotient_mk _).forall.trans (forall_congr' fun b => _)
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
a b : α
⊢ Quotient.mk s a = Quotient.mk s b ↔ ⊤ → Setoid.Rel s a b
[PROOFSTEP]
simp_rw [← Quotient.mk''_eq_mk, Prop.top_eq_true, true_implies, Quotient.eq'']
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
a b : α
⊢ Setoid.r a b ↔ Setoid.Rel s a b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
⊢ Subsingleton (Quot r) ↔ EqvGen r = ⊤
[PROOFSTEP]
simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply, forall_const]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
⊢ (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ EqvGen r i i_1
[PROOFSTEP]
refine' (surjective_quot_mk _).forall.trans (forall_congr' fun a => _)
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
a : α
⊢ (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ EqvGen r a i
[PROOFSTEP]
refine' (surjective_quot_mk _).forall.trans (forall_congr' fun b => _)
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
a b : α
⊢ mk r a = mk r b ↔ ⊤ ≤ EqvGen r a b
[PROOFSTEP]
rw [Quot.eq]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
a b : α
⊢ EqvGen r a b ↔ ⊤ ≤ EqvGen r a b
[PROOFSTEP]
simp only [forall_const, le_Prop_eq, OrderTop.toTop, Pi.orderTop, Pi.top_apply, Prop.top_eq_true, true_implies]
