awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
refine_1 :
  (MorphismProperty.pi (C := fun (i : J) ↦ C) fun (x : J) ↦ W) ≤
    MorphismProperty.inverseImage (MorphismProperty.isoClosure (W.functorCategory (Discrete J))) E.functor
refine_2 : MorphismProperty.IsInvertedBy (W.functorCategory (Discrete J)) L₂
⊢ IsLocalization (C := Functor.{0, v₁, 0, u₁} (Discrete J) C) (obj (whiskeringRight (Discrete J) C D) L)
    (W.functorCategory (Discrete J))

Tactic:
refine Functor.IsLocalization.of_equivalences L₁
    (MorphismProperty.pi (fun _ => W)) L₂ _ E E' ?_ ?_

Premises used: CategoryTheory.MorphismProperty.pi, CategoryTheory.Functor.IsLocalization.of_equivalences
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
X Y : (i : J) → C
f : X ⟶ Y
hf : MorphismProperty.pi (C := fun (i : J) ↦ C) (fun (x : J) ↦ W) f
⊢ MorphismProperty.inverseImage (MorphismProperty.isoClosure (W.functorCategory (Discrete J))) E.functor f

Tactic:
MorphismProperty.le_isoClosure _ _ (fun ⟨j⟩ => hf j)

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map, _private.0.CategoryTheory.Functor.IsLocalization.instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities.match_1, CategoryTheory.MorphismProperty.isoClosure, CategoryTheory.MorphismProperty.le_isoClosure, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
X Y : (i : J) → C
f : X ⟶ Y
hf : MorphismProperty.pi (C := fun (i : J) ↦ C) (fun (x : J) ↦ W) f
⊢ MorphismProperty.inverseImage (MorphismProperty.isoClosure (W.functorCategory (Discrete J))) E.functor f

Tactic:
exact MorphismProperty.le_isoClosure _ _ (fun ⟨j⟩ => hf j)

Premises used: CategoryTheory.MorphismProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
X Y : Functor.{0, v₁, 0, u₁} (Discrete J) C
f : X ⟶ Y
hf : W.functorCategory (Discrete J) f
⊢ ∀ (j : Discrete J), IsIso ((L₂.map f).app j)

