Theorem: Category.imageQuotientFunctor_faithful (CategoryTheory/Exercises1.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
⊢ Faithful (imageQuotientFunctor F)
Tactic:
intro A B f g
State after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ Functor.map (imageQuotientFunctor F) f = Functor.map (imageQuotientFunctor F) g → f = g

State before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ Functor.map (imageQuotientFunctor F) f = Functor.map (imageQuotientFunctor F) g → f = g
Tactic:
refine HomQuotient.inductionOn f ?_
State after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ ∀ (f : A.unquot ⟶ B.unquot),
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f) =
        Functor.map (imageQuotientFunctor F) g →
      HomQuotient.quotHom (imageCongruence F) f = g

State before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ ∀ (f : A.unquot ⟶ B.unquot),
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f) =
        Functor.map (imageQuotientFunctor F) g →
      HomQuotient.quotHom (imageCongruence F) f = g
Tactic:
refine HomQuotient.inductionOn g ?_
State after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ ∀ (f f_1 : A.unquot ⟶ B.unquot),
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f_1) =
        Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f) →
      HomQuotient.quotHom (imageCongruence F) f_1 = HomQuotient.quotHom (imageCongruence F) f

State before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ ∀ (f f_1 : A.unquot ⟶ B.unquot),
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f_1) =
        Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f) →
      HomQuotient.quotHom (imageCongruence F) f_1 = HomQuotient.quotHom (imageCongruence F) f
Tactic:
intro f g h
State after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f✝ g✝ : A ⟶ B
f g : A.unquot ⟶ B.unquot
h :
  Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) g) =
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f)
⊢ HomQuotient.quotHom (imageCongruence F) g = HomQuotient.quotHom (imageCongruence F) f

State before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f✝ g✝ : A ⟶ B
f g : A.unquot ⟶ B.unquot
h :
  Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) g) =
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f)
⊢ HomQuotient.quotHom (imageCongruence F) g = HomQuotient.quotHom (imageCongruence F) f
Tactic:
rw [HomQuotient.quotHom_eq_iff]
State after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f✝ g✝ : A ⟶ B
f g : A.unquot ⟶ B.unquot
h :
  Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) g) =
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f)
⊢ Congruence.rel (imageCongruence F) A.unquot B.unquot g f

State before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f✝ g✝ : A ⟶ B
f g : A.unquot ⟶ B.unquot
h :
  Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) g) =
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f)
⊢ Congruence.rel (imageCongruence F) A.unquot B.unquot g f
Tactic:
exact h
State after:
no goals