awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : X ⟶ Z
h : ∀ (a : X' ⟶ Y) (h : (fun (f : X' ⟶ Y) ↦ f ≫ g) a = e.inv ≫ f), ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f
⊢ ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f

Tactic:
obtain ⟨a, h⟩ := (hg _ hX').2 (e.inv ≫ f)

Premises used: And.right, CategoryTheory.CategoryStruct.comp, 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 : X ⟶ Z
a : X' ⟶ Y
h : (fun (f : X' ⟶ Y) ↦ f ≫ g) a = e.inv ≫ f
⊢ (fun (f : X ⟶ Y) ↦ f ≫ g) (e.hom ≫ a) = f

Tactic:
simp [h]
-- 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 : X ⟶ Z
a : X' ⟶ Y
h : (fun (f : X' ⟶ Y) ↦ f ≫ g) a = e.inv ≫ f
⊢ ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f

Tactic:
exact ⟨e.hom ≫ a, by simp [h]⟩
-- 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 x_1 : C
h : P x_1
⊢ Function.Bijective (β := x_1 ⟶ x) fun (f : x_1 ⟶ x) ↦ f ≫ 𝟙 x

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_1 Y Z : C
f : X_1 ⟶ Y
g : Y ⟶ Z
hf : P.isColocal f
hg : P.isColocal g
X : C
hX : P X
⊢ Function.Bijective.{v_1 + 1, v_1 + 1} (α := X ⟶ X_1) (β := X ⟶ Z)
    ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f)

Tactic:
Function.Bijective.comp (hg X hX) (hf X hX)

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_1 Y Z : C
f : X_1 ⟶ Y
g : Y ⟶ Z
hf : P.isColocal f
hg : P.isColocal g
X : C
hX : P X
h : ∀ (x : X ⟶ X_1), x ≫ f ≫ g = ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f) x
⊢ Function.Bijective (β := X ⟶ Z) fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f ≫ g

Tactic:
convert! Function.Bijective.comp (hg X hX) (hf X hX)

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_1 Y Z : C
f : X_1 ⟶ Y
g : Y ⟶ Z
hg : P.isColocal g
hfg : P.isColocal (f ≫ g)
X : C
hX : P X
rw :
  Function.Bijective.{v_1 + 1, v_1 + 1} (α := X ⟶ X_1) (β := X ⟶ Z)
    ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f)
⊢ Function.Bijective (β := X ⟶ Y) fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f

Tactic:
rw [← Function.Bijective.of_comp_iff' (hg X hX)]

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_1 Y Z : C
f : X_1 ⟶ Y
g : Y ⟶ Z
hg : P.isColocal g
hfg : P.isColocal (f ≫ g)
X : C
hX : P X
⊢ Function.Bijective (β := X ⟶ Z) fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f ≫ g

Tactic:
hfg X hX
-- 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_1 Y Z : C
f : X_1 ⟶ Y
g : Y ⟶ Z
hg : P.isColocal g
hfg : P.isColocal (f ≫ g)
X : C
hX : P X
h : ∀ (x : X ⟶ X_1), ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f) x = x ≫ f ≫ g
⊢ Function.Bijective.{v_1 + 1, v_1 + 1} (α := X ⟶ X_1) (β := X ⟶ Z)
    ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f)

Tactic:
convert! hfg X hX
-- 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_1 Y Z : C
f : X_1 ⟶ Y
g : Y ⟶ Z
hf : P.isColocal f
hfg : P.isColocal (f ≫ g)
X : C
hX : P X
rw :
  Function.Bijective.{v_1 + 1, v_1 + 1} (α := X ⟶ X_1) (β := X ⟶ Z)
    ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f)
⊢ Function.Bijective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g

Tactic:
rw [← Function.Bijective.of_comp_iff _ (hf X hX)]

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_1 Y Z : C
f : X_1 ⟶ Y
g : Y ⟶ Z
hf : P.isColocal f
hfg : P.isColocal (f ≫ g)
X : C
hX : P X
⊢ Function.Bijective (β := X ⟶ Z) fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f ≫ g

