awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
g : L₂.obj X ⟶ L₂.obj Y
⊢ Eq.{v_5 + 1} (α := L₁.obj X ⟶ L₁.obj Y)
    (((Equiv.symm (homEquiv W L₁ L₂) : Equiv.{v_6 + 1, v_5 + 1} (L₂.obj X ⟶ L₂.obj Y) (L₁.obj X ⟶ L₁.obj Y)) :
          (a : L₂.obj X ⟶ L₂.obj Y) → L₁.obj X ⟶ L₁.obj Y)
        g :
      L₁.obj X ⟶ L₁.obj Y)
    (((homEquiv W L₂ L₁ : Equiv.{v_6 + 1, v_5 + 1} (L₂.obj X ⟶ L₂.obj Y) (L₁.obj X ⟶ L₁.obj Y)) :
          (a : L₂.obj X ⟶ L₂.obj Y) → L₁.obj X ⟶ L₁.obj Y)
        g :
      L₁.obj X ⟶ L₁.obj Y)

Tactic:
rfl

Premises used: CategoryTheory.LocalizerMorphism.homMap, rfl
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂
e : L₁ ⋙ G ≅ L₂
f : L₁.obj X ⟶ L₁.obj Y
rw : (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
rw₁ : e.symm.hom.app X ≫ G.map f ≫ e.symm.inv.app Y = e.inv.app X ≫ G.map f ≫ e.hom.app Y
rw₂ : e.inv.app X ≫ G.map f ≫ e.symm.inv.app Y = e.inv.app X ≫ G.map f ≫ e.hom.app Y
rw₃ rw₄ : e.inv.app X ≫ G.map f ≫ e.hom.app Y = e.inv.app X ≫ G.map f ≫ e.hom.app Y
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      f =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
rw [homEquiv_apply, LocalizerMorphism.homMap_apply (LocalizerMorphism.id W) L₁ L₂ G e.symm,
    Iso.symm_hom, Iso.symm_inv]

Premises used: CategoryTheory.Iso.symm_hom, CategoryTheory.LocalizerMorphism.homMap_apply, CategoryTheory.Iso.symm_inv, CategoryTheory.Localization.homEquiv_apply, CategoryTheory.LocalizerMorphism.id, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
D₁ : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_2 : L₁.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (homEquiv W L₁ L₁ : (a : L₁.obj X ⟶ L₁.obj Y) → L₁.obj X ⟶ L₁.obj Y) f = f

Tactic:
apply LocalizerMorphism.id_homMap

Premises used: CategoryTheory.LocalizerMorphism.id_homMap
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
inst_3 : Category.{v_7, u_7} D₃
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_4 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_5 : L₂.IsLocalization W
L₃ : Functor.{v_1, v_7, u_1, u_7} C D₃
inst_6 : L₃.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
dsimp :
  (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₂ L₃
      ((LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f) =
    (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₃ f
⊢ Eq.{v_7 + 1} (α := L₃.obj X ⟶ L₃.obj Y)
    (((homEquiv W L₂ L₃ : Equiv.{v_6 + 1, v_7 + 1} (L₂.obj X ⟶ L₂.obj Y) (L₃.obj X ⟶ L₃.obj Y)) :
          (a : L₂.obj X ⟶ L₂.obj Y) → L₃.obj X ⟶ L₃.obj Y)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          f) :
      L₃.obj X ⟶ L₃.obj Y)
    (((homEquiv W L₁ L₃ : Equiv.{v_5 + 1, v_7 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₃.obj X ⟶ L₃.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₃.obj X ⟶ L₃.obj Y)
        f :
      L₃.obj X ⟶ L₃.obj Y)

Tactic:
dsimp only [homEquiv_apply]

Premises used: CategoryTheory.Localization.homEquiv_apply
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
inst_3 : Category.{v_7, u_7} D₃
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_4 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_5 : L₂.IsLocalization W
L₃ : Functor.{v_1, v_7, u_1, u_7} C D₃
inst_6 : L₃.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₂ L₃
      ((LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f) =
    (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₃ f

Tactic:
apply LocalizerMorphism.homMap_homMap

Premises used: CategoryTheory.LocalizerMorphism.homMap_homMap
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y Z : C
f : L₁.obj X ⟶ L₁.obj Y
g : L₁.obj Y ⟶ L₁.obj Z
⊢ Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj Z)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Z) (L₂.obj X ⟶ L₂.obj Z)) :
          (a : L₁.obj X ⟶ L₁.obj Z) → L₂.obj X ⟶ L₂.obj Z)
        (f ≫ g) :
      L₂.obj X ⟶ L₂.obj Z)
    (CategoryStruct.comp (Y := L₂.obj Y)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          f)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj Y ⟶ L₁.obj Z) (L₂.obj Y ⟶ L₂.obj Z)) :
            (a : L₁.obj Y ⟶ L₁.obj Z) → L₂.obj Y ⟶ L₂.obj Z)
          g) :
      L₂.obj X ⟶ L₂.obj Z)

