awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : P.isoClosure.isLocal f → P.isLocal f
⊢ P.isoClosure.isLocal f ↔ P.isLocal f
have h₁ : P.isLocal f → P.isoClosure.isLocal f
Tactic: constructor
-- 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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have h : Function.Injective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
Tactic: constructor
-- 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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
h : Function.Injective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have h₁ : Function.Surjective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
Tactic: constructor
-- 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
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₂)
⊢ g₁ = g₂
have h : g₁ ≫ e.hom = g₂ ≫ e.hom
Tactic: rw [← cancel_mono e.hom]
-- 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
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₂)
⊢ g₁ ≫ e.hom = g₂ ≫ e.hom
have 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))
Tactic: apply (hf _ hZ').1
-- 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
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g : X ⟶ Z
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
have 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
Tactic: obtain ⟨a, h⟩ := (hf _ hZ').2 (g ≫ e.hom)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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 (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have 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)
Tactic: rw [← Function.Bijective.of_comp_iff _ (hg Z hZ)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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 (β := Y ⟶ Z) fun (g_1 : Z_1 ⟶ Z) ↦ g ≫ g_1
have 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)
Tactic: rw [← Function.Bijective.of_comp_iff' (hf Z hZ)]
-- 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
inst_1 : IsIso f
Z : C
h : P Z
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have left : Function.Injective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
Tactic: constructor
-- 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
inst_1 : IsIso f
Z : C
h : P Z
left : Function.Injective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have right : Function.Surjective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
Tactic: constructor
-- 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
hX : P X
hY : P Y
⊢ P.isLocal f ↔ IsIso f
have mp : P.isLocal f → IsIso f
Tactic: constructor
-- 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
hX : P X
hY : P Y
mp : P.isLocal f → IsIso f
⊢ P.isLocal f ↔ IsIso f
have mpr : IsIso f → P.isLocal f
Tactic: constructor
-- 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
hX : P X
hY : P Y
hf : P.isLocal f
⊢ IsIso f
have mp : ∀ (g : Y ⟶ X) (hg : Eq.{v_1 + 1} (α := X ⟶ X) ((fun (g : Y ⟶ X) ↦ f ≫ g) g) (𝟙 X)), IsIso f
Tactic: obtain ⟨g, hg⟩ := (hf _ hX).2 (𝟙 X)
-- 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.isColocal = P.isColocal
have h : ∀ ⦃Y Z : C⦄ (g : Y ⟶ Z), P.isoClosure.isColocal g ↔ P.isColocal g
Tactic: ext Y Z g
-- 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
Y Z : C
g : Y ⟶ Z
⊢ P.isoClosure.isColocal g ↔ P.isColocal g
have h : P.isoClosure.isColocal g → P.isColocal g
Tactic: constructor
-- 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
Y Z : C
g : Y ⟶ Z
h : P.isoClosure.isColocal g → P.isColocal g
⊢ P.isoClosure.isColocal g ↔ P.isColocal g
have h₁ : P.isColocal g → P.isoClosure.isColocal g
Tactic: constructor
-- 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
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Function.Bijective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g
have h : Function.Injective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g
Tactic: constructor
-- 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
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
⊢ Function.Bijective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g
have h₁ : Function.Surjective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g
Tactic: constructor
-- 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
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₂)
⊢ f₁ = f₂
have h : e.inv ≫ f₁ = e.inv ≫ f₂
Tactic: rw [← cancel_epi e.inv]
-- 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
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₂)
⊢ e.inv ≫ f₁ = e.inv ≫ f₂
have 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₂))
Tactic: apply (hg _ hX').1
-- 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
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), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f
have 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
Tactic: obtain ⟨a, h⟩ := (hg _ hX').2 (e.inv ≫ f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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 (β := X ⟶ Z) fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f ≫ g
have h : ∀ (x : X ⟶ X_1), x ≫ f ≫ g = ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f) x
Tactic: convert! Function.Bijective.comp (hg X hX) (hf X hX)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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 ⟶ Y) fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f
have 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)
Tactic: rw [← Function.Bijective.of_comp_iff' (hg X hX)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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.{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)
have h : ∀ (x : X ⟶ X_1), ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f) x = x ≫ f ≫ g
Tactic: convert! hfg X hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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 : X ⟶ Y) ↦ f ≫ g
have 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)
Tactic: rw [← Function.Bijective.of_comp_iff _ (hf X hX)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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.{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)
have h : ∀ (x : X ⟶ X_1), ((fun (f : X ⟶ Y) ↦ f ≫ g) ∘ fun (f_1 : X ⟶ X_1) ↦ f_1 ≫ f) x = x ≫ f ≫ g
Tactic: convert! hfg X hX
-- 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
inst_1 : IsIso f
Z : C
h : P Z
⊢ Function.Bijective (β := Z ⟶ Y) fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f
have left : Function.Injective (β := Z ⟶ Y) fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f
Tactic: constructor
-- 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
inst_1 : IsIso f
Z : C
h : P Z
left : Function.Injective (β := Z ⟶ Y) fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f
⊢ Function.Bijective (β := Z ⟶ Y) fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f
have right : Function.Surjective (β := Z ⟶ Y) fun (f_1 : Z ⟶ X) ↦ f_1 ≫ f
Tactic: constructor
-- 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
hX : P X
hY : P Y
⊢ P.isColocal f ↔ IsIso f
have mp : P.isColocal f → IsIso f
Tactic: constructor
-- 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
hX : P X
hY : P Y
mp : P.isColocal f → IsIso f
⊢ P.isColocal f ↔ IsIso f
have mpr : IsIso f → P.isColocal f
Tactic: constructor
-- 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
hX : P X
hY : P Y
hf : P.isColocal f
⊢ IsIso f
have mp : ∀ (g : Y ⟶ X) (hg : Eq.{v_1 + 1} (α := Y ⟶ Y) ((fun (f_1 : Y ⟶ X) ↦ f_1 ≫ f) g) (𝟙 Y)), IsIso f
Tactic: obtain ⟨g, hg⟩ := (hf _ hY).2 (𝟙 Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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 (β := 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
have 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)
Tactic: convert!
    ((Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm.trans
        (adj.homEquiv X Y)).bijective using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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 (α := ((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)
have 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))
Tactic: dsimp [Adjunction.homEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (hypothesis)
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
⊢ isLocal (fun (x : D) ↦ x ∈ Set.range F.obj) f ↔ IsIso (G.map f)
have this : Functor.map (𝟭 D) f ≫ adj.unit.app Y = adj.unit.app X ≫ (G ⋙ F).map f
Tactic: have := adj.unit.naturality f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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)
⊢ isLocal (fun (x : D) ↦ x ∈ Set.range F.obj) f ↔ IsIso (G.map f)
have rw : IsIso (F.map (G.map 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⟩]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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
⊢ (isLocal fun (x : D) ↦ x ∈ Set.range F.obj) = MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G
have h : ∀ ⦃P₁ P₂ : D⦄ (f : P₁ ⟶ P₂),
  isLocal (fun (x : D) ↦ x ∈ Set.range F.obj) f ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G f
Tactic: ext P₁ P₂ f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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₂
⊢ isLocal (fun (x : D) ↦ x ∈ Set.range F.obj) f ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G f
have h : IsIso (G.map f) ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G f
Tactic: rw [isLocal_iff_isIso_map adj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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 (isLocal fun (x : D) ↦ x ∈ Set.range F.obj)
have rw : G.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms C) G)
Tactic: rw [isLocal_eq_inverseImage_isomorphisms adj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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 ⟶ 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
have 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)
Tactic: convert!
    ((Functor.FullyFaithful.ofFullyFaithful G).homEquiv.symm.trans
        (adj.homEquiv Y X).symm).bijective using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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)
⊢ 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)
have 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))
Tactic: dsimp [Adjunction.homEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (hypothesis)
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
⊢ isColocal (fun (x : C) ↦ x ∈ Set.range G.obj) f ↔ IsIso (F.map f)
have this : (F ⋙ G).map f ≫ adj.counit.app Y = adj.counit.app X ≫ Functor.map (𝟭 C) f
Tactic: have := adj.counit.naturality f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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
⊢ isColocal (fun (x : C) ↦ x ∈ Set.range G.obj) f ↔ IsIso (F.map f)
have rw : IsIso (G.map (F.map 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⟩]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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
⊢ (isColocal fun (x : C) ↦ x ∈ Set.range G.obj) = MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F
have h : ∀ ⦃P₁ P₂ : C⦄ (f : P₁ ⟶ P₂),
  isColocal (fun (x : C) ↦ x ∈ Set.range G.obj) f ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F f
Tactic: ext P₁ P₂ f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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
P₁ P₂ : C
f : P₁ ⟶ P₂
⊢ isColocal (fun (x : C) ↦ x ∈ Set.range G.obj) f ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F f
have h : IsIso (F.map f) ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F f
Tactic: rw [isColocal_iff_isIso_map adj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
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
⊢ F.IsLocalization (isColocal fun (x : C) ↦ x ∈ Set.range G.obj)
have rw : F.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F)
Tactic: rw [isColocal_eq_inverseImage_isomorphisms adj]
-- 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 ≤ P.isLocal.isLocal
have rw : P.isLocal ≤ P.isLocal
Tactic: rw [← le_isLocal_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
⊢ W ≤ W.isLocal.isLocal
have rw : W.isLocal ≤ W.isLocal
Tactic: rw [ObjectProperty.le_isLocal_iff]
-- 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 ≤ P.isColocal.isColocal
have rw : P.isColocal ≤ P.isColocal
Tactic: rw [← le_isColocal_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Bousfield (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
⊢ W ≤ W.isColocal.isColocal
have rw : W.isColocal ≤ W.isColocal
Tactic: rw [ObjectProperty.le_isColocal_iff]