awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
X Y : Quotient r
f : Hom r X Y
⊢ ∀ (a : X.as (r := r) ⟶ Y.as (r := r)),
    comp r (Quot.mk (HomRel.CompClosure r) a) (Quot.mk (HomRel.CompClosure r) (𝟙 (Y.as (r := r)))) =
      Quot.mk (HomRel.CompClosure r) a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
W X Y Z : Quotient r
f : Hom r W X
g : Hom r X Y
h : Hom r Y Z
⊢ ∀ (a : Y.as (r := r) ⟶ Z.as (r := r)) (a_1 : X.as (r := r) ⟶ Y.as (r := r)) (a_2 : W.as (r := r) ⟶ X.as (r := r)),
    comp r (comp r (Quot.mk (HomRel.CompClosure r) a_2) (Quot.mk (HomRel.CompClosure r) a_1))
        (Quot.mk (HomRel.CompClosure r) a) =
      comp r (Quot.mk (HomRel.CompClosure r) a_2)
        (comp r (Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r_1 : HomRel.{u_1, v_1} C
G : Type u_2
inst_1 : Groupoid.{u_3, u_2} G
r : HomRel.{u_2, u_3} G
X Y : Quotient r
f : X ⟶ Y
x x_1 : X.as (r := r) ⟶ Y.as (r := r)
con : HomRel.CompClosure r x x_1
obtain :
  ∀ ⦃X_1 Y_1 : G⦄ (a b : G) (f g : a ⟶ b) (hfg : r f g) (a_1 : X.as (r := r) ⟶ a) (b_1 : b ⟶ Y.as (r := r)),
    Eq.{u_3 + 1} (α := Y ⟶ X)
      ((fun (f' : X.as (r := r) ⟶ Y.as (r := r)) ↦
          (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
            Quot (α := Y.as (r := r) ⟶ X.as (r := r)) (HomRel.CompClosure r)))
        (a_1 ≫ f ≫ b_1))
      ((fun (f' : X.as (r := r) ⟶ Y.as (r := r)) ↦
          (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
            Quot (α := Y.as (r := r) ⟶ X.as (r := r)) (HomRel.CompClosure r)))
        (a_1 ≫ g ≫ b_1))
⊢ Eq.{u_3 + 1} (α := Y ⟶ X)
    ((fun (f' : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
          Quot (α := Y.as (r := r) ⟶ X.as (r := r)) (HomRel.CompClosure r)))
      x)
    ((fun (f' : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
          Quot (α := Y.as (r := r) ⟶ X.as (r := r)) (HomRel.CompClosure r)))
      x_1)

Tactic:
obtain ⟨_, _, a, f, g, b, hfg⟩ := con
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r_1 : HomRel.{u_1, v_1} C
G : Type u_2
inst_1 : Groupoid.{u_3, u_2} G
r : HomRel.{u_2, u_3} G
X_1 Y_1 : Quotient r
f_1 : X_1 ⟶ Y_1
X Y a_1 b_1 : G
f g : a_1 ⟶ b_1
hfg : r f g
a : X_1.as (r := r) ⟶ a_1
b : b_1 ⟶ Y_1.as (r := r)
⊢ Eq.{u_3 + 1} (α := Y_1 ⟶ X_1)
    ((fun (f' : X_1.as (r := r) ⟶ Y_1.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
          Quot (α := Y_1.as (r := r) ⟶ X_1.as (r := r)) (HomRel.CompClosure r)))
      (a ≫ f ≫ b))
    ((fun (f' : X_1.as (r := r) ⟶ Y_1.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
          Quot (α := Y_1.as (r := r) ⟶ X_1.as (r := r)) (HomRel.CompClosure r)))
      (a ≫ g ≫ b))

Tactic:
simpa using (Quot.sound (HomRel.CompClosure.intro _ _
      (inv b ≫ inv g) _ _ (inv f ≫ inv a) hfg)).symm

Premises used: Quot.sound, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, Eq.symm, CategoryTheory.HomRel.CompClosure.intro
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
G : Type u_2
inst : Groupoid.{u_3, u_2} G
r : HomRel.{u_2, u_3} G
X Y : Quotient r
f : X.as (r := r) ⟶ Y.as (r := r)
⊢ Quotient.inv r (Quot.mk (HomRel.CompClosure r) f) = Quot.mk (HomRel.CompClosure r) (Groupoid.inv f)

Tactic:
rfl

Premises used: rfl, CategoryTheory.Quotient.inv
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r_1 : HomRel.{u_1, v_1} C
G : Type u_2
inst_1 : Groupoid.{u_3, u_2} G
r : HomRel.{u_2, u_3} G
X Y : Quotient r
f : X ⟶ Y
⊢ ∀ (a : X.as (r := r) ⟶ Y.as (r := r)),
    Quotient.inv r (Quot.mk (HomRel.CompClosure r) a) ≫ Quot.mk (HomRel.CompClosure r) a = 𝟙 Y

Tactic:
simp [CategoryStruct.comp, CategoryStruct.id]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r_1 : HomRel.{u_1, v_1} C
G : Type u_2
inst_1 : Groupoid.{u_3, u_2} G
r : HomRel.{u_2, u_3} G
X Y : Quotient r
f : X ⟶ Y
⊢ ∀ (a : X.as (r := r) ⟶ Y.as (r := r)),
    Quot.mk (HomRel.CompClosure r) a ≫ Quotient.inv r (Quot.mk (HomRel.CompClosure r) a) = 𝟙 X

Tactic:
simp [CategoryStruct.comp, CategoryStruct.id]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
X Y : C
f : (functor r).obj X ⟶ (functor r).obj Y
⊢ (functor r).map (Quot.out (r := HomRel.CompClosure r) f) = f

Tactic:
simp [functor]

Premises used: CategoryTheory.Quotient.functor
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : Unique C
a : Quotient r
as : a.as (r := r) = Quotient.as (r := r) default
⊢ a = default

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : Unique C
a : Quotient r
⊢ a.as (r := r) = as (r := r) default

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : ∀ (x y : C), Subsingleton.{v_1 + 1} (x ⟶ y)
x y : Quotient r
⊢ Subsingleton.{v_1 + 1} (x ⟶ y)

Tactic:
(full_functor r).map_surjective.subsingleton

Premises used: CategoryTheory.Functor.Full.map_surjective, Function.Surjective.subsingleton
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
x y : C
f_1 : Quiver.Hom (V := Quotient r) (mk (r := r) x) (mk (r := r) y)
f : as (r := r) (mk (r := r) x) ⟶ as (r := r) (mk (r := r) y)
⊢ P (Quot.mk (HomRel.CompClosure r) f)

Tactic:
h f
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
x y : C
f_1 : Quiver.Hom (V := Quotient r) (mk (r := r) x) (mk (r := r) y)
f : as (r := r) (mk (r := r) x) ⟶ as (r := r) (mk (r := r) y)
⊢ P (Quot.mk (HomRel.CompClosure r) f)

Tactic:
exact h f
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
a b : C
f₁ f₂ : a ⟶ b
h : r f₁ f₂
⊢ (functor r).map f₁ = (functor r).map f₂

Tactic:
simpa using Quot.sound (HomRel.CompClosure.intro _ _ (𝟙 a) f₁ f₂ (𝟙 b) h)

Premises used: Quot.sound, CategoryTheory.CategoryStruct.id, CategoryTheory.HomRel.CompClosure.intro
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
h : Congruence r
X Y : C
f f' : X ⟶ Y
dsimp :
  Eq (α := Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)) (Quot.mk (HomRel.CompClosure r) f)
      (Quot.mk (HomRel.CompClosure r) f') ↔
    r f f'
⊢ (functor r).map f = (functor r).map f' ↔ r f f'

Tactic:
dsimp [functor]

Premises used: CategoryTheory.Quotient.functor
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
h : Congruence r
X Y : C
f f' : X ⟶ Y
h₁ : _root_.Equivalence (α := X ⟶ Y) (HomRel.CompClosure r)
⊢ Eq (α := Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)) (Quot.mk (HomRel.CompClosure r) f)
      (Quot.mk (HomRel.CompClosure r) f') ↔
    r f f'

Tactic:
rw [Equivalence.quot_mk_eq_iff, HomRel.compClosure_eq_self r]

Premises used: CategoryTheory.HomRel.compClosure_eq_self, Equivalence.quot_mk_eq_iff
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ _root_.Equivalence (α := X ⟶ Y) (HomRel.CompClosure r)

Tactic:
simpa only [HomRel.compClosure_eq_self r] using h.equivalence

Premises used: CategoryTheory.Congruence.equivalence, CategoryTheory.HomRel.compClosure_eq_self
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
X Y : C
f g : X ⟶ Y
⊢ (functor r).homRel f g ↔ Relation.EqvGen (HomRel.CompClosure r) f g

Tactic:
Quot.eq

Premises used: CategoryTheory.Quotient.Hom, Quot.eq, CategoryTheory.Functor.homRel
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
⊢ Congruence (functor r).homRel

Tactic:
(inferInstance : Congruence (functor r).homRel)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
h : ∀ (x x_1 : C), Eq (α := (x ⟶ x_1) → (x ⟶ x_1) → Prop) (Relation.EqvGen (HomRel.CompClosure r)) (functor r).homRel
⊢ Congruence.{v_1, u_1} (C := C) fun (X Y : C) ↦ Relation.EqvGen (HomRel.CompClosure r)

Tactic:
convert! (inferInstance : Congruence (functor r).homRel)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
x x_1 : C
h : ∀ (x_2 x_3 : x ⟶ x_1), Relation.EqvGen (HomRel.CompClosure r) x_2 x_3 ↔ (functor r).homRel x_2 x_3
⊢ Eq (α := (x ⟶ x_1) → (x ⟶ x_1) → Prop) (Relation.EqvGen (HomRel.CompClosure r)) (functor r).homRel

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
x x_1 : C
x_2 x_3 : x ⟶ x_1
h h₁ : Relation.EqvGen (HomRel.CompClosure r) x_2 x_3 ↔ Relation.EqvGen (HomRel.CompClosure r) x_2 x_3
⊢ Relation.EqvGen (HomRel.CompClosure r) x_2 x_3 ↔ (functor r).homRel x_2 x_3

Tactic:
rw [functor_homRel_eq_compClosure_eqvGen]

Premises used: CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X_1 Y_1 : Quotient r
hf : X_1 ⟶ Y_1
X Y a b : C
m₁ m₂ : a ⟶ b
h : r m₁ m₂
f : X_1.as (r := r) ⟶ a
g : b ⟶ Y_1.as (r := r)
⊢ Eq.{v_2 + 1} (α := F.obj (X_1.as (r := r)) ⟶ F.obj (Y_1.as (r := r)))
    ((fun (f : X_1.as (r := r) ⟶ Y_1.as (r := r)) ↦ F.map f) (f ≫ m₁ ≫ g))
    ((fun (f : X_1.as (r := r) ⟶ Y_1.as (r := r)) ↦ F.map f) (f ≫ m₂ ≫ g))

Tactic:
simp [H _ _ _ _ h]
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b c : Quotient r
f_1 : a ⟶ b
f : a.as (r := r) ⟶ b.as (r := r)
g_1 : b ⟶ c
g : b.as (r := r) ⟶ c.as (r := r)
⊢ Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) f ≫ Quot.mk (HomRel.CompClosure r) g)
      (fun (f : a.as (r := r) ⟶ c.as (r := r)) ↦ F.map f) ⋯ =
    Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) f)
        (fun (f : a.as (r := r) ⟶ b.as (r := r)) ↦ F.map f) ⋯ ≫
      Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) g)
        (fun (f : b.as (r := r) ⟶ c.as (r := r)) ↦ F.map f) ⋯

