awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
h : ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
X Y : C
f : X ⟶ Y
r : R
this : r • f = HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f
mpr : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f) = r • F.map f
mpr₁ : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) ≫ F.map f = r • F.map f
⊢ F.map (r • f) = r • F.map f
have mpr₂ : HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X)) ≫ F.map f = r • F.map f
Tactic: rw [this, F.map_comp, h, Linear.smul_comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
h : ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
X Y : C
f : X ⟶ Y
r : R
this : r • f = HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f
mpr : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f) = r • F.map f
mpr₁ : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) ≫ F.map f = r • F.map f
mpr₂ : HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X)) ≫ F.map f = r • F.map f
⊢ F.map (r • f) = r • F.map f
have mpr₃ : r • 𝟙 (F.obj X) ≫ F.map f = r • F.map f
Tactic: rw [this, F.map_comp, h, Linear.smul_comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
h : ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
X Y : C
f : X ⟶ Y
r : R
this : r • f = HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f
mpr : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f) = r • F.map f
mpr₁ : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) ≫ F.map f = r • F.map f
mpr₂ : HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X)) ≫ F.map f = r • F.map f
mpr₃ : r • 𝟙 (F.obj X) ≫ F.map f = r • F.map f
⊢ F.map (r • f) = r • F.map f
have mpr₄ : r • F.map f = r • F.map f
Tactic: rw [this, F.map_comp, h, Linear.smul_comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
inst_13 : Linear R (F ⋙ G)
⊢ Linear R G
have refine : ∀ {X Y : D} (f : X ⟶ Y) (r : R), G.map (r • f) = r • G.map f
Tactic: refine ⟨fun {X Y} f r ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
inst_13 : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
⊢ ∃ (X' : C) (Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y) (f' : X' ⟶ Y'), f = eX.inv ≫ F.map f' ≫ eY.hom
have obtain : ∀ (f' : F.objPreimage X ⟶ F.objPreimage Y)
  (hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)),
  ∃ (X' : C) (Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y) (f' : X' ⟶ Y'), f = eX.inv ≫ F.map f' ≫ eY.hom
Tactic: obtain ⟨f', hf'⟩ :=
      F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
inst_13 : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
⊢ G.map (r • f) = r • G.map f
have obtain : ∀ (X' Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y) (f' : X' ⟶ Y'),
  G.map (r • eX.inv ≫ F.map f' ≫ eY.hom) = r • G.map (eX.inv ≫ F.map f' ≫ eY.hom)
Tactic: obtain ⟨X', Y', eX, eY, f', rfl⟩ :
      ∃ (X' Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y)
        (f' : X' ⟶ Y'), f = eX.inv ≫ F.map f' ≫ eY.hom := by
    obtain ⟨f', hf'⟩ :=
      F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
    exact ⟨_, _, F.objObjPreimageIso X, F.objObjPreimageIso Y, f', by cat_disch⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : Linear.{u_1, v_1, u_2} R C
inst_6 : Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
e : Equivalence.{v_1, v_2, u_2, u_3} C D
inst_7 : Functor.Linear R e.functor
X Y : D
r : X ⟶ Y
f : R
⊢ e.inverse.map (f • r) = f • e.inverse.map r
have a : e.functor.map (e.inverse.map (f • r)) = e.functor.map (f • e.inverse.map r)
Tactic: apply e.functor.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
⊢ whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
      (G'.associator F' G').hom ≫ G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F') =
    NatTrans.id (𝟭 D₁ ⋙ G')
have apply : ∀ (X : C₁),
  Eq (α := (𝟭 D₁ ⋙ G').obj (L₁.obj X) ⟶ (G' ⋙ 𝟭 D₂).obj (L₁.obj X))
    ((whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
          (G'.associator F' G').hom ≫ G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F')).app
      (L₁.obj X))
    ((NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X))
Tactic: apply natTrans_ext L₁ W₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ Eq (α := (𝟭 D₁ ⋙ G').obj (L₁.obj X₁) ⟶ (G' ⋙ 𝟭 D₂).obj (L₁.obj X₁))
    ((whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
          (G'.associator F' G').hom ≫ G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F')).app
      (L₁.obj X₁))
    ((NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁))
have eq : (whiskerRight adj.unit G ≫ G.whiskerLeft adj.counit).app X₁ = NatTrans.app (𝟙 (𝟭 C₁ ⋙ G)) X₁
Tactic: have eq := congr_app adj.left_triangle X₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ Eq (α := (𝟭 D₁ ⋙ G').obj (L₁.obj X₁) ⟶ (G' ⋙ 𝟭 D₂).obj (L₁.obj X₁))
    ((whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
          (G'.associator F' G').hom ≫ G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F')).app
      (L₁.obj X₁))
    ((NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁))
have rw : G'.map (L₁.map (adj.unit.app X₁)) ≫
    G'.map ((CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) ≫
      G'.map (F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)) ≫
        (Localization.η adj L₁ L₂ W₂ G' F').app (G'.obj (L₁.obj X₁)) =
  (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
Tactic: rw [NatTrans.comp_app, NatTrans.comp_app, whiskerRight_app, Localization.ε_app,
          Functor.associator_hom_app, id_comp, whiskerLeft_app, G'.map_comp, G'.map_comp,
          assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map (L₁.map (adj.unit.app X₁)) ≫
      G'.map ((CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) ≫
        G'.map (F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)) ≫
          (Localization.η adj L₁ L₂ W₂ G' F').app (G'.obj (L₁.obj X₁)) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
have erw : 𝟙 ((L₁ ⋙ G').obj (obj.{v_1, v_1, u_1, u_1} (𝟭 C₁) X₁)) = (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
Tactic: erw [(Localization.η adj L₁ L₂ W₂ G' F').naturality, Localization.η_app,
          assoc, assoc, ← G'.map_comp_assoc, ← G'.map_comp_assoc, assoc, Iso.hom_inv_id_app,
          comp_id, (CatCommSq.iso G L₁ L₂ G').inv.naturality_assoc, ← L₂.map_comp_assoc, eq,
          L₂.map_id, id_comp, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
⊢ F'.whiskerLeft (Localization.ε adj L₁ W₁ L₂ G' F') ≫
      (F'.associator G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F' =
    NatTrans.id (F' ⋙ 𝟭 D₁)
have apply : ∀ (X : C₂),
  Eq (α := (F' ⋙ 𝟭 D₁).obj (L₂.obj X) ⟶ (𝟭 D₂ ⋙ F').obj (L₂.obj X))
    ((F'.whiskerLeft (Localization.ε adj L₁ W₁ L₂ G' F') ≫
          (F'.associator G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F').app
      (L₂.obj X))
    ((NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X))
Tactic: apply natTrans_ext L₂ W₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ Eq (α := (F' ⋙ 𝟭 D₁).obj (L₂.obj X₂) ⟶ (𝟭 D₂ ⋙ F').obj (L₂.obj X₂))
    ((F'.whiskerLeft (Localization.ε adj L₁ W₁ L₂ G' F') ≫
          (F'.associator G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F').app
      (L₂.obj X₂))
    ((NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂))
have eq : (F.whiskerLeft adj.unit ≫ whiskerRight adj.counit F).app X₂ = NatTrans.app (𝟙 (F ⋙ 𝟭 C₁)) X₂
Tactic: have eq := congr_app adj.right_triangle X₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ Eq (α := (F' ⋙ 𝟭 D₁).obj (L₂.obj X₂) ⟶ (𝟭 D₂ ⋙ F').obj (L₂.obj X₂))
    ((F'.whiskerLeft (Localization.ε adj L₁ W₁ L₂ G' F') ≫
          (F'.associator G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F').app
      (L₂.obj X₂))
    ((NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂))
have rw : (Localization.ε adj L₁ W₁ L₂ G' F').app (F'.obj (L₂.obj X₂)) ≫
    F'.map (G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂)) ≫
      F'.map ((CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) =
  (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
Tactic: rw [NatTrans.comp_app, NatTrans.comp_app, whiskerLeft_app, whiskerRight_app,
          Localization.η_app, Functor.associator_inv_app, id_comp, F'.map_comp, F'.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (Localization.ε adj L₁ W₁ L₂ G' F').app (F'.obj (L₂.obj X₂)) ≫
      F'.map (G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂)) ≫
        F'.map ((CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
have erw : 𝟙 ((L₂ ⋙ F').obj X₂) = (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
Tactic: erw [← (Localization.ε _ _ _ _ _ _).naturality_assoc, Localization.ε_app,
          assoc, assoc, ← F'.map_comp_assoc, Iso.hom_inv_id_app, F'.map_id, id_comp,
          ← NatTrans.naturality, ← L₁.map_comp_assoc, eq, L₁.map_id, id_comp,
          Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
⊢ G.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G)
have hG : W.IsInvertedBy G
Tactic: have hG : W.IsInvertedBy G := fun _ _ _ hf => hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
hG : W.IsInvertedBy G
X : C₁
⊢ W (adj.unit.app X)
have change : IsIso (G.map (adj.unit.app X))
Tactic: change IsIso _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
hG : W.IsInvertedBy G
⊢ G.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G)
have this : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
Tactic: have : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X) := fun X =>
    Localization.inverts W.Q W _ (by
      change IsIso _
      infer_instance)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
W : MorphismProperty.{v_1, u_1} C₁ := MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G
hG : W.IsInvertedBy G
this : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
⊢ G.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₂) G)
have this₁ : IsIso (whiskerRight adj.unit W.Q)
Tactic: have : IsIso (whiskerRight adj.unit W.Q) := NatIso.isIso_of_isIso_app _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
⊢ F.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₁) F)
have rw : F.op.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C₁ᵒᵖ) F.op)
Tactic: rw [← Functor.IsLocalization.op_iff, MorphismProperty.op_inverseImage,
    MorphismProperty.op_isomorphisms]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
inst_4 : Category.{v_5, u_5} E
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
inst_7 : W₁.ContainsIdentities
inst_8 : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ E
F₁' F₂' : D₁ ⥤ Functor.{v_4, v_5, u_4, u_5} D₂ E
inst_9 : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst_10 : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ NatTrans.app ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)) (L₂.obj X₂) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂
have dsimp : 𝟙 ((F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) ≫
    NatTrans.app
        (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (obj uncurry F₁) (obj uncurry F₂) (obj uncurry F₁') (obj uncurry F₂')
          (map uncurry τ))
        (L₁.obj X₁, L₂.obj X₂) ≫
      𝟙 ((F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) =
  ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
    (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂
Tactic: dsimp [lift₂NatTrans, fullyFaithfulUncurry, Equivalence.fullyFaithfulFunctor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
inst_4 : Category.{v_5, u_5} E
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
inst_7 : W₁.ContainsIdentities
inst_8 : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ E
F₁' F₂' : D₁ ⥤ Functor.{v_4, v_5, u_4, u_5} D₂ E
inst_9 : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst_10 : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ 𝟙 ((F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) ≫
      NatTrans.app
          (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (obj uncurry F₁) (obj uncurry F₂) (obj uncurry F₁') (obj uncurry F₂')
            (map uncurry τ))
          (L₁.obj X₁, L₂.obj X₂) ≫
        𝟙 ((F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂
have simp : NatTrans.app
    (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (obj uncurry F₁) (obj uncurry F₂) (obj uncurry F₁') (obj uncurry F₂')
      (map uncurry τ))
    (L₁.obj X₁, L₂.obj X₂) =
  ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
    (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂
Tactic: simp only [comp_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
⊢ P.isoClosure.isLocal = P.isLocal
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P.isoClosure.isLocal f ↔ P.isLocal f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ P.isoClosure.isLocal f ↔ P.isLocal f
have h : P.isoClosure.isLocal f → P.isLocal f
Tactic: constructor