awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Bifunctor
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₂
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₂
⊢ 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₂

Tactic:
dsimp [lift₂NatTrans, fullyFaithfulUncurry, Equivalence.fullyFaithfulFunctor]

Premises used: CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.Functor.fullyFaithfulUncurry, CategoryTheory.Localization.lift₂NatTrans
-- Module: Mathlib.CategoryTheory.Localization.Bifunctor
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₂
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₂
⊢ 𝟙 ((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:
simp only [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Bifunctor
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
      (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:
liftNatTrans_app _ _ _ _ (uncurry.obj F₁') (uncurry.obj F₂') (uncurry.map τ) ⟨X₁, X₂⟩

Premises used: Prod.mk, CategoryTheory.Functor.uncurry, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.Functor.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Localization.Bifunctor
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
      (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:
exact liftNatTrans_app _ _ _ _ (uncurry.obj F₁') (uncurry.obj F₂') (uncurry.map τ) ⟨X₁, X₂⟩

Premises used: Prod.mk, CategoryTheory.Functor.uncurry, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.Functor.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Localization.Bifunctor
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₂' : D₁ ⥤ Functor.{v_4, v_5, u_4, u_5} D₂ E
τ τ' : F₁' ⟶ F₂'
h :
  ∀ (X₁ : C₁) (X₂ : C₂),
    Eq (α := (F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂) ⟶ (F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂))
      (NatTrans.app (τ.app (L₁.obj X₁)) (L₂.obj X₂)) (NatTrans.app (τ'.app (L₁.obj X₁)) (L₂.obj X₂))
⊢ τ = τ'

Tactic:
uncurry.map_injective (natTrans_ext (L₁.prod L₂) (W₁.prod W₂) (fun _ ↦ h _ _))

Premises used: CategoryTheory.Localization.natTrans_ext, CategoryTheory.MorphismProperty.prod, CategoryTheory.Functor.uncurry, CategoryTheory.Functor.prod, Prod.fst, CategoryTheory.Functor.map_injective, Prod.snd
-- Module: Mathlib.CategoryTheory.Localization.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
E' : Type u_6
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
inst_5 : Category.{v_6, u_6} 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_6 : L₁.IsLocalization W₁
inst_7 : L₂.IsLocalization W₂
inst_8 : W₁.ContainsIdentities
inst_9 : 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_10 : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst_11 : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂),
    Eq (α := (F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂) ⟶ (F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂))
      (NatTrans.app
        ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom ≫ lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv).app
          (L₁.obj X₁))
        (L₂.obj X₂))
      (NatTrans.app (NatTrans.app (𝟙 F₁') (L₁.obj X₁)) (L₂.obj X₂))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
E' : Type u_6
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
inst_5 : Category.{v_6, u_6} 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_6 : L₁.IsLocalization W₁
inst_7 : L₂.IsLocalization W₂
inst_8 : W₁.ContainsIdentities
inst_9 : 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_10 : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst_11 : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂),
    Eq (α := (F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂) ⟶ (F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂))
      (NatTrans.app
        ((lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv ≫ lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom).app
          (L₁.obj X₁))
        (L₂.obj X₂))
      (NatTrans.app (NatTrans.app (𝟙 F₂') (L₁.obj X₁)) (L₂.obj X₂))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P.isoClosure.isLocal f ↔ P.isLocal f
⊢ P.isoClosure.isLocal = P.isLocal

Tactic:
ext X Y f
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
h : P.isoClosure.isLocal f → P.isLocal f
h₁ : P.isLocal f → P.isoClosure.isLocal f
⊢ P.isoClosure.isLocal f ↔ P.isLocal f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hf : P.isoClosure.isLocal f
Z : C
hZ : P Z
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
hf _ (P.le_isoClosure _ hZ)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hf : P.isoClosure.isLocal f
Z : C
hZ : P Z
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
exact hf _ (P.le_isoClosure _ hZ)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
h : Function.Injective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
h₁ : Function.Surjective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : Eq.{v_1 + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
h : g₁ ≫ e.hom = g₂ ≫ e.hom
⊢ g₁ = g₂

Tactic:
rw [← cancel_mono e.hom]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : Eq.{v_1 + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
h : Eq.{v_1 + 1} (α := X ⟶ Z') ((fun (g : Y ⟶ Z') ↦ f ≫ g) (g₁ ≫ e.hom)) ((fun (g : Y ⟶ Z') ↦ f ≫ g) (g₂ ≫ e.hom))
⊢ g₁ ≫ e.hom = g₂ ≫ e.hom

Tactic:
apply (hf _ hZ').1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : Eq.{v_1 + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
⊢ Eq.{v_1 + 1} (α := X ⟶ Z') ((fun (g : Y ⟶ Z') ↦ f ≫ g) (g₁ ≫ e.hom)) ((fun (g : Y ⟶ Z') ↦ f ≫ g) (g₂ ≫ e.hom))

Tactic:
simp only [reassoc_of% eq]
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g : X ⟶ Z
h : ∀ (a : Y ⟶ Z') (h : (fun (g : Y ⟶ Z') ↦ f ≫ g) a = g ≫ e.hom), ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g

Tactic:
obtain ⟨a, h⟩ := (hf _ hZ').2 (g ≫ e.hom)

Premises used: And.right, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g : X ⟶ Z
a : Y ⟶ Z'
h : (fun (g : Y ⟶ Z') ↦ f ≫ g) a = g ≫ e.hom
⊢ (fun (g : Y ⟶ Z) ↦ f ≫ g) (a ≫ e.inv) = g

Tactic:
simp only [reassoc_of% h, e.hom_inv_id, comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g : X ⟶ Z
a : Y ⟶ Z'
h : (fun (g : Y ⟶ Z') ↦ f ≫ g) a = g ≫ e.hom
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g

Tactic:
exact ⟨a ≫ e.inv, by simp only [reassoc_of% h, e.hom_inv_id, comp_id]⟩
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
X Z : C
h : P Z
⊢ Function.Bijective (β := X ⟶ Z) fun (g : X ⟶ Z) ↦ 𝟙 X ≫ g

Tactic:
simpa [id_comp] using Function.bijective_id

Premises used: Function.bijective_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
X Y Z_1 : C
f : X ⟶ Y
g : Y ⟶ Z_1
hf : P.isLocal f
hg : P.isLocal g
Z : C
hZ : P Z
⊢ Function.Bijective (β := X ⟶ Z) fun (g_1 : Z_1 ⟶ Z) ↦ (f ≫ g) ≫ g_1

Tactic:
simpa using Function.Bijective.comp (hf Z hZ) (hg Z hZ)

Premises used: Function.Bijective.comp
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
X Y Z_1 : C
f : X ⟶ Y
g : Y ⟶ Z_1
hg : P.isLocal g
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
rw :
  Function.Bijective.{v_1 + 1, v_1 + 1} (α := Z_1 ⟶ Z) (β := X ⟶ Z)
    ((fun (g : Y ⟶ Z) ↦ f ≫ g) ∘ fun (g_1 : Z_1 ⟶ Z) ↦ g ≫ g_1)
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
rw [← Function.Bijective.of_comp_iff _ (hg Z hZ)]

Premises used: Function.Bijective.of_comp_iff
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
X Y Z_1 : C
f : X ⟶ Y
g : Y ⟶ Z_1
hg : P.isLocal g
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
⊢ Function.Bijective.{v_1 + 1, v_1 + 1} (α := Z_1 ⟶ Z) (β := X ⟶ Z)
    ((fun (g : Y ⟶ Z) ↦ f ≫ g) ∘ fun (g_1 : Z_1 ⟶ Z) ↦ g ≫ g_1)

Tactic:
simpa using hfg Z hZ
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
X Y Z_1 : C
f : X ⟶ Y
g : Y ⟶ Z_1
hf : P.isLocal f
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
rw :
  Function.Bijective.{v_1 + 1, v_1 + 1} (α := Z_1 ⟶ Z) (β := X ⟶ Z)
    ((fun (g : Y ⟶ Z) ↦ f ≫ g) ∘ fun (g_1 : Z_1 ⟶ Z) ↦ g ≫ g_1)
⊢ Function.Bijective (β := Y ⟶ Z) fun (g_1 : Z_1 ⟶ Z) ↦ g ≫ g_1

Tactic:
rw [← Function.Bijective.of_comp_iff' (hf Z hZ)]

Premises used: Function.Bijective.of_comp_iff'
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
X Y Z_1 : C
f : X ⟶ Y
g : Y ⟶ Z_1
hf : P.isLocal f
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
⊢ Function.Bijective.{v_1 + 1, v_1 + 1} (α := Z_1 ⟶ Z) (β := X ⟶ Z)
    ((fun (g : Y ⟶ Z) ↦ f ≫ g) ∘ fun (g_1 : Z_1 ⟶ Z) ↦ g ≫ g_1)

Tactic:
simpa using hfg Z hZ
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
inst_1 : IsIso f
Z : C
h : P Z
left : Function.Injective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
right : Function.Surjective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
inst_1 : IsIso f
Z : C
h : P Z
g₁ g₂ : Y ⟶ Z
left : Eq.{v_1 + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂) → g₁ = g₂
⊢ Eq.{v_1 + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂) → g₁ = g₂

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
inst_1 : IsIso f
Z : C
h : P Z
g₁ g₂ : Y ⟶ Z
h_1 : Eq.{v_1 + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
⊢ g₁ = g₂

Tactic:
simpa only [← cancel_epi f]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
inst_1 : IsIso f
Z : C
h : P Z
g : X ⟶ Z
⊢ (fun (g : Y ⟶ Z) ↦ f ≫ g) (inv f ≫ g) = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
inst_1 : IsIso f
Z : C
h : P Z
g : X ⟶ Z
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g

Tactic:
exact ⟨inv f ≫ g, by simp⟩
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hX : P X
hY : P Y
mp : P.isLocal f → IsIso f
mpr : IsIso f → P.isLocal f
⊢ P.isLocal f ↔ IsIso f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hX : P X
hY : P Y
hf : P.isLocal f
mp : ∀ (g : Y ⟶ X) (hg : Eq.{v_1 + 1} (α := X ⟶ X) ((fun (g : Y ⟶ X) ↦ f ≫ g) g) (𝟙 X)), IsIso f
⊢ IsIso f

Tactic:
obtain ⟨g, hg⟩ := (hf _ hX).2 (𝟙 X)

Premises used: CategoryTheory.CategoryStruct.id, And.right
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hX : P X
hY : P Y
hf : P.isLocal f
g : Y ⟶ X
hg : Eq.{v_1 + 1} (α := X ⟶ X) ((fun (g : Y ⟶ X) ↦ f ≫ g) g) (𝟙 X)
⊢ Eq.{v_1 + 1} (α := X ⟶ Y) ((fun (g : Y ⟶ Y) ↦ f ≫ g) (g ≫ f)) ((fun (g : Y ⟶ Y) ↦ f ≫ g) (𝟙 Y))

Tactic:
simp only [reassoc_of% hg, comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hX : P X
hY : P Y
hf : P.isLocal f
g : Y ⟶ X
hg : Eq.{v_1 + 1} (α := X ⟶ X) ((fun (g : Y ⟶ X) ↦ f ≫ g) g) (𝟙 X)
⊢ IsIso f

Tactic:
exact ⟨g, hg, (hf _ hY).1 (by simp only [reassoc_of% hg, comp_id])⟩
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
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
hX : P X
hY : P Y
⊢ IsIso f → P.isLocal f

Tactic:
apply isLocal_of_isIso

Premises used: CategoryTheory.ObjectProperty.isLocal_of_isIso
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
⊢ W ≤ P.isLocal ↔ P ≤ W.isLocal

Tactic:
⟨fun h _ hZ _ _ _ hf ↦ h _ hf _ hZ,
    fun h _ _ _ hf _ hZ ↦ h _ hZ _ hf⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ GaloisConnection (α := ObjectProperty.{v_1, u_1} C) (β := (MorphismProperty.{v_1, u_1} C)ᵒᵈ)
    ((⇑OrderDual.toDual : (a : MorphismProperty C) → (MorphismProperty C)ᵒᵈ) ∘ isLocal)
    (MorphismProperty.isLocal ∘ (⇑OrderDual.ofDual : (a : (MorphismProperty C)ᵒᵈ) → MorphismProperty C))

Tactic:
le_isLocal_iff

Premises used: CategoryTheory.ObjectProperty.isLocal, CategoryTheory.ObjectProperty.le_isLocal_iff, CategoryTheory.MorphismProperty.isLocal, OrderDual, GaloisConnection
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
h : ∀ ⦃Y Z : C⦄ (g : Y ⟶ Z), P.isoClosure.isColocal g ↔ P.isColocal g
⊢ P.isoClosure.isColocal = P.isColocal

Tactic:
ext Y Z g
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
Y Z : C
g : Y ⟶ Z
h : P.isoClosure.isColocal g → P.isColocal g
h₁ : P.isColocal g → P.isoClosure.isColocal g
⊢ P.isoClosure.isColocal g ↔ P.isColocal g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
Y Z : C
g : Y ⟶ Z
hg : P.isoClosure.isColocal g
X : C
hX : P X
⊢ Function.Bijective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g

Tactic:
hg _ (P.le_isoClosure _ hX)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
Y Z : C
g : Y ⟶ Z
hg : P.isoClosure.isColocal g
X : C
hX : P X
⊢ Function.Bijective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g

Tactic:
exact hg _ (P.le_isoClosure _ hX)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
h : Function.Injective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g
h₁ : Function.Surjective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g
⊢ Function.Bijective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
f₁ f₂ : X ⟶ Y
eq : Eq.{v_1 + 1} (α := X ⟶ Z) ((fun (f : X ⟶ Y) ↦ f ≫ g) f₁) ((fun (f : X ⟶ Y) ↦ f ≫ g) f₂)
h : e.inv ≫ f₁ = e.inv ≫ f₂
⊢ f₁ = f₂

Tactic:
rw [← cancel_epi e.inv]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
f₁ f₂ : X ⟶ Y
eq : Eq.{v_1 + 1} (α := X ⟶ Z) ((fun (f : X ⟶ Y) ↦ f ≫ g) f₁) ((fun (f : X ⟶ Y) ↦ f ≫ g) f₂)
h : Eq.{v_1 + 1} (α := X' ⟶ Z) ((fun (f : X' ⟶ Y) ↦ f ≫ g) (e.inv ≫ f₁)) ((fun (f : X' ⟶ Y) ↦ f ≫ g) (e.inv ≫ f₂))
⊢ e.inv ≫ f₁ = e.inv ≫ f₂

Tactic:
apply (hg _ hX').1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
f₁ f₂ : X ⟶ Y
eq : Eq.{v_1 + 1} (α := X ⟶ Z) ((fun (f : X ⟶ Y) ↦ f ≫ g) f₁) ((fun (f : X ⟶ Y) ↦ f ≫ g) f₂)
⊢ Eq.{v_1 + 1} (α := X' ⟶ Z) ((fun (f : X' ⟶ Y) ↦ f ≫ g) (e.inv ≫ f₁)) ((fun (f : X' ⟶ Y) ↦ f ≫ g) (e.inv ≫ f₂))

Tactic:
simp [eq]