Tactic:
F.map_comp f g

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b c : Quotient r
f_1 : a ⟶ b
f : a.as (r := r) ⟶ b.as (r := r)
g_1 : b ⟶ c
g : b.as (r := r) ⟶ c.as (r := r)
⊢ Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) f ≫ Quot.mk (HomRel.CompClosure r) g)
      (fun (f : a.as (r := r) ⟶ c.as (r := r)) ↦ F.map f) ⋯ =
    Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) f)
        (fun (f : a.as (r := r) ⟶ b.as (r := r)) ↦ F.map f) ⋯ ≫
      Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) g)
        (fun (f : b.as (r := r) ⟶ c.as (r := r)) ↦ F.map f) ⋯

Tactic:
exact F.map_comp f g

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ functor r ⋙ lift r F H = F

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
hΦ : functor r ⋙ Φ = F
subst_vars :
  ∀ (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂),
    Φ = lift r (functor r ⋙ Φ) H
⊢ Φ = lift r F H

Tactic:
subst_vars
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
h_obj : ∀ (X : Quotient r), Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X
h_map : ∀ (X Y : Quotient r) (f : X ⟶ Y), Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f
⊢ Φ = lift r (functor r ⋙ Φ) H

Tactic:
fapply Functor.hext

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X : Quotient r
h_obj : Φ.obj X = Φ.obj ((functor r).obj (X.as (r := r)))
⊢ Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X