Tactic:
hfg X hX
-- 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_1 Y Z : C
f : X_1 ⟶ Y
g : Y ⟶ Z
hf : P.isColocal f
hfg : P.isColocal (f ≫ g)
X : C
hX : P X
h : ∀ (x : X ⟶ X_1), ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f) x = x ≫ f ≫ g
⊢ Function.Bijective.{v_1 + 1, v_1 + 1} (α := X ⟶ X_1) (β := X ⟶ Z)
    ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f)

Tactic:
convert! hfg X hX
-- 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 (β := Z ⟶ Y) fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f
right : Function.Surjective (β := Z ⟶ Y) fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f
⊢ Function.Bijective (β := Z ⟶ Y) fun (f_1 : Z ⟶ X) ↦ f_1 ≫ 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
inst_1 : IsIso f
Z : C
h : P Z
g₁ g₂ : Z ⟶ X
left : Eq.{v_1 + 1} (α := Z ⟶ Y) ((fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f) g₁) ((fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f) g₂) → g₁ = g₂
⊢ Eq.{v_1 + 1} (α := Z ⟶ Y) ((fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f) g₁) ((fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f) 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₂ : Z ⟶ X
h_1 : Eq.{v_1 + 1} (α := Z ⟶ Y) ((fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f) g₁) ((fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f) g₂)
⊢ g₁ = g₂

Tactic:
simpa only [← cancel_mono f]

Premises used: CategoryTheory.cancel_mono
-- 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 : Z ⟶ Y
⊢ (fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f) (g ≫ inv f) = 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 : Z ⟶ Y
⊢ ∃ (a : Z ⟶ X), (fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f) a = g

Tactic:
exact ⟨g ≫ inv f, 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.isColocal f → IsIso f
mpr : IsIso f → P.isColocal f
⊢ P.isColocal 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.isColocal f
mp : ∀ (g : Y ⟶ X) (hg : Eq.{v_1 + 1} (α := Y ⟶ Y) ((fun (f_1 : Y ⟶ X) ↦ f_1 ≫ f) g) (𝟙 Y)), IsIso f
⊢ IsIso f

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

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.isColocal f
g : Y ⟶ X
hg : Eq.{v_1 + 1} (α := Y ⟶ Y) ((fun (f_1 : Y ⟶ X) ↦ f_1 ≫ f) g) (𝟙 Y)
⊢ IsIso f

Tactic:
exact ⟨g, (hf _ hX).1 (by cat_disch), hg⟩
-- 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.isColocal f

Tactic:
apply isColocal_of_isIso

Premises used: CategoryTheory.ObjectProperty.isColocal_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.isColocal ↔ P ≤ W.isColocal

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)ᵒᵈ) ∘ isColocal)
    (MorphismProperty.isColocal ∘ (⇑OrderDual.ofDual : (a : (MorphismProperty C)ᵒᵈ) → MorphismProperty C))

Tactic:
le_isColocal_iff

Premises used: CategoryTheory.MorphismProperty.isColocal, CategoryTheory.ObjectProperty.le_isColocal_iff, OrderDual, GaloisConnection, CategoryTheory.ObjectProperty.isColocal
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
X : D
Y : C
⊢ Function.Bijective (α := F.obj (G.obj X) ⟶ F.obj Y) (β := X ⟶ F.obj Y)
    (⇑(Equiv.trans (Equiv.symm (Functor.FullyFaithful.ofFullyFaithful F).homEquiv) (adj.homEquiv X Y)) :
      (a : F.obj (G.obj X) ⟶ F.obj Y) → X ⟶ F.obj Y)

