case mp
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ (functor r).map f = (functor r).map f' → r f f'

case mpr
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ r f f' → (functor r).map f = (functor r).map f'
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ (functor r).map f = (functor r).map f' ↔ r f f'
constructor
case mp
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ EqvGen (CompClosure r) f f' → r f f'
case mp
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ (functor r).map f = (functor r).map f' → r f f'
erw [Quot.eq]
case mp
C : Type u_1
inst✝ : Category C
r : HomRel C
h✝ : Congruence r
X Y : C
f f' : X ⟶ Y
h : EqvGen (CompClosure r) f f'
⊢ r f f'
case mp
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ EqvGen (CompClosure r) f f' → r f f'
intro h
case mp.rel
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' m m' : X ⟶ Y
hm : CompClosure r m m'
⊢ r m m'

case mp.refl
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ : X ⟶ Y
⊢ r x✝ x✝

case mp.symm
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ : X ⟶ Y
a✝ : EqvGen (CompClosure r) x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r y✝ x✝

case mp.trans
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ z✝ : X ⟶ Y
a✝¹ : EqvGen (CompClosure r) x✝ y✝
a✝ : EqvGen (CompClosure r) y✝ z✝
a_ih✝¹ : r x✝ y✝
a_ih✝ : r y✝ z✝
⊢ r x✝ z✝
case mp
C : Type u_1
inst✝ : Category C
r : HomRel C
h✝ : Congruence r
X Y : C
f f' : X ⟶ Y
h : EqvGen (CompClosure r) f f'
⊢ r f f'
induction' h with m m' hm
case mp.rel.intro
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
a✝ b✝ : C
f✝ : X ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r (f✝ ≫ m₁✝ ≫ g✝) (f✝ ≫ m₂✝ ≫ g✝)
case mp.rel
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' m m' : X ⟶ Y
hm : CompClosure r m m'
⊢ r m m'
cases hm
case mp.rel.intro.a
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
a✝ b✝ : C
f✝ : X ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r (m₁✝ ≫ g✝) (m₂✝ ≫ g✝)
case mp.rel.intro
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
a✝ b✝ : C
f✝ : X ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r (f✝ ≫ m₁✝ ≫ g✝) (f✝ ≫ m₂✝ ≫ g✝)
apply Congruence.compLeft
case mp.rel.intro.a.a
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
a✝ b✝ : C
f✝ : X ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r m₁✝ m₂✝
case mp.rel.intro.a
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
a✝ b✝ : C
f✝ : X ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r (m₁✝ ≫ g✝) (m₂✝ ≫ g✝)
apply Congruence.compRight
no goals
case mp.rel.intro.a.a
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
a✝ b✝ : C
f✝ : X ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r m₁✝ m₂✝
assumption
case mp.refl
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ : X ⟶ Y
this : IsEquiv (X ⟶ Y) r
⊢ r x✝ x✝
case mp.refl
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ : X ⟶ Y
⊢ r x✝ x✝
haveI := (h.isEquiv : IsEquiv _ (@r X Y))
no goals
case mp.refl
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ : X ⟶ Y
this : IsEquiv (X ⟶ Y) r
⊢ r x✝ x✝
apply refl
case mp.symm.a
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ : X ⟶ Y
a✝ : EqvGen (CompClosure r) x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝
case mp.symm
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ : X ⟶ Y
a✝ : EqvGen (CompClosure r) x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r y✝ x✝
apply symm
no goals
case mp.symm.a
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ : X ⟶ Y
a✝ : EqvGen (CompClosure r) x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝
assumption
no goals
case mp.trans
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ z✝ : X ⟶ Y
a✝¹ : EqvGen (CompClosure r) x✝ y✝
a✝ : EqvGen (CompClosure r) y✝ z✝
a_ih✝¹ : r x✝ y✝
a_ih✝ : r y✝ z✝
⊢ r x✝ z✝
apply _root_.trans <;> assumption
no goals
case mpr
C : Type u_1
inst✝ : Category C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ r f f' → (functor r).map f = (functor r).map f'
apply Quotient.sound