awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y : C₁
φ : W.RightFraction X Y
obtain :
  ∀ (T : C₁) (s : T ⟶ X) (w : W s) (f : T ⟶ Y),
    ∃ (ψ : W.LeftFraction X Y),
      (RightFraction.mk (W := W) s w f).f (W := W) ≫ ψ.s (W := W) =
        (RightFraction.mk (W := W) s w f).s (W := W) ≫ ψ.f (W := W)
⊢ ∃ (ψ : W.LeftFraction X Y), φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W)

Tactic:
obtain ⟨T, s, _, f, rfl⟩ := φ.cases

Premises used: CategoryTheory.MorphismProperty.RightFraction.cases, rfl
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
dsimp : ∃ (ψ : W.LeftFraction X Y), f ≫ ψ.s (W := W) = s ≫ ψ.f (W := W)
⊢ ∃ (ψ : W.LeftFraction X Y),
    (RightFraction.mk (W := W) s w f).f (W := W) ≫ ψ.s (W := W) =
      (RightFraction.mk (W := W) s w f).s (W := W) ≫ ψ.f (W := W)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
⊢ W s

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
⊢ IsIso (G.map s)

Tactic:
have := hW s (by assumption)
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this : IsIso (G.map s)
⊢ Functor.map (𝟭 C₁) s ≫ adj.unit.app X = adj.unit.app T ≫ (G ⋙ F).map s

Tactic:
have := adj.unit.naturality s
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this_1 : IsIso (G.map s)
this : Functor.map (𝟭 C₁) s ≫ adj.unit.app X = adj.unit.app T ≫ (G ⋙ F).map s
dsimp : f ≫ adj.unit.app Y = s ≫ adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
⊢ f ≫
      (LeftFraction.mk (W := W) (adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)) (adj.unit.app Y) ⋯).s (W :=
        W) =
    s ≫
      (LeftFraction.mk (W := W) (adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)) (adj.unit.app Y) ⋯).f (W :=
        W)

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this_1 : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
rw : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
rw₁ : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ inv (F.map (G.map s)) ≫ F.map (G.map f)
rw₂ : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map f)
rw₃ rw₄ : f ≫ adj.unit.app Y = f ≫ adj.unit.app Y
⊢ f ≫ adj.unit.app Y = s ≫ adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)

Tactic:
rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]

Premises used: CategoryTheory.Functor.map_inv, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.Adjunction.unit_naturality
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this : IsIso (G.map s)
⊢ ∃ (ψ : W.LeftFraction X Y), f ≫ ψ.s (W := W) = s ≫ ψ.f (W := W)