Tactic:
((Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm.trans
        (adj.homEquiv X Y)).bijective

Premises used: Equiv.bijective, Equiv.trans, CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.Adjunction.homEquiv, Equiv.symm, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
X : D
Y : C
h :
  ((G ⋙ F).obj X ⟶ F.obj Y) = (F.obj (G.obj X) ⟶ F.obj Y) →
    (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) X ⟶ F.obj Y) = (X ⟶ F.obj Y) →
      Eq (α := ((G ⋙ F).obj X ⟶ F.obj Y) → (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) X ⟶ F.obj Y))
        (fun (g : (G ⋙ F).obj X ⟶ F.obj Y) ↦ adj.unit.app X ≫ g)
        (⇑(Equiv.trans (Equiv.symm (Functor.FullyFaithful.ofFullyFaithful F).homEquiv) (adj.homEquiv X Y)) :
          (a : F.obj (G.obj X) ⟶ F.obj Y) → X ⟶ F.obj Y)
⊢ Function.Bijective (β := Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) X ⟶ F.obj Y) fun (g : (G ⋙ F).obj X ⟶ F.obj Y) ↦
    adj.unit.app X ≫ g

Tactic:
convert!
    ((Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm.trans
        (adj.homEquiv X Y)).bijective using 1

Premises used: Equiv.bijective, Equiv.trans, CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.Adjunction.homEquiv, Equiv.symm, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
X : D
Y : C
e_1 : ((G ⋙ F).obj X ⟶ F.obj Y) = (F.obj (G.obj X) ⟶ F.obj Y)
e_2 : (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) X ⟶ F.obj Y) = (X ⟶ F.obj Y)
h :
  Eq.{v_2 + 1} (α := (F.obj (G.obj X) ⟶ F.obj Y) → (X ⟶ F.obj Y))
    (fun (g : F.obj (G.obj X) ⟶ F.obj Y) ↦ adj.unit.app X ≫ g)
    ((fun (f : G.obj X ⟶ Y) ↦ adj.unit.app X ≫ F.map f) ∘
      (⇑(Equiv.symm (Functor.FullyFaithful.ofFullyFaithful F).homEquiv) :
        (a : F.obj (G.obj X) ⟶ F.obj Y) → G.obj X ⟶ Y))
⊢ Eq (α := ((G ⋙ F).obj X ⟶ F.obj Y) → (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) X ⟶ F.obj Y))
    (fun (g : (G ⋙ F).obj X ⟶ F.obj Y) ↦ adj.unit.app X ≫ g)
    (⇑(Equiv.trans (Equiv.symm (Functor.FullyFaithful.ofFullyFaithful F).homEquiv) (adj.homEquiv X Y)) :
      (a : F.obj (G.obj X) ⟶ F.obj Y) → X ⟶ F.obj Y)

Tactic:
dsimp [Adjunction.homEquiv]

Premises used: CategoryTheory.Adjunction.homEquiv
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
X : D
Y : C
e_1 : ((G ⋙ F).obj X ⟶ F.obj Y) = (F.obj (G.obj X) ⟶ F.obj Y)
e_2 : (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) X ⟶ F.obj Y) = (X ⟶ F.obj Y)
⊢ Eq.{v_2 + 1} (α := (F.obj (G.obj X) ⟶ F.obj Y) → (X ⟶ F.obj Y))
    (fun (g : F.obj (G.obj X) ⟶ F.obj Y) ↦ adj.unit.app X ≫ g)
    ((fun (f : G.obj X ⟶ Y) ↦ adj.unit.app X ≫ F.map f) ∘
      (⇑(Equiv.symm (Functor.FullyFaithful.ofFullyFaithful F).homEquiv) :
        (a : F.obj (G.obj X) ⟶ F.obj Y) → G.obj X ⟶ Y))

Tactic:
aesop
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
X Y : D
f : X ⟶ Y
⊢ Functor.map (𝟭 D) f ≫ adj.unit.app Y = adj.unit.app X ≫ (G ⋙ F).map f

Tactic:
have := adj.unit.naturality f
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
X Y : D
f : X ⟶ Y
this : f ≫ adj.unit.app Y = adj.unit.app X ≫ F.map (G.map f)
rw : IsIso (F.map (G.map f)) ↔ IsIso (G.map f)
⊢ isLocal (fun (x : D) ↦ x ∈ Set.range F.obj) f ↔ IsIso (G.map f)