Tactic:
have : ∀ (j : Discrete J), IsIso ((L₂.map f).app j) :=
      fun j => Localization.inverts L W _ (hf j)
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
this_1 : CatCommSq E.functor L₁ L₂ E'.functor
X Y : Functor.{0, v₁, 0, u₁} (Discrete J) C
f : X ⟶ Y
hf : W.functorCategory (Discrete J) f
this : ∀ (j : Discrete J), IsIso ((L₂.map f).app j)
⊢ IsIso (L₂.map f)

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Localization.Preadditive
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
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_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₂'
inst_6 : HasZeroMorphisms.{v_3, u_3} E
⊢ ∀ (X : C), (liftNatTrans L W F₁ F₂ F₁' F₂' 0).app (L.obj X) = NatTrans.app 0 (L.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Preadditive
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
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
inst_4 : Preadditive.{v_3, u_3} E
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_5 : Lifting L W F₁ F₁'
inst_6 : Lifting L W F₂ F₂'
τ τ' : F₁ ⟶ F₂
⊢ ∀ (X : C),
    Eq (α := F₁'.obj (L.obj X) ⟶ F₂'.obj (L.obj X)) ((liftNatTrans L W F₁ F₂ F₁' F₂' (τ + τ')).app (L.obj X))
      ((liftNatTrans L W F₁ F₂ F₁' F₂' τ + liftNatTrans L W F₁ F₂ F₁' F₂' τ').app (L.obj X))

Tactic:
simp
-- 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
this : Localization.Construction.lift (W := W) W.Q ⋯ = 𝟭 W.Localization
rw : IsEquivalence (C := W.Localization) (𝟭 W.Localization)
⊢ (Localization.Construction.lift (W := W) W.Q ⋯).IsEquivalence

Tactic:
rw [this]
-- 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
this : Localization.Construction.lift (W := W) W.Q ⋯ = 𝟭 W.Localization
⊢ IsEquivalence (C := W.Localization) (𝟭 W.Localization)

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
suffices : Localization.Construction.lift (W := W) W.Q ⋯ = 𝟭 W.Localization
⊢ (Localization.Construction.lift (W := W) W.Q ⋯).IsEquivalence

Tactic:
suffices Localization.Construction.lift W.Q W.Q_inverts = 𝟭 _ by
      rw [this]
      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
h : W.Q ⋙ Localization.Construction.lift (W := W) W.Q ⋯ = W.Q ⋙ 𝟭 W.Localization
⊢ Localization.Construction.lift (W := W) W.Q ⋯ = 𝟭 W.Localization

Tactic:
apply Localization.Construction.uniq

Premises used: CategoryTheory.Localization.Construction.uniq
-- 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
h : W.Q = W.Q ⋙ 𝟭 W.Localization
⊢ W.Q ⋙ Localization.Construction.lift (W := W) W.Q ⋯ = W.Q ⋙ 𝟭 W.Localization

Tactic:
simp only [Localization.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
⊢ W.Q = W.Q ⋙ 𝟭 W.Localization

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
hW : W ≤ MorphismProperty.isomorphisms C
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
mk :
  ∀ (obj : C → E) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    (hF :
      W.IsInvertedBy
        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E }),
    𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp }
⊢ 𝟭 C ⋙ F = F

Tactic:
cases F
-- 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
hW : W ≤ MorphismProperty.isomorphisms C
obj : C → E
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
hF :
  W.IsInvertedBy { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E }
⊢ 𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp }

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
hW : W ≤ MorphismProperty.isomorphisms C
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C E
eq : 𝟭 C ⋙ F₁ = 𝟭 C ⋙ F₂
mk :
  ∀ (obj : C → E) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    (eq :
      𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
        𝟭 C ⋙ F₂),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } = F₂
⊢ F₁ = F₂

Tactic:
cases F₁
-- 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
hW : W ≤ MorphismProperty.isomorphisms C
F₂ : Functor.{v_1, v_3, u_1, u_3} C E
obj : C → E
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
eq :
  𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
    𝟭 C ⋙ F₂
mk :
  ∀ (obj_1 : C → E) (map_1 : {X Y : C} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y))
    (map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (obj_1 X))
    (map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g)
    (eq :
      𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
        𝟭 C ⋙
          { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 :
            Functor.{v_1, v_3, u_1, u_3} C E }),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
      { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } = F₂

Tactic:
cases F₂
-- 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
hW : W ≤ MorphismProperty.isomorphisms C
obj : C → E
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
obj_1 : C → E
map_1 : {X Y : C} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y)
map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (obj_1 X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
eq :
  𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
    𝟭 C ⋙
      { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v_1, v_3, u_1, u_3} C E }
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
    { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }

Tactic:
eq

Premises used: CategoryTheory.Functor.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
hW : W ≤ MorphismProperty.isomorphisms C
obj : C → E
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
obj_1 : C → E
map_1 : {X Y : C} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y)
map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (obj_1 X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
eq :
  𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
    𝟭 C ⋙
      { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v_1, v_3, u_1, u_3} C E }
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
    { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }

Tactic:
exact eq
-- 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
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization
⊢ W.Q ⋙ 𝟭 W.Localization = W.Q ⋙ Localization.Construction.lift (W := W) L ⋯ ⋙ h₂.lift (W := W) W.Q ⋯

Tactic:
simp only [← Functor.assoc, Localization.Construction.fac, h₂.fac, Functor.comp_id]

Premises used: CategoryTheory.Functor.assoc, CategoryTheory.Functor.comp_id, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac, 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
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization
⊢ L ⋙ h₂.lift (W := W) W.Q ⋯ ⋙ Localization.Construction.lift (W := W) L ⋯ = L ⋙ 𝟭 D

Tactic:
simp only [← Functor.assoc, h₂.fac, Localization.Construction.fac, Functor.comp_id]