Tactic:
apply LocalizerMorphism.homMap_comp

Premises used: CategoryTheory.LocalizerMorphism.homMap_comp
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
f : X ⟶ Y
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      (L₁.map f) =
    L₂.map f

Tactic:
simp [homEquiv_apply]

Premises used: CategoryTheory.Localization.homEquiv_apply
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X : C
⊢ Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj X) (L₂.obj X ⟶ L₂.obj X)) :
          (a : L₁.obj X ⟶ L₁.obj X) → L₂.obj X ⟶ L₂.obj X)
        (𝟙 (L₁.obj X)) :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)

Tactic:
simp [homEquiv_apply]

Premises used: CategoryTheory.Localization.homEquiv_apply
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
R : Type w
inst : Ring R
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₁, u₁} C
inst_4 : Preadditive.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : L.Additive
inst_7 : Linear.{w, v₁, u₁} R C
this : Linear.{w, v₂, u₂} R D := linear R L W
map_smul : autoParam (∀ {X Y : C} (f : X ⟶ Y) (r : R), L.map (r • f) = r • L.map f) Functor.Linear.map_smul._autoParam
⊢ Functor.Linear R L

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
R : Type w
inst : Ring R
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₁, u₁} C
inst_4 : Preadditive.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : L.Additive
inst_7 : Linear.{w, v₁, u₁} R C
this : Linear.{w, v₂, u₂} R D := linear R L W
X Y : C
f : X ⟶ Y
r : R
map_smul :
  L.map (r • f) =
    (CatCenter.localization ((Linear.toCatCenter R C : (a : R) → CatCenter C) r) L W).app (L.obj X) ≫ L.map f
⊢ L.map (r • f) = r • L.map f

Tactic:
change L.map (r • f) = ((Linear.toCatCenter R C r).localization L W).app (L.obj X) ≫ L.map f

Premises used: CategoryTheory.Functor.map, CategoryTheory.CatCenter.localization, HSMul.hSMul, CategoryTheory.Linear.toCatCenter, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.CatCenter.app
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
R : Type w
inst : Ring R
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₁, u₁} C
inst_4 : Preadditive.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : L.Additive
inst_7 : Linear.{w, v₁, u₁} R C
this : Linear.{w, v₂, u₂} R D := linear R L W
X Y : C
f : X ⟶ Y
r : R
⊢ L.map (r • f) =
    (CatCenter.localization ((Linear.toCatCenter R C : (a : R) → CatCenter C) r) L W).app (L.obj X) ≫ L.map f

Tactic:
simp [← L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
R : Type w
inst : Ring R
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₁, u₁} C
inst_4 : Preadditive.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : L.Additive
inst_7 : Linear.{w, v₁, u₁} R C
inst_8 : Preadditive W.Localization
inst_9 : W.Q.Additive
⊢ Functor.Linear R W.Q

Tactic:
Localization.functor_linear R W.Q W

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.functor_linear
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
R : Type w
inst : Ring R
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₁, u₁} C
inst_4 : Preadditive.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : L.Additive
inst_7 : Linear.{w, v₁, u₁} R C
inst_8 : MorphismProperty.HasLocalization.{u_1, v₁, u₁} W
inst_9 : Preadditive.{u_1, u₁} (MorphismProperty.Localization'.{u_1, v₁, u₁} W)
inst_10 : Functor.Additive.{v₁, u₁, u_1, u₁} (D := MorphismProperty.Localization'.{u_1, v₁, u₁} W) W.Q'
⊢ Functor.Linear.{w, v₁, u₁, u_1, u₁} R (D := MorphismProperty.Localization'.{u_1, v₁, u₁} W) W.Q'

Tactic:
Localization.functor_linear R W.Q' W

Premises used: CategoryTheory.Localization.functor_linear, CategoryTheory.MorphismProperty.Q'
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
mp : Functor.Linear R F → Functor.Linear R G
mpr : Functor.Linear R G → Functor.Linear R F
⊢ Functor.Linear R F ↔ Functor.Linear R G

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R F
⊢ Functor.Linear R (L ⋙ G)

Tactic:
have : (L ⋙ G).Linear R := Functor.linear_of_iso _ (Lifting.iso L W F G).symm
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R F
this : Functor.Linear R (L ⋙ G)
⊢ L.EssSurj

Tactic:
have := Localization.essSurj L W
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R F
this_1 : Functor.Linear R (L ⋙ G)
this : L.EssSurj
mp : ∀ (X : D) (r : R), G.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
⊢ Functor.Linear R G

Tactic:
rw [Functor.linear_iff]

Premises used: CategoryTheory.Functor.linear_iff
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R F
this_1 : Functor.Linear R (L ⋙ G)
this : L.EssSurj
X : D
r : R
mp :
  ∀ (e : L.obj (L.objPreimage X) ≅ X),
    G.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
⊢ G.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))

Tactic:
have e := L.objObjPreimageIso X
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R F
this_1 : Functor.Linear R (L ⋙ G)
this : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
⊢ HSMul.hSMul (β := X ⟶ X) r (𝟙 X) =
    e.inv ≫ HSMul.hSMul (β := L.obj (L.objPreimage X) ⟶ L.obj (L.objPreimage X)) r (𝟙 (L.obj (L.objPreimage X))) ≫ e.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R F
this_1 : Functor.Linear R (L ⋙ G)
this : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
⊢ HSMul.hSMul (β := X ⟶ X) r (𝟙 X) =
    e.inv ≫ HSMul.hSMul (β := L.obj (L.objPreimage X) ⟶ L.obj (L.objPreimage X)) r (𝟙 (L.obj (L.objPreimage X))) ≫ e.hom

Tactic:
have : r • 𝟙 X = e.inv ≫ (r • 𝟙 _) ≫ e.hom := by simp
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R F
this_1 : Functor.Linear R (L ⋙ G)
this_2 : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this :
  HSMul.hSMul (β := X ⟶ X) r (𝟙 X) =
    e.inv ≫ HSMul.hSMul (β := L.obj (L.objPreimage X) ⟶ L.obj (L.objPreimage X)) r (𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
mp :
  r • G.map e.inv ≫ 𝟙 ((L ⋙ G).obj (L.objPreimage X)) ≫ G.map e.hom =
    HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
⊢ G.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))