Tactic:
rw [← (isLocal (· ∈ Set.range F.obj)).postcomp_iff _ _ (isLocal_adj_unit_app adj Y),
    this, (isLocal (· ∈ Set.range F.obj)).precomp_iff _ _ (isLocal_adj_unit_app adj X),
    isLocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩]

Premises used: CategoryTheory.MorphismProperty.postcomp_iff, CategoryTheory.ObjectProperty.isLocal, Membership.mem, CategoryTheory.ObjectProperty.isLocal_iff_isIso, CategoryTheory.MorphismProperty.precomp_iff, CategoryTheory.ObjectProperty.isLocal_adj_unit_app, Set.range, CategoryTheory.Functor.obj
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
X Y : D
f : X ⟶ Y
this : f ≫ adj.unit.app Y = adj.unit.app X ≫ F.map (G.map f)
⊢ IsIso (F.map (G.map f)) ↔ IsIso (G.map f)

Tactic:
⟨fun _ ↦ isIso_of_fully_faithful F (G.map f), fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.isIso_of_fully_faithful, inferInstance, CategoryTheory.Functor.map, Iff.intro
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
X Y : D
f : X ⟶ Y
this : f ≫ adj.unit.app Y = adj.unit.app X ≫ F.map (G.map f)
⊢ IsIso (F.map (G.map f)) ↔ IsIso (G.map f)

Tactic:
exact ⟨fun _ ↦ isIso_of_fully_faithful F (G.map f), fun _ ↦ inferInstance⟩
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
h :
  ∀ ⦃P₁ P₂ : D⦄ (f : P₁ ⟶ P₂),
    isLocal (fun (x : D) ↦ x ∈ Set.range F.obj) f ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G f
⊢ (isLocal fun (x : D) ↦ x ∈ Set.range F.obj) = MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G

Tactic:
ext P₁ P₂ f
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
P₁ P₂ : D
f : P₁ ⟶ P₂
h : IsIso (G.map f) ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G f
⊢ isLocal (fun (x : D) ↦ x ∈ Set.range F.obj) f ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G f

Tactic:
rw [isLocal_iff_isIso_map adj]

Premises used: CategoryTheory.ObjectProperty.isLocal_iff_isIso_map
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
P₁ P₂ : D
f : P₁ ⟶ P₂
⊢ IsIso (G.map f) ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G f

Tactic:
rfl
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
rw : G.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G)
⊢ G.IsLocalization (isLocal fun (x : D) ↦ x ∈ Set.range F.obj)

Tactic:
rw [isLocal_eq_inverseImage_isomorphisms adj]

Premises used: CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
⊢ G.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G)

Tactic:
adj.isLocalization

Premises used: CategoryTheory.Adjunction.isLocalization
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : F.Full
inst_3 : F.Faithful
⊢ G.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G)

Tactic:
exact adj.isLocalization

Premises used: CategoryTheory.Adjunction.isLocalization
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
X : C
Y : D
⊢ Function.Bijective (α := G.obj Y ⟶ G.obj (F.obj X)) (β := G.obj Y ⟶ X)
    (⇑(Equiv.trans (Equiv.symm (Functor.FullyFaithful.ofFullyFaithful G).homEquiv) (adj.homEquiv Y X).symm) :
      (a : G.obj Y ⟶ G.obj (F.obj X)) → G.obj Y ⟶ X)

Tactic:
((Functor.FullyFaithful.ofFullyFaithful G).homEquiv.symm.trans
        (adj.homEquiv Y X).symm).bijective

