awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
have this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).IsLocalization W₁
Tactic: haveI : Functor.IsLocalization (Φ.functor ⋙ MorphismProperty.Q W₂) W₁ := by
    refine Functor.IsLocalization.of_equivalence_source W₂.Q W₂ (Φ.functor ⋙ W₂.Q) W₁
      (asEquivalence Φ.functor).symm ?_ (Φ.inverts W₂.Q)
      ((associator _ _ _).symm ≪≫ isoWhiskerRight ((Equivalence.unitIso _).symm) _ ≪≫
        leftUnitor _)
    erw [W₁.isoClosure.inverseImage_equivalence_functor_eq_map_inverse]
    rw [MorphismProperty.map_isoClosure]
    exact h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
⊢ IsIso (whiskerRight ε₁ W₁.Q)
have rw : ∀ (X : C₁), IsIso ((whiskerRight ε₁ W₁.Q).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence
have this : IsIso (whiskerRight ε₁ W₁.Q)
Tactic: have : IsIso (whiskerRight ε₁ W₁.Q) := by
      rw [NatTrans.isIso_iff_isIso_app]
      exact fun _ ↦ Localization.inverts W₁.Q W₁ _ (hε₁ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
⊢ IsIso (whiskerRight ε₂ W₂.Q)
have rw : ∀ (X : C₂), IsIso ((whiskerRight ε₂ W₂.Q).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence
have this₁ : IsIso (whiskerRight ε₂ W₂.Q)
Tactic: have : IsIso (whiskerRight ε₂ W₂.Q) := by
      rw [NatTrans.isIso_iff_isIso_app]
      exact fun _ ↦ Localization.inverts W₂.Q W₂ _ (hε₂ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this_1 : IsIso (whiskerRight ε₁ W₁.Q)
this : IsIso (whiskerRight ε₂ W₂.Q)
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence
have refine_1 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ Ψ.localizedFunctor (W₁ := W₂) (W₂ := W₁) W₂.Q W₁.Q ≅ W₁.Q
Tactic: refine (Localization.equivalence W₁.Q W₁ W₂.Q W₂ (Φ.functor ⋙ W₂.Q)
      (Φ.localizedFunctor W₁.Q W₂.Q)
      (Ψ.functor ⋙ W₁.Q) (Ψ.localizedFunctor W₂.Q W₁.Q) ?_ ?_).isEquivalence_functor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this_1 : IsIso (whiskerRight ε₁ W₁.Q)
this : IsIso (whiskerRight ε₂ W₂.Q)
refine_1 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ Ψ.localizedFunctor (W₁ := W₂) (W₂ := W₁) W₂.Q W₁.Q ≅ W₁.Q
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence
have refine_2 : (Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ W₁.Q) ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ≅ W₂.Q
Tactic: refine (Localization.equivalence W₁.Q W₁ W₂.Q W₂ (Φ.functor ⋙ W₂.Q)
      (Φ.localizedFunctor W₁.Q W₂.Q)
      (Ψ.functor ⋙ W₁.Q) (Ψ.localizedFunctor W₂.Q W₁.Q) ?_ ?_).isEquivalence_functor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_6 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
hG : G.FullyFaithful
⊢ Nonempty (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).FullyFaithful
have rw : Nonempty G.FullyFaithful
Tactic: rw [Φ.nonempty_fullyFaithful_iff W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) L₁ L₂ G]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
h : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
inst_7 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
⊢ Nonempty G.FullyFaithful
have rw : Nonempty (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).FullyFaithful
Tactic: rw [Φ.nonempty_fullyFaithful_iff L₁ L₂ G W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
x x_1 : C₁
f : x ⟶ x_1
hf : W₁ f
⊢ IsIso (L₁.map f)
have rw : IsIso (F.map (L₁.map f))
Tactic: rw [← isIso_iff_of_reflects_iso  _ F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
⊢ L₁.IsLocalization W₁
have h : W₁.IsInvertedBy L₁
Tactic: have h : W₁.IsInvertedBy L₁ := fun _ _ f hf ↦ by
    rw [← isIso_iff_of_reflects_iso  _ F]
    exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (Arrow.isoOfNatIso iso f)).1 (Localization.inverts L₂ W₂ _ (Φ.map _ hf))
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
⊢ L₁.IsLocalization W₁
have have : ∀ (hG : G.FullyFaithful), L₁.IsLocalization W₁
Tactic: have hG : G.FullyFaithful := Functor.FullyFaithful.ofCompFaithful
    (Φ.fullyFaithful W₁.Q L₂ (G ⋙ F))
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
⊢ L₁.IsLocalization W₁
have this₁ : G.Full
Tactic: have := hG.full
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this_1 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this : G.Full
⊢ L₁.IsLocalization W₁
have this₁ : G.Faithful
Tactic: have := hG.faithful
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this_1 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this_2 : G.Full
this : G.Faithful
⊢ L₁.IsLocalization W₁
have this₁ : G.EssSurj
Tactic: have : G.EssSurj :=
    ⟨fun X ↦ ⟨W₁.Q.obj (L₁.objPreimage X), ⟨e.app _ ≪≫ L₁.objObjPreimageIso X⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this_1 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this_2 : G.Full
this_3 : G.Faithful
this : G.EssSurj
⊢ L₁.IsLocalization W₁
have this₁ : G.IsEquivalence
Tactic: have : G.IsEquivalence := { }
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
⊢ W₂.arrow.inverseImage (Φ.arrow (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.arrow) (W₂ := W₂.arrow)) = W₁.arrow
have simp : W₂.arrow.inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).mapArrow =
  (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).arrow
Tactic: simp only [← Φ.inverseImage_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
⊢ W₂ ≤ W₁.inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).inv
have simp : W₂ ≤ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).inv
Tactic: simp only [← Φ.inverseImage_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
⊢ W₁.inverseImage (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) = W₂
have h : ∀ ⦃X Y : C₂⦄ (f : X ⟶ Y), W₁.inverseImage (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) f ↔ W₂ f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
⊢ W₁.inverseImage (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) f ↔ W₂ f
have h : (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage
    (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) f ↔
  W₂ f
Tactic: simp only [← Φ.inverseImage_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_3 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_4 : W₂.RespectsIso
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
have refine : ∀ (X Y : C₂) (f : X ⟶ Y) (hf : W₂ f), W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂)) f
Tactic: refine IsLocalizedEquivalence.of_equivalence _ (fun X Y f hf ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocalizerMorphism (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_3 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_4 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
hf : W₂ f
e : Arrow.mk (X := Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).objPreimage X)) (Y :=
    Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).objPreimage Y))
    (Φ.functor (W₁ := W₁) (W₂ := W₂).map
      (Φ.functor (W₁ := W₁) (W₂ := W₂).preimage
        (Iso.hom (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso X) ≫
          f ≫ Iso.inv (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso Y)))) ≅
  Arrow.mk f :=
  Arrow.isoMk (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso X)
    (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso Y) ⋯
⊢ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂)) f
have simp : (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).map (Φ.functor (W₁ := W₁) (W₂ := W₂)) f
Tactic: simp only [← Φ.inverseImage_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocallySmall (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
⊢ HasLocalization.{w, v₁, u₁} W
have this : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
Tactic: have : LocallySmall.{w} (InducedCategory _ L.obj) :=
    ⟨fun X Y ↦ small_of_injective InducedCategory.homEquiv.injective⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocallySmall (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
this : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : Functor.{v₁, v₂, u₁, u₁} C (InducedCategory D L.obj) :=
  { obj := fun (X : C) ↦ X, map := fun {X Y : C} (f : X ⟶ Y) ↦ InducedCategory.homMk (L.map f), map_id := ⋯,
    map_comp := ⋯ }
⊢ HasLocalization.{w, v₁, u₁} W
have this₁ : L.EssSurj
Tactic: have := Localization.essSurj L W
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocallySmall (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
this_1 : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : Functor.{v₁, v₂, u₁, u₁} C (InducedCategory D L.obj) :=
  { obj := fun (X : C) ↦ X, map := fun {X Y : C} (f : X ⟶ Y) ↦ InducedCategory.homMk (L.map f), map_id := ⋯,
    map_comp := ⋯ }
this : L.EssSurj
⊢ HasLocalization.{w, v₁, u₁} W
have this₁ : EssSurj.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
Tactic: have : (inducedFunctor L.obj).EssSurj := ⟨fun Y ↦ ⟨_, ⟨L.objObjPreimageIso Y⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocallySmall (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
this_1 : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : Functor.{v₁, v₂, u₁, u₁} C (InducedCategory D L.obj) :=
  { obj := fun (X : C) ↦ X, map := fun {X Y : C} (f : X ⟶ Y) ↦ InducedCategory.homMk (L.map f), map_id := ⋯,
    map_comp := ⋯ }
this_2 : L.EssSurj
this : EssSurj.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
⊢ HasLocalization.{w, v₁, u₁} W
have this₁ : IsEquivalence.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
Tactic: have : (inducedFunctor L.obj).IsEquivalence := { }
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.LocallySmall (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
this_1 : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : Functor.{v₁, v₂, u₁, u₁} C (InducedCategory D L.obj) :=
  { obj := fun (X : C) ↦ X, map := fun {X Y : C} (f : X ⟶ Y) ↦ InducedCategory.homMk (L.map f), map_id := ⋯,
    map_comp := ⋯ }
this_2 : L.EssSurj
this_3 : EssSurj.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
this : IsEquivalence.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
e : Equivalence.{v₂, v₂, u₁, u₂} (InducedCategory D L.obj) D := asEquivalence (inducedFunctor L.obj)
e' : (L' ⋙ e.functor) ⋙ e.inverse ≅ L' :=
  L'.associator e.functor e.inverse ≪≫ L'.isoWhiskerLeft e.unitIso.symm ≪≫ L'.rightUnitor
⊢ HasLocalization.{w, v₁, u₁} W
have this₁ : L'.IsLocalization W
Tactic: have : L'.IsLocalization W :=
    Functor.IsLocalization.of_iso W (L₁ := L ⋙ e.inverse) e'