awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F : Functor.{v_2, v_3, u_2, u_3} D E
h : (W.Q ⋙ Construction.lift (W := W) L ⋯) ⋙ F = L ⋙ F
⊢ (obj
          (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
            Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
          F).obj
      (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F) =
    (obj (whiskeringLeftFunctor L W E) F).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)

Tactic:
change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ F = L ⋙ F

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.Localization.Construction.lift, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F : Functor.{v_2, v_3, u_2, u_3} D E
h h₁ : L ⋙ F = L ⋙ F
⊢ (W.Q ⋙ Construction.lift (W := W) L ⋯) ⋙ F = L ⋙ F

Tactic:
rw [Construction.fac]

Premises used: CategoryTheory.Localization.Construction.fac
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
x : C
h :
  Eq (α :=
    X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ⟶
      (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x)
    (τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
      NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x)
    (NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x ≫
      NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x)
⊢ Eq (α :=
    (obj
                (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                  Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                X).obj
            (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x ⟶
      (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (map
            (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
              Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
            τ ≫
          Iso.hom
            ((fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦
                (eqToIso ⋯ :
                  obj
                      (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                        Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                      F ≅
                    obj (whiskeringLeftFunctor L W E) F))
              Y)))
      x)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (Iso.hom
            ((fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦
                (eqToIso ⋯ :
                  obj
                      (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                        Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                      F ≅
                    obj (whiskeringLeftFunctor L W E) F))
              X) ≫
          map (whiskeringLeftFunctor L W E) τ))
      x)

Tactic:
dsimp [Construction.whiskeringLeftEquivalence, equivalenceFromModel, whiskerLeft]

Premises used: CategoryTheory.Localization.Construction.whiskeringLeftEquivalence, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Localization.equivalenceFromModel
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
x : C
h :
  τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
      𝟙
        ((obj (Construction.WhiskeringLeftEquivalence.functor W E) (Construction.lift (W := W) L ⋯ ⋙ Y)).obj (P :=
              fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
          x) =
    𝟙
        ((obj (Construction.WhiskeringLeftEquivalence.functor W E) (Construction.lift (W := W) L ⋯ ⋙ X)).obj (P :=
              fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
          x) ≫
      NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x
⊢ Eq (α :=
    X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ⟶
      (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x)
    (τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
      NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x)
    (NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x ≫
      NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x)

Tactic:
rw [ObjectProperty.eqToHom_hom, ObjectProperty.eqToHom_hom, eqToHom_app, eqToHom_app,
          eqToHom_refl, eqToHom_refl]

Premises used: CategoryTheory.ObjectProperty.eqToHom_hom, CategoryTheory.eqToHom_app, CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
x : C
h :
  τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
      𝟙 (Y.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W)))) =
    𝟙 (X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W)))) ≫
      NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x
⊢ τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
      𝟙
        ((obj (Construction.WhiskeringLeftEquivalence.functor W E) (Construction.lift (W := W) L ⋯ ⋙ Y)).obj (P :=
              fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
          x) =
    𝟙
        ((obj (Construction.WhiskeringLeftEquivalence.functor W E) (Construction.lift (W := W) L ⋯ ⋙ X)).obj (P :=
              fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
          x) ≫
      NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
x : C
h :
  Eq (α :=
    X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ⟶
      (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x)
    (τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))))
    (NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x)
⊢ τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
      𝟙 (Y.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W)))) =
    𝟙 (X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W)))) ≫
      NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x