Premises used: Equiv.bijective, Equiv.trans, CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.Adjunction.homEquiv, Equiv.symm, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
X : C
Y : D
h :
  (G.obj Y ⟶ (F ⋙ G).obj X) = (G.obj Y ⟶ G.obj (F.obj X)) →
    (G.obj Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) = (G.obj Y ⟶ X) →
      Eq (α := (G.obj Y ⟶ (F ⋙ G).obj X) → (G.obj Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))
        (fun (f : G.obj Y ⟶ (F ⋙ G).obj X) ↦ f ≫ adj.counit.app X)
        (⇑(Equiv.trans (Equiv.symm (Functor.FullyFaithful.ofFullyFaithful G).homEquiv) (adj.homEquiv Y X).symm) :
          (a : G.obj Y ⟶ G.obj (F.obj X)) → G.obj Y ⟶ X)
⊢ Function.Bijective (β := G.obj Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) fun (f : G.obj Y ⟶ (F ⋙ G).obj X) ↦
    f ≫ adj.counit.app X

Tactic:
convert!
    ((Functor.FullyFaithful.ofFullyFaithful G).homEquiv.symm.trans
        (adj.homEquiv Y X).symm).bijective using 1

Premises used: Equiv.bijective, Equiv.trans, CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.Adjunction.homEquiv, Equiv.symm, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
X : C
Y : D
e_1 : (G.obj Y ⟶ (F ⋙ G).obj X) = (G.obj Y ⟶ G.obj (F.obj X))
e_2 : (G.obj Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) = (G.obj Y ⟶ X)
h :
  Eq.{v_1 + 1} (α := (G.obj Y ⟶ G.obj (F.obj X)) → (G.obj Y ⟶ X))
    (fun (f : G.obj Y ⟶ G.obj (F.obj X)) ↦ f ≫ adj.counit.app X)
    ((fun (g : Y ⟶ F.obj X) ↦ G.map g ≫ adj.counit.app X) ∘
      (⇑(Equiv.symm (Functor.FullyFaithful.ofFullyFaithful G).homEquiv) :
        (a : G.obj Y ⟶ G.obj (F.obj X)) → Y ⟶ F.obj X))
⊢ Eq (α := (G.obj Y ⟶ (F ⋙ G).obj X) → (G.obj Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))
    (fun (f : G.obj Y ⟶ (F ⋙ G).obj X) ↦ f ≫ adj.counit.app X)
    (⇑(Equiv.trans (Equiv.symm (Functor.FullyFaithful.ofFullyFaithful G).homEquiv) (adj.homEquiv Y X).symm) :
      (a : G.obj Y ⟶ G.obj (F.obj X)) → G.obj Y ⟶ X)

Tactic:
dsimp [Adjunction.homEquiv]

Premises used: CategoryTheory.Adjunction.homEquiv
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
X Y : C
f : X ⟶ Y
⊢ (F ⋙ G).map f ≫ adj.counit.app Y = adj.counit.app X ≫ Functor.map (𝟭 C) f

Tactic:
have := adj.counit.naturality f
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
X Y : C
f : X ⟶ Y
this : G.map (F.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f
rw : IsIso (G.map (F.map f)) ↔ IsIso (F.map f)
⊢ isColocal (fun (x : C) ↦ x ∈ Set.range G.obj) f ↔ IsIso (F.map f)

Tactic:
rw [← (isColocal _).precomp_iff _ _ (isColocal_adj_counit_app adj X),
    ← this, (isColocal _).postcomp_iff _ _ (isColocal_adj_counit_app adj Y),
    isColocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩]

Premises used: CategoryTheory.MorphismProperty.postcomp_iff, CategoryTheory.ObjectProperty.isColocal_iff_isIso, CategoryTheory.ObjectProperty.isColocal_adj_counit_app, CategoryTheory.MorphismProperty.precomp_iff, CategoryTheory.ObjectProperty.isColocal
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
X Y : C
f : X ⟶ Y
this : G.map (F.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f
⊢ IsIso (G.map (F.map f)) ↔ IsIso (F.map f)

Tactic:
⟨fun _ ↦ isIso_of_fully_faithful G (F.map f), fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.isIso_of_fully_faithful, inferInstance, CategoryTheory.Functor.map, Iff.intro