X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
⊢ π ⁻¹' (π '' U) = U
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
⊢ π ⁻¹' (π '' U) = U
have lem : ∀ x y, CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U) := by
  rintro _ _ ⟨x⟩
  change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
  rw [H]
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
⊢ π ⁻¹' (π '' U) = U
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
⊢ π ⁻¹' (π '' U) = U
have eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U :=
  { refl := by tauto
    symm := by tauto
    trans := by tauto }
case h
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ π ⁻¹' (π '' U) ↔ x✝ ∈ U
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
⊢ π ⁻¹' (π '' U) = U
ext
case h.mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ π ⁻¹' (π '' U) → x✝ ∈ U

case h.mpr
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ U → x✝ ∈ π ⁻¹' (π '' U)
case h
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ π ⁻¹' (π '' U) ↔ x✝ ∈ U
constructor
case Rel
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
x : X
⊢ f x ∈ U ↔ g x ∈ U
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
⊢ ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
rintro _ _ ⟨x⟩
case Rel
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
x : X
⊢ x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
case Rel
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
x : X
⊢ f x ∈ U ↔ g x ∈ U
change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
no goals
case Rel
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
x : X
⊢ x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
rw [H]
no goals
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
⊢ ∀ (x : Y), x ∈ U ↔ x ∈ U
tauto
no goals
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
⊢ ∀ {x y : Y}, (x ∈ U ↔ y ∈ U) → (y ∈ U ↔ x ∈ U)
tauto
no goals
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
⊢ ∀ {x y z : Y}, (x ∈ U ↔ y ∈ U) → (y ∈ U ↔ z ∈ U) → (x ∈ U ↔ z ∈ U)
tauto
case h.mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈
      ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
          (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv) ⁻¹'
        (((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
            (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv) ''
          U) →
    x✝ ∈ U
case h.mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ π ⁻¹' (π '' U) → x✝ ∈ U
rw [←
  show _ = π from
    h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2
      WalkingParallelPair.one]
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' :
  ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
        (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv)
      y =
    ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
        (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv)
      x✝
⊢ x✝ ∈ U
case h.mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈
      ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
          (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv) ⁻¹'
        (((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
            (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv) ''
          U) →
    x✝ ∈ U
rintro ⟨y, hy, e'⟩
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' :
  (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv
      (Cofork.π (coequalizerColimit f g).cocone y) =
    (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv
      (Cofork.π (coequalizerColimit f g).cocone x✝)
⊢ x✝ ∈ U
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' :
  ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
        (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv)
      y =
    ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
        (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv)
      x✝
⊢ x✝ ∈ U
dsimp at e'
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' : Cofork.π (coequalizerColimit f g).cocone y = Cofork.π (coequalizerColimit f g).cocone x✝
⊢ x✝ ∈ U
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' :
  (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv
      (Cofork.π (coequalizerColimit f g).cocone y) =
    (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv
      (Cofork.π (coequalizerColimit f g).cocone x✝)
⊢ x✝ ∈ U
replace e' :=
  (mono_iff_injective
        (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp
    inferInstance e'
no goals
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' : Cofork.π (coequalizerColimit f g).cocone y = Cofork.π (coequalizerColimit f g).cocone x✝
⊢ x✝ ∈ U
exact (eqv.eqvGen_iff.mp (EqvGen.mono lem (Quot.exact _ e'))).mp hy
no goals
case h.mpr
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ U → x✝ ∈ π ⁻¹' (π '' U)
exact fun hx => ⟨_, hx, rfl⟩