Tactic:
dsimp [lift, Functor]

Premises used: CategoryTheory.Functor, CategoryTheory.Quotient.lift
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X : Quotient r
⊢ Φ.obj X = Φ.obj ((functor r).obj (X.as (r := r)))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X Y : Quotient r
f : X ⟶ Y
h_map :
  Φ.map f ≍
    Quot.liftOn (r := HomRel.CompClosure r) f (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) ⋯
⊢ Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f

Tactic:
dsimp [lift, Functor]

Premises used: CategoryTheory.Functor, CategoryTheory.Quotient.lift
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X Y : Quotient r
f : X ⟶ Y
⊢ Φ.map f ≍
    Quot.liftOn (r := HomRel.CompClosure r) f (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) ⋯

Tactic:
Quot.inductionOn f fun _ ↦ ?_

Premises used: Quot.inductionOn
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X Y : Quotient r
f : X ⟶ Y
h_map :
  ∀ (x : X.as (r := r) ⟶ Y.as (r := r)),
    Φ.map (Quot.mk (HomRel.CompClosure r) x) ≍
      Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) x)
        (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) ⋯
⊢ Φ.map f ≍
    Quot.liftOn (r := HomRel.CompClosure r) f (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) ⋯

Tactic:
refine Quot.inductionOn f fun _ ↦ ?_
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X Y : Quotient r
f : X ⟶ Y
x : X.as (r := r) ⟶ Y.as (r := r)
h_map :
  Φ.map (Quot.mk (HomRel.CompClosure r) x) =
    Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) x)
      (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) ⋯