Tactic:
rw [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
x : C
⊢ Eq (α :=
    X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ⟶
      (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x)
    (τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))))
    (NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
iso : Iso (C := Functor.{v_2, v_3, u_2, u_3} D E ⥤ MorphismProperty.FunctorsInverting.{v_1, u_1, v_3, u_3} W E)
  (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
    Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
  (whiskeringLeftFunctor L W E) :=
  NatIso.ofComponents (fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦ eqToIso ⋯) ⋯
⊢ IsEquivalence (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)

Tactic:
Functor.isEquivalence_of_iso iso

Premises used: CategoryTheory.Functor.isEquivalence_of_iso
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
iso : Iso (C := Functor.{v_2, v_3, u_2, u_3} D E ⥤ MorphismProperty.FunctorsInverting.{v_1, u_1, v_3, u_3} W E)
  (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
    Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
  (whiskeringLeftFunctor L W E) :=
  NatIso.ofComponents (fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦ eqToIso ⋯) ⋯
⊢ IsEquivalence (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)

Tactic:
exact Functor.isEquivalence_of_iso iso

Premises used: CategoryTheory.Functor.isEquivalence_of_iso
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
⊢ Eq (α := Functor.{v_2, v_3, u_2, u_3} D E ⥤ Functor.{v_1, v_3, u_1, u_3} C E) (whiskeringLeftFunctor' L W E)
    (whiskeringLeftFunctor L W E ⋙
      inducedFunctor
        (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Localization.whiskeringLeftFunctor', rfl
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F : Functor.{v_2, v_3, u_2, u_3} D E
⊢ obj (whiskeringLeftFunctor' L W E) F = L ⋙ F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
apply : Full (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)
apply₁ :
  Full (C := MorphismProperty.FunctorsInverting.{v_1, u_1, v_3, u_3} W E)
    (inducedFunctor
      (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))
⊢ Full (C := Functor.{v_2, v_3, u_2, u_3} D E)
    (whiskeringLeftFunctor L W E ⋙
      inducedFunctor
        (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))

Tactic:
apply @Functor.Full.comp _ _ _ _ _ _ _ _ ?_ ?_

Premises used: CategoryTheory.Functor.Full.comp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
⊢ Full (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
⊢ Full (C := MorphismProperty.FunctorsInverting.{v_1, u_1, v_3, u_3} W E)
    (inducedFunctor
      (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))

Tactic:
apply InducedCategory.full

Premises used: CategoryTheory.InducedCategory.full
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
apply : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)
apply₁ :
  Faithful (C := MorphismProperty.FunctorsInverting.{v_1, u_1, v_3, u_3} W E)
    (inducedFunctor
      (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))
⊢ Faithful (C := Functor.{v_2, v_3, u_2, u_3} D E)
    (whiskeringLeftFunctor L W E ⋙
      inducedFunctor
        (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))

Tactic:
apply @Functor.Faithful.comp _ _ _ _ _ _ _ _ ?_ ?_

Premises used: CategoryTheory.Functor.Faithful.comp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
⊢ Faithful (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
⊢ Faithful (C := MorphismProperty.FunctorsInverting.{v_1, u_1, v_3, u_3} W E)
    (inducedFunctor
      (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))

Tactic:
apply InducedCategory.faithful

Premises used: CategoryTheory.InducedCategory.faithful
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
E : Type u_4
inst_3 : Category.{v_4, u_4} E
⊢ Full (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)

Tactic:
inferInstanceAs (whiskeringLeftFunctor' L W E).Full

Premises used: _private.0.CategoryTheory.Localization.full_whiskeringLeft._proof_1
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
E : Type u_4
inst_3 : Category.{v_4, u_4} E
⊢ Faithful (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)

Tactic:
inferInstanceAs (whiskeringLeftFunctor' L W E).Faithful

Premises used: _private.0.CategoryTheory.Localization.faithful_whiskeringLeft._proof_1
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
E_1 : Type u_3
inst_2 : Category.{v_3, u_3} E_1
inst_3 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_4 : L.IsLocalization W
E : Type u_4
inst_5 : Category.{v_4, u_4} E
⊢ Full (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)

Tactic:
have := full_whiskeringLeft L W E
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
E_1 : Type u_3
inst_2 : Category.{v_3, u_3} E_1
inst_3 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_4 : L.IsLocalization W
E : Type u_4
inst_5 : Category.{v_4, u_4} E
this : Full (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)
⊢ Faithful (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)

Tactic:
have := faithful_whiskeringLeft L W E
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
E_1 : Type u_3
inst_2 : Category.{v_3, u_3} E_1
inst_3 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_4 : L.IsLocalization W
E : Type u_4
inst_5 : Category.{v_4, u_4} E
this_1 : Full (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)
this : Faithful (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)
⊢ FullyFaithful (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)

Tactic:
exact FullyFaithful.ofFullyFaithful _

Premises used: CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), Eq (α := F₁.obj (L.obj X) ⟶ F₂.obj (L.obj X)) (τ.app (L.obj X)) (τ'.app (L.obj X))
⊢ L.EssSurj

Tactic:
haveI := essSurj L W
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), Eq (α := F₁.obj (L.obj X) ⟶ F₂.obj (L.obj X)) (τ.app (L.obj X)) (τ'.app (L.obj X))
this : L.EssSurj
w : ∀ (Y : D), τ.app Y = τ'.app Y
⊢ τ = τ'

Tactic:
ext Y
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), Eq (α := F₁.obj (L.obj X) ⟶ F₂.obj (L.obj X)) (τ.app (L.obj X)) (τ'.app (L.obj X))
this : L.EssSurj
Y : D
w :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y) (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ.app Y)
    (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ'.app Y)
w₁ :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y)
    (τ.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
    (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ'.app Y)
w₂ :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y)
    (τ.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
    (τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
w₃ w₄ :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y)
    (τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
    (τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
⊢ τ.app Y = τ'.app Y

Tactic:
rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.NatTrans.naturality, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C E
F₁' F₂' : Functor.{v_2, v_3, u_2, u_3} D E
inst_4 : Lifting L W F₁ F₁'
inst_5 : Lifting L W F₂ F₂'
τ : F₁ ⟶ F₂
X : C
⊢ (liftNatTrans L W F₁ F₂ F₁' F₂' τ).app (L.obj X) =
    (Lifting.iso L W F₁ F₁').hom.app X ≫ τ.app X ≫ (Lifting.iso L W F₂ F₂').inv.app X

Tactic:
congr_app (Functor.map_preimage (whiskeringLeftFunctor' L W E) _) X

Premises used: CategoryTheory.Localization.whiskeringLeftFunctor', CategoryTheory.congr_app, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F₁ F₂ F₃ : Functor.{v_1, v_3, u_1, u_3} C E
F₁' F₂' F₃' : Functor.{v_2, v_3, u_2, u_3} D E
h₁ : Lifting L W F₁ F₁'
h₂ : Lifting L W F₂ F₂'
h₃ : Lifting L W F₃ F₃'
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
X : C
⊢ Eq (α := F₁'.obj (L.obj X) ⟶ F₃'.obj (L.obj X))
    ((liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ').app (L.obj X))
    ((liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ')).app (L.obj X))

Tactic:
simp only [NatTrans.comp_app, liftNatTrans_app, assoc, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F : Functor.{v_1, v_3, u_1, u_3} C E
F' : Functor.{v_2, v_3, u_2, u_3} D E
h : Lifting L W F F'
X : C
simp : Eq.{v_3 + 1} (α := F'.obj (L.obj X) ⟶ F'.obj (L.obj X)) (𝟙 ((L ⋙ F').obj X)) (𝟙 (F'.obj (L.obj X)))
⊢ Eq (α := F'.obj (L.obj X) ⟶ F'.obj (L.obj X)) ((liftNatTrans L W F F F' F' (𝟙 F)).app (L.obj X))
    (NatTrans.app (𝟙 F') (L.obj X))

Tactic:
simp only [liftNatTrans_app, NatTrans.id_app, id_comp, Iso.hom_inv_id_app]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.NatTrans.id_app, CategoryTheory.Category.id_comp