Tactic:
rw [this, G.map_comp, G.map_comp, ← L.map_id, ← L.map_smul, ← Functor.comp_map,
      (L ⋙ G).map_smul, Functor.map_id, Linear.smul_comp, Linear.comp_smul]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.map_smul, CategoryTheory.Linear.comp_smul, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R F
this_1 : Functor.Linear R (L ⋙ G)
this_2 : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this :
  HSMul.hSMul (β := X ⟶ X) r (𝟙 X) =
    e.inv ≫ HSMul.hSMul (β := L.obj (L.objPreimage X) ⟶ L.obj (L.objPreimage X)) r (𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
mp :
  r • G.map e.inv ≫ 𝟙 (G.obj (L.obj (L.objPreimage X))) ≫ G.map e.hom =
    HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
⊢ r • G.map e.inv ≫ 𝟙 ((L ⋙ G).obj (L.objPreimage X)) ≫ G.map e.hom =
    HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R F
this_1 : Functor.Linear R (L ⋙ G)
this_2 : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this :
  HSMul.hSMul (β := X ⟶ X) r (𝟙 X) =
    e.inv ≫ HSMul.hSMul (β := L.obj (L.objPreimage X) ⟶ L.obj (L.objPreimage X)) r (𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
mp : r • G.map e.inv ≫ G.map e.hom = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
mp₁ : r • G.map (e.inv ≫ e.hom) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
mp₂ : r • G.map (𝟙 X) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
mp₃ mp₄ : HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X)) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
⊢ r • G.map e.inv ≫ 𝟙 (G.obj (L.obj (L.objPreimage X))) ≫ G.map e.hom =
    HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))

Tactic:
rw [Category.id_comp, ← G.map_comp, e.inv_hom_id, G.map_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R G
⊢ Functor.Linear R F

Tactic:
Functor.linear_of_iso _ (Lifting.iso L W F G)

Premises used: CategoryTheory.Localization.Lifting.iso, CategoryTheory.Functor.linear_of_iso
-- Module: Mathlib.CategoryTheory.Localization.Linear
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
E : Type u_1
inst_4 : Category.{v_1, u_1} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_5 : L.IsLocalization W
inst_6 : Preadditive.{v_1, u_1} E
R : Type u_2
inst_7 : Ring R
inst_8 : Linear.{u_2, v₁, u₁} R C
inst_9 : Linear.{u_2, v₂, u₂} R D
inst_10 : Linear.{u_2, v_1, u_1} R E
inst_11 : Functor.Linear R L
F : Functor.{v₁, v_1, u₁, u_1} C E
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_12 : Lifting L W F G
h : Functor.Linear R G
⊢ Functor.Linear R F

Tactic:
exact Functor.linear_of_iso _ (Lifting.iso L W F G)

Premises used: CategoryTheory.Localization.Lifting.iso, CategoryTheory.Functor.linear_of_iso
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
hW : W₁ = W₂.inverseImage F
rw rw₁ : W₂.inverseImage F ≤ W₂.inverseImage F
⊢ W₁ ≤ W₂.inverseImage F

Tactic:
rw [hW]