awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
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 : Y ⟶ X
hf : W f
rw :
  ((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)
        (isoOfHom L₁ W f hf).inv ≫
      (isoOfHom L₂ W f hf).hom =
    (isoOfHom L₂ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom
rw₁ :
  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 Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        (isoOfHom L₂ W f hf).hom :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₂ :
  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 Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        L₂.map f :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₃ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (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)
          (isoOfHom L₁ W f hf).inv)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj Y ⟶ L₁.obj X) (L₂.obj Y ⟶ L₂.obj X)) :
            (a : L₁.obj Y ⟶ L₁.obj X) → L₂.obj Y ⟶ L₂.obj X)
          (L₁.map f)) :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₄ :
  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)
        ((isoOfHom L₁ W f hf).inv ≫ L₁.map f) :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₅ :
  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)
⊢ ((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)
      (isoOfHom L₁ W f hf).inv =
    (isoOfHom L₂ W f hf).inv
have rw₆ : Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X) (𝟙 (L₂.obj X)) (𝟙 (L₂.obj X))
Tactic: rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
    ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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
⊢ Functor.Linear R L
have map_smul : autoParam (∀ {X Y : C} (f : X ⟶ Y) (r : R), L.map (r • f) = r • L.map f) Functor.Linear.map_smul._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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) = r • L.map f
have 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
Tactic: change L.map (r • f) = ((Linear.toCatCenter R C r).localization L W).app (L.obj X) ≫ L.map f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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
⊢ Functor.Linear R F ↔ Functor.Linear R G
have mp : Functor.Linear R F → Functor.Linear R G
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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
⊢ Functor.Linear R F ↔ Functor.Linear R G
have mpr : Functor.Linear R G → Functor.Linear R F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (hypothesis)
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 G
have this : Functor.Linear R (L ⋙ G)
Tactic: have : (L ⋙ G).Linear R := Functor.linear_of_iso _ (Lifting.iso L W F G).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (hypothesis)
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)
⊢ Functor.Linear R G
have this₁ : L.EssSurj
Tactic: have := Localization.essSurj L W
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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
⊢ Functor.Linear R G
have 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))
Tactic: rw [Functor.linear_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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
⊢ G.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
have 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))
Tactic: have e := L.objObjPreimageIso X
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (hypothesis)
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
⊢ G.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
have 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
Tactic: have : r • 𝟙 X = e.inv ≫ (r • 𝟙 _) ≫ e.hom := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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
⊢ G.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := G.obj X ⟶ G.obj X) r (𝟙 (G.obj X))
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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
⊢ 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))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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
⊢ 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))
have mp : r • G.map e.inv ≫ 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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))
⊢ 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))
have mp₁ : r • G.map (e.inv ≫ 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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))
⊢ 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))
have mp₂ : r • G.map (𝟙 X) = 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Linear (goal)
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))
⊢ 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))
have 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))
Tactic: rw [Category.id_comp, ← G.map_comp, e.inv_hom_id, G.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
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
⊢ W₁ ≤ W₂.inverseImage F
have rw : W₂.inverseImage F ≤ W₂.inverseImage F
Tactic: rw [hW]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
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₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
h : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
inst_6 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
⊢ G.IsEquivalence
have rw : (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence
Tactic: rw [Φ.isEquivalence_iff L₁ L₂ G W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (hypothesis)
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₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G_1 : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
G : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
this : CatCommSq (Φ.op (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.op) (W₂ := W₂.op)) W₁.Q.op W₂.Q.op G.op :=
  { iso := NatIso.op (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G).symm }
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsLocalizedEquivalence (W₁ := W₁.op) (W₂ := W₂.op)
have this₁ : G.IsEquivalence
Tactic: have := Φ.isEquivalence W₁.Q W₂.Q G
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_3 : L₂.IsLocalization W₂
inst_4 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).IsLocalization W₁
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
have have : ∀ (this : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) L₂ (𝟭 D₂)),
  Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
Tactic: have : CatCommSq Φ.functor (Φ.functor ⋙ L₂) L₂ (𝟭 D₂) :=
    CatCommSq.mk (rightUnitor _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).IsLocalization W₁
have refine : W₂ ≤ W₁.isoClosure.inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.symm.functor
Tactic: refine Functor.IsLocalization.of_equivalence_source W₂.Q W₂ (Φ.functor ⋙ W₂.Q) W₁
      (asEquivalence Φ.functor).symm ?_ (Φ.inverts W₂.Q)
      ((associator _ _ _).symm ≪≫ isoWhiskerRight ((Equivalence.unitIso _).symm) _ ≪≫
        leftUnitor _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
⊢ W₂ ≤ W₁.isoClosure.inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.symm.functor
have erw : W₂ ≤ W₁.isoClosure.map Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.functor
Tactic: erw [W₁.isoClosure.inverseImage_equivalence_functor_eq_map_inverse]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
⊢ W₂ ≤ W₁.isoClosure.map Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.functor
have rw : W₂ ≤ W₁.map Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.functor
Tactic: rw [MorphismProperty.map_isoClosure]