awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
apply :
  ∀ (X : C₁),
    Eq (α := (𝟭 D₁ ⋙ G').obj (L₁.obj X) ⟶ (G' ⋙ 𝟭 D₂).obj (L₁.obj X))
      ((whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
            (G'.associator F' G').hom ≫ G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F')).app
        (L₁.obj X))
      ((NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X))
⊢ whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
      (G'.associator F' G').hom ≫ G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F') =
    NatTrans.id (𝟭 D₁ ⋙ G')

Tactic:
apply natTrans_ext L₁ W₁

Premises used: CategoryTheory.Localization.natTrans_ext
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ (whiskerRight adj.unit G ≫ G.whiskerLeft adj.counit).app X₁ = NatTrans.app (𝟙 (𝟭 C₁ ⋙ G)) X₁

Tactic:
have eq := congr_app adj.left_triangle X₁
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
rw :
  G'.map (L₁.map (adj.unit.app X₁)) ≫
      G'.map ((CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) ≫
        G'.map (F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)) ≫
          (Localization.η adj L₁ L₂ W₂ G' F').app (G'.obj (L₁.obj X₁)) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
⊢ Eq (α := (𝟭 D₁ ⋙ G').obj (L₁.obj X₁) ⟶ (G' ⋙ 𝟭 D₂).obj (L₁.obj X₁))
    ((whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
          (G'.associator F' G').hom ≫ G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F')).app
      (L₁.obj X₁))
    ((NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁))

Tactic:
rw [NatTrans.comp_app, NatTrans.comp_app, whiskerRight_app, Localization.ε_app,
          Functor.associator_hom_app, id_comp, whiskerLeft_app, G'.map_comp, G'.map_comp,
          assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.Localization.ε_app, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
erw : 𝟙 ((L₁ ⋙ G').obj (obj.{v_1, v_1, u_1, u_1} (𝟭 C₁) X₁)) = (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
⊢ G'.map (L₁.map (adj.unit.app X₁)) ≫
      G'.map ((CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) ≫
        G'.map (F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)) ≫
          (Localization.η adj L₁ L₂ W₂ G' F').app (G'.obj (L₁.obj X₁)) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)

Tactic:
erw [(Localization.η adj L₁ L₂ W₂ G' F').naturality, Localization.η_app,
          assoc, assoc, ← G'.map_comp_assoc, ← G'.map_comp_assoc, assoc, Iso.hom_inv_id_app,
          comp_id, (CatCommSq.iso G L₁ L₂ G').inv.naturality_assoc, ← L₂.map_comp_assoc, eq,
          L₂.map_id, id_comp, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, CategoryTheory.CatCommSq.iso, CategoryTheory.Adjunction.Localization.η, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Adjunction.Localization.η_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ 𝟙 ((L₁ ⋙ G').obj (obj.{v_1, v_1, u_1, u_1} (𝟭 C₁) X₁)) = (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
apply :
  ∀ (X : C₂),
    Eq (α := (F' ⋙ 𝟭 D₁).obj (L₂.obj X) ⟶ (𝟭 D₂ ⋙ F').obj (L₂.obj X))
      ((F'.whiskerLeft (Localization.ε adj L₁ W₁ L₂ G' F') ≫
            (F'.associator G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F').app
        (L₂.obj X))
      ((NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X))
⊢ F'.whiskerLeft (Localization.ε adj L₁ W₁ L₂ G' F') ≫
      (F'.associator G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F' =
    NatTrans.id (F' ⋙ 𝟭 D₁)

Tactic:
apply natTrans_ext L₂ W₂

Premises used: CategoryTheory.Localization.natTrans_ext
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ (F.whiskerLeft adj.unit ≫ whiskerRight adj.counit F).app X₂ = NatTrans.app (𝟙 (F ⋙ 𝟭 C₁)) X₂

Tactic:
have eq := congr_app adj.right_triangle X₂
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
rw :
  (Localization.ε adj L₁ W₁ L₂ G' F').app (F'.obj (L₂.obj X₂)) ≫
      F'.map (G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂)) ≫
        F'.map ((CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
⊢ Eq (α := (F' ⋙ 𝟭 D₁).obj (L₂.obj X₂) ⟶ (𝟭 D₂ ⋙ F').obj (L₂.obj X₂))
    ((F'.whiskerLeft (Localization.ε adj L₁ W₁ L₂ G' F') ≫
          (F'.associator G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F').app
      (L₂.obj X₂))
    ((NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂))

Tactic:
rw [NatTrans.comp_app, NatTrans.comp_app, whiskerLeft_app, whiskerRight_app,
          Localization.η_app, Functor.associator_inv_app, id_comp, F'.map_comp, F'.map_comp]

Premises used: CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.associator_inv_app, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Adjunction.Localization.η_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
erw : 𝟙 ((L₂ ⋙ F').obj X₂) = (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
⊢ (Localization.ε adj L₁ W₁ L₂ G' F').app (F'.obj (L₂.obj X₂)) ≫
      F'.map (G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂)) ≫
        F'.map ((CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)

Tactic:
erw [← (Localization.ε _ _ _ _ _ _).naturality_assoc, Localization.ε_app,
          assoc, assoc, ← F'.map_comp_assoc, Iso.hom_inv_id_app, F'.map_id, id_comp,
          ← NatTrans.naturality, ← L₁.map_comp_assoc, eq, L₁.map_id, id_comp,
          Iso.inv_hom_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.Localization.ε_app, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Adjunction.Localization.ε, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ 𝟙 ((L₂ ⋙ F').obj X₂) = (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ (adj.localization L₁ W₁ L₂ W₂ G' F').unit.app (L₁.obj X₁) =
    L₁.map (adj.unit.app X₁) ≫
      (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)

Tactic:
apply Localization.ε_app

Premises used: CategoryTheory.Adjunction.Localization.ε_app
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ (adj.localization L₁ W₁ L₂ W₂ G' F').counit.app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Tactic:
apply Localization.η_app

Premises used: CategoryTheory.Adjunction.Localization.η_app
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
⊢ W.IsInvertedBy G

Tactic:
have hG : W.IsInvertedBy G := fun _ _ _ hf => hf
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
hG : W.IsInvertedBy G
X : C₁
change : IsIso (G.map (adj.unit.app X))
⊢ W (adj.unit.app X)

Tactic:
change IsIso _

Premises used: CategoryTheory.IsIso
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
hG : W.IsInvertedBy G
X : C₁
⊢ IsIso (G.map (adj.unit.app X))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
hG : W.IsInvertedBy G
⊢ ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)

Tactic:
have : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X) := fun X =>
    Localization.inverts W.Q W _ (by
      change IsIso _
      infer_instance)
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
hG : W.IsInvertedBy G
this : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
⊢ IsIso (whiskerRight adj.unit W.Q)

Tactic:
have : IsIso (whiskerRight adj.unit W.Q) := NatIso.isIso_of_isIso_app _
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
hG : W.IsInvertedBy G
this_1 : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
this : IsIso (whiskerRight adj.unit W.Q)
e : W.Localization ≌ C₂ :=
  Equivalence.mk (lift (W := W) G hG W.Q) (F ⋙ W.Q)
    (liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) (𝟭 W.Localization) (lift (W := W) G hG W.Q ⋙ F ⋙ W.Q)
      (W.Q.leftUnitor.symm ≪≫ asIso (whiskerRight adj.unit W.Q)))
    (F.associator W.Q (lift (W := W) G hG W.Q) ≪≫ F.isoWhiskerLeft (fac (W := W) G hG W.Q) ≪≫ asIso adj.counit)
⊢ G.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G)

Tactic:
apply Functor.IsLocalization.of_equivalence_target W.Q W G e
    (Localization.fac G hG W.Q)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.fac, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
rw : F.op.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₁ᵒᵖ) F.op)
⊢ F.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₁) F)

Tactic:
rw [← Functor.IsLocalization.op_iff, MorphismProperty.op_inverseImage,
    MorphismProperty.op_isomorphisms]

Premises used: CategoryTheory.MorphismProperty.op_isomorphisms, CategoryTheory.Functor.IsLocalization.op_iff, CategoryTheory.MorphismProperty.op_inverseImage
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
⊢ F.op.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₁ᵒᵖ) F.op)

Tactic:
adj.op.isLocalization

Premises used: CategoryTheory.Adjunction.op, CategoryTheory.Adjunction.isLocalization
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
⊢ F.op.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₁ᵒᵖ) F.op)

Tactic:
exact adj.op.isLocalization

Premises used: CategoryTheory.Adjunction.op, CategoryTheory.Adjunction.isLocalization
-- Module: Mathlib.CategoryTheory.Localization.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
inst_4 : Category.{v_5, u_5} E
F : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ E
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
hF : W₁.IsInvertedBy₂ W₂ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
inst_7 : W₁.ContainsIdentities
inst_8 : W₂.ContainsIdentities
X₁ : C₁
X₂ : C₂
⊢ Eq (α :=
    ((obj (obj (obj (whiskeringLeft₂ E) L₁) L₂) (lift₂ F (W₁ := W₁) (W₂ := W₂) hF L₁ L₂)).obj X₁).obj X₂ ⟶
      (F.obj X₁).obj X₂)
    (NatTrans.app (NatTrans.app (Iso.hom (Lifting₂.iso L₁ L₂ W₁ W₂ F (lift₂ F (W₁ := W₁) (W₂ := W₂) hF L₁ L₂))) X₁) X₂)
    (NatTrans.app (Iso.hom (Lifting.iso L₂ W₂ (F.obj X₁) ((lift₂ F (W₁ := W₁) (W₂ := W₂) hF L₁ L₂).obj (L₁.obj X₁))))
      X₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Localization.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
inst_4 : Category.{v_5, u_5} E
F : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ E
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
hF : W₁.IsInvertedBy₂ W₂ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
inst_7 : W₁.ContainsIdentities
inst_8 : W₂.ContainsIdentities
X₁ : C₁
X₂ : C₂
⊢ Eq (α :=
    ((obj (obj (obj (whiskeringLeft₂ E) L₁) L₂) (lift₂ F (W₁ := W₁) (W₂ := W₂) hF L₁ L₂)).obj X₁).obj X₂ ⟶
      (F.obj X₁).obj X₂)
    (NatTrans.app (NatTrans.app (Iso.hom (Lifting₂.iso L₁ L₂ W₁ W₂ F (lift₂ F (W₁ := W₁) (W₂ := W₂) hF L₁ L₂))) X₁) X₂)
    (NatTrans.app
      (Iso.hom (Lifting.iso L₁ W₁ (F.flip.obj X₂) ((lift₂ F (W₁ := W₁) (W₂ := W₂) hF L₁ L₂).flip.obj (L₂.obj X₂)))) X₁)

Tactic:
rfl

Premises used: rfl