⊢ Φ.map (Quot.mk (HomRel.CompClosure r) x) ≍
    Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) x)
      (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) ⋯

Tactic:
simp only [heq_eq_eq]

Premises used: heq_eq_eq
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X Y : Quotient r
f : X ⟶ Y
x : X.as (r := r) ⟶ Y.as (r := r)
⊢ Φ.map (Quot.mk (HomRel.CompClosure r) x) =
    Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) x)
      (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) ⋯

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h : functor r ⋙ F₁ = functor r ⋙ F₂
rw : F₁ = lift r (functor r ⋙ F₂) ⋯
rw₁ : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂
⊢ F₁ = F₂

Tactic:
rw [lift_unique r (functor r ⋙ F₂) _ F₂ rfl]

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Functor.comp, CategoryTheory.Quotient.lift_unique, rfl
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h_1 : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f g : X ⟶ Y
h : r f g
dsimp : F₂.map ((functor r).map f) = F₂.map ((functor r).map g)
⊢ (functor r ⋙ F₂).map f = (functor r ⋙ F₂).map g

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h_1 : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f g : X ⟶ Y
h : r f g
rw rw₁ : F₂.map ((functor r).map g) = F₂.map ((functor r).map g)
⊢ F₂.map ((functor r).map f) = F₂.map ((functor r).map g)

Tactic:
rw [Quotient.sound r h]

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h hΦ : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = lift r (functor r ⋙ F₂) ⋯

Tactic:
apply lift_unique

Premises used: CategoryTheory.Quotient.lift_unique
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h : functor r ⋙ F₁ = functor r ⋙ F₂
hΦ hΦ₁ : functor r ⋙ F₂ = functor r ⋙ F₂
⊢ functor r ⋙ F₁ = functor r ⋙ F₂

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (isLift r F H).hom.app X = 𝟙 (F.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (isLift r F H).inv.app X = 𝟙 (F.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F H).obj ((functor r).obj X) = F.obj X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (lift r F H).map ((functor r).map f) = F.map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ₁ τ₂ : F ⟶ G
h : (functor r).whiskerLeft τ₁ = (functor r).whiskerLeft τ₂
h₁ :
  ∀ (X : C), Eq (α := F.obj (mk (r := r) X) ⟶ G.obj (mk (r := r) X)) (τ₁.app (mk (r := r) X)) (τ₂.app (mk (r := r) X))
⊢ τ₁.app = τ₂.app

Tactic:
ext1 ⟨X⟩
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ₁ τ₂ : F ⟶ G
h : (functor r).whiskerLeft τ₁ = (functor r).whiskerLeft τ₂
X : C
⊢ Eq (α := F.obj (mk (r := r) X) ⟶ G.obj (mk (r := r) X)) (τ₁.app (mk (r := r) X)) (τ₂.app (mk (r := r) X))

Tactic:
NatTrans.congr_app h X

Premises used: CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ₁ τ₂ : F ⟶ G
h : (functor r).whiskerLeft τ₁ = (functor r).whiskerLeft τ₂
X : C
⊢ Eq (α := F.obj (mk (r := r) X) ⟶ G.obj (mk (r := r) X)) (τ₁.app (mk (r := r) X)) (τ₂.app (mk (r := r) X))

Tactic:
exact NatTrans.congr_app h X

Premises used: CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ⟶ functor r ⋙ G
x x_1 : Quotient r
X Y : C
f_1 : Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)
f : as (r := r) (mk (r := r) X) ⟶ as (r := r) (mk (r := r) Y)
⊢ Eq (α := F.obj (mk (r := r) X) ⟶ G.obj (mk (r := r) Y))
    (F.map (Quot.mk (HomRel.CompClosure r) f) ≫
      match (motive := (x : Quotient r) → F.obj x ⟶ G.obj x) mk (r := r) Y with
      | { as := X } => τ.app X)
    ((match (motive := (x : Quotient r) → F.obj x ⟶ G.obj x) mk (r := r) X with
      | { as := X } => τ.app X) ≫
      G.map (Quot.mk (HomRel.CompClosure r) f))

Tactic:
τ.naturality f

Premises used: CategoryTheory.NatTrans.naturality