Tactic:
exact ⟨{
      f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
      s := adj.unit.app Y
      hs := hW' Y}, by
      have := adj.unit.naturality s
      dsimp at this ⊢
      rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
⊢ W s

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
⊢ IsIso (G.map s)

Tactic:
have := hW s (by assumption)
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ ∃ (Y' : C₁) (t : Y ⟶ Y') (_ : W t), f₁ ≫ t = f₂ ≫ t

Tactic:
⟨_, adj.unit.app Y, hW' _, ?_⟩

Premises used: CategoryTheory.Adjunction.unit, Exists.intro, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
refine : f₁ ≫ adj.unit.app Y = f₂ ≫ adj.unit.app Y
⊢ ∃ (Y' : C₁) (t : Y ⟶ Y') (_ : W t), f₁ ≫ t = f₂ ≫ t

Tactic:
refine ⟨_, adj.unit.app Y, hW' _, ?_⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
rw : adj.unit.app X ≫ F.map (G.map f₁) = adj.unit.app X ≫ F.map (G.map f₂)
⊢ f₁ ≫ adj.unit.app Y = f₂ ≫ adj.unit.app Y

Tactic:
rw [← adj.unit_naturality f₁, ← adj.unit_naturality f₂]

Premises used: CategoryTheory.Adjunction.unit_naturality
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
e_a : G.map f₁ = G.map f₂
⊢ adj.unit.app X ≫ F.map (G.map f₁) = adj.unit.app X ≫ F.map (G.map f₂)

Tactic:
congr 2
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
e_a : G.map s ≫ G.map f₁ = G.map s ≫ G.map f₂
e_a₁ : G.map (s ≫ f₁) = G.map s ≫ G.map f₂
e_a₂ : G.map (s ≫ f₁) = G.map (s ≫ f₂)
e_a₃ e_a₄ : G.map (s ≫ f₂) = G.map (s ≫ f₂)
⊢ G.map f₁ = G.map f₂

Tactic:
rw [← cancel_epi (G.map s), ← G.map_comp, ← G.map_comp, h]

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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 : F ⊣ G
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.counit
⊢ W.HasRightCalculusOfFractions

Tactic:
have := hasLeftCalculusOfFractions adj.op W.op hW.op (fun _ ↦ hW' _)
  inferInstanceAs W.op.unop.HasRightCalculusOfFractions

Premises used: CategoryTheory.Adjunction.op, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.IsInvertedBy.op, CategoryTheory.Adjunction.hasLeftCalculusOfFractions, Opposite.unop, _private.0.CategoryTheory.Adjunction.hasRightCalculusOfFractions._proof_1
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift (W := W) G hW W.Q
⊢ W.Q ⋙ Φ ≅ G

Tactic:
apply Localization.fac

Premises used: CategoryTheory.Localization.fac
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift (W := W) G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac (W := W) G hW W.Q
rw : ∀ (X : C₁), IsIso ((Functor.whiskerRight adj.unit W.Q).app X)
⊢ IsIso (Functor.whiskerRight adj.unit W.Q)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift (W := W) G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac (W := W) G hW W.Q
X : C₁
⊢ IsIso ((Functor.whiskerRight adj.unit W.Q).app X)

Tactic:
Localization.inverts W.Q W _ (hW' X)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift (W := W) G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac (W := W) G hW W.Q
X : C₁
⊢ IsIso ((Functor.whiskerRight adj.unit W.Q).app X)

Tactic:
exact Localization.inverts W.Q W _ (hW' X)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift (W := W) G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac (W := W) G hW W.Q
⊢ IsIso (Functor.whiskerRight adj.unit W.Q)

Tactic:
have : IsIso (Functor.whiskerRight adj.unit W.Q) := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro X
    exact Localization.inverts W.Q W _ (hW' X)
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift (W := W) G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac (W := W) G hW W.Q
this : IsIso (Functor.whiskerRight adj.unit W.Q)
⊢ G.IsLocalization W

Tactic:
Functor.IsLocalization.of_equivalence_target W.Q W _
    (Equivalence.mk Φ (F ⋙ W.Q)
      (Localization.liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) _ _
        (W.Q.leftUnitor.symm ≪≫ asIso (Functor.whiskerRight adj.unit W.Q) ≪≫
        Functor.associator _ _ _))
      (Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ e ≪≫ asIso adj.counit)) e

Premises used: CategoryTheory.Localization.liftNatIso, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.associator, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.IsLocalization.of_equivalence_target, CategoryTheory.Equivalence.mk, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift (W := W) G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac (W := W) G hW W.Q
this : IsIso (Functor.whiskerRight adj.unit W.Q)
⊢ G.IsLocalization W

Tactic:
exact Functor.IsLocalization.of_equivalence_target W.Q W _
    (Equivalence.mk Φ (F ⋙ W.Q)
      (Localization.liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) _ _
        (W.Q.leftUnitor.symm ≪≫ asIso (Functor.whiskerRight adj.unit W.Q) ≪≫
        Functor.associator _ _ _))
      (Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ e ≪≫ asIso adj.counit)) e

Premises used: CategoryTheory.Localization.liftNatIso, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.associator, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.IsLocalization.of_equivalence_target, CategoryTheory.Equivalence.mk, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : F ⊣ G
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.counit
⊢ G.IsLocalization W

Tactic:
simpa using isLocalization_leftAdjoint adj.op W.op hW.op (fun X ↦ hW' X.unop)

Premises used: CategoryTheory.Adjunction.op, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.IsInvertedBy.op, CategoryTheory.Adjunction.isLocalization_leftAdjoint, Opposite.unop
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
j : C₁
simp : IsIso (G.map (adj.unit.app j))
⊢ inverseImage (isomorphisms C₂) G (adj.unit.app j)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, inverseImage_iff, isomorphisms.iff]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.Functor.id_obj, CategoryTheory.MorphismProperty.inverseImage_iff
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
j : C₁
⊢ IsIso (G.map (adj.unit.app j))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : F ⊣ G
j : C₁
simp : IsIso (G.map (adj.counit.app j))
⊢ inverseImage (isomorphisms C₂) G (adj.counit.app j)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, inverseImage_iff, isomorphisms.iff]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.Functor.id_obj, CategoryTheory.MorphismProperty.inverseImage_iff
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : F ⊣ G
j : C₁
⊢ IsIso (G.map (adj.counit.app j))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
⊢ G.IsLocalization (inverseImage (isomorphisms C₂) G)

Tactic:
adj.isLocalization_leftAdjoint _ (fun _ _ _ h ↦ h)
    adj.functorCategory_inverseImage_isomorphisms_unit

Premises used: CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_unit, CategoryTheory.Adjunction.isLocalization_leftAdjoint
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : F ⊣ G
⊢ G.IsLocalization (inverseImage (isomorphisms C₂) G)

Tactic:
adj.isLocalization_rightAdjoint _ (fun _ _ _ h ↦ h)
    adj.functorCategory_inverseImage_isomorphisms_counit

Premises used: CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_counit, CategoryTheory.Adjunction.isLocalization_rightAdjoint
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
⊢ (inverseImage (isomorphisms C₂) G).HasLeftCalculusOfFractions

Tactic:
hasLeftCalculusOfFractions adj _ (fun _ _ _ h ↦ h)
    adj.functorCategory_inverseImage_isomorphisms_unit

Premises used: CategoryTheory.Adjunction.hasLeftCalculusOfFractions, CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_unit
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
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₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : F ⊣ G
⊢ (inverseImage (isomorphisms C₂) G).HasRightCalculusOfFractions

Tactic:
hasRightCalculusOfFractions adj _ (fun _ _ _ h ↦ h)
    adj.functorCategory_inverseImage_isomorphisms_counit

Premises used: CategoryTheory.Adjunction.hasRightCalculusOfFractions, CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_counit
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
⊢ φ.symm (W := W).add (W := W) = φ.add (W := W)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : F.Additive
⊢ IsIso (F.map (φ.s (W := W)))

Tactic:
have := hF φ.s φ.hs