Premises used: CategoryTheory.Functor.assoc, CategoryTheory.Functor.comp_id, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac, CategoryTheory.Localization.Construction.fac
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W ≤ MorphismProperty.isomorphisms C
⊢ IsLocalization (𝟭 C) W

Tactic:
IsLocalization.mk' _ _ (Localization.strictUniversalPropertyFixedTargetId W _ hW)
    (Localization.strictUniversalPropertyFixedTargetId W _ hW)

Premises used: CategoryTheory.Functor.IsLocalization.mk', CategoryTheory.Localization.strictUniversalPropertyFixedTargetId
-- 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
⊢ W.IsInvertedBy L

Tactic:
(inferInstance : L.IsLocalization W).inverts

Premises used: CategoryTheory.Functor.IsLocalization.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
inst_2 : L.IsLocalization W
X Y : C
f : X ⟶ Y
hf : W f
⊢ L.map f ≫ (isoOfHom L W f hf).inv = 𝟙 (L.obj X)

Tactic:
(isoOfHom L W f hf).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Localization.isoOfHom
-- 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
X Y : C
f : X ⟶ Y
hf : W f
⊢ (isoOfHom L W f hf).inv ≫ L.map f = 𝟙 (L.obj Y)

Tactic:
(isoOfHom L W f hf).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Localization.isoOfHom
-- 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
X : C
hX : W (𝟙 X)
rw : (isoOfHom L W (𝟙 X) hX).inv ≫ (isoOfHom L W (𝟙 X) hX).hom = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
rw₁ : 𝟙 (L.obj X) = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
rw₂ : 𝟙 (L.obj X) = (isoOfHom L W (𝟙 X) hX).hom
rw₃ : 𝟙 (L.obj X) = L.map (𝟙 X)
rw₄ rw₅ : Eq.{v_2 + 1} (α := L.obj X ⟶ L.obj X) (𝟙 (L.obj X)) (𝟙 (L.obj X))
⊢ (isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)

Tactic:
rw [← cancel_mono (isoOfHom L W (𝟙 X) hX).hom, Iso.inv_hom_id, id_comp,
    isoOfHom_hom, Functor.map_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.CategoryStruct.id, CategoryTheory.Localization.isoOfHom_hom, CategoryTheory.cancel_mono, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.map_id, CategoryTheory.Iso.hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : W f
w : (wIso (W := W) f hf).hom = (isoOfHom W.Q W f hf).hom
⊢ wIso (W := W) f hf = isoOfHom W.Q W f hf

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : W f
⊢ (wIso (W := W) f hf).hom = (isoOfHom W.Q W f hf).hom

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : W f
⊢ wInv (W := W) f hf = (isoOfHom W.Q W f hf).inv

Tactic:
congr_arg Iso.inv (wIso_eq_isoOfHom f hf)

Premises used: congr_arg, CategoryTheory.Iso.inv, CategoryTheory.Localization.Construction.wIso_eq_isoOfHom
-- 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
⊢ (Construction.lift (W := W) L ⋯).IsEquivalence

Tactic:
(inferInstance : L.IsLocalization W).isEquivalence

Premises used: CategoryTheory.Functor.IsLocalization.isEquivalence
-- 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
⊢ L.EssSurj

Tactic:
⟨fun X =>
    ⟨(Construction.objEquiv W).invFun ((equivalenceFromModel L W).inverse.obj X),
      Nonempty.intro
        ((qCompEquivalenceFromModelFunctorIso L W).symm.app _ ≪≫
          (equivalenceFromModel L W).counitIso.app X)⟩⟩

Premises used: CategoryTheory.Functor.EssSurj.mk, Nonempty.intro, CategoryTheory.Iso.trans, CategoryTheory.Localization.equivalenceFromModel, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Localization.Construction.objEquiv, CategoryTheory.Localization.qCompEquivalenceFromModelFunctorIso, CategoryTheory.Functor.obj, Equiv.invFun, CategoryTheory.Equivalence.counitIso, CategoryTheory.Equivalence.inverse
-- 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 :
  (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)
⊢ obj
      (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
        Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
      F =
    obj (whiskeringLeftFunctor L W E) F

Tactic:
ext