awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
mp : L.map f₁ = L.map f₂ → ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂
⊢ L.map f₁ = L.map f₂ ↔ ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂
have mpr : (∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂) → L.map f₁ = L.map f₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
h : L.map f₁ = L.map f₂
⊢ ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂
have h₁ : RightFractionRel (W := W) (RightFraction.ofHom W f₁) (RightFraction.ofHom W f₂)
Tactic: rw [← RightFraction.map_ofHom W _ L (Localization.inverts _ _),
      ← RightFraction.map_ofHom W _ L (Localization.inverts _ _),
      RightFraction.map_eq_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
h : RightFractionRel (W := W) (RightFraction.ofHom W f₁) (RightFraction.ofHom W f₂)
⊢ ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂
have mp : ∀ (Z_1 : C) (t₁ : Z_1 ⟶ (RightFraction.ofHom W f₁).X' (W := W)) (t₂ : Z_1 ⟶ (RightFraction.ofHom W f₂).X' (W := W))
  (hst : t₁ ≫ (RightFraction.ofHom W f₁).s (W := W) = t₂ ≫ (RightFraction.ofHom W f₂).s (W := W))
  (hft : t₁ ≫ (RightFraction.ofHom W f₁).f (W := W) = t₂ ≫ (RightFraction.ofHom W f₂).f (W := W))
  (ht : W (t₁ ≫ (RightFraction.ofHom W f₁).s (W := W))), ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂
Tactic: obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
f : Arrow.{v_2, u_2} D
⊢ L.mapArrow.essImage f
have this : L.op.mapArrow.EssSurj
Tactic: have := Localization.essSurj_mapArrow L.op W.op
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.op.mapArrow.EssSurj
⊢ L.mapArrow.essImage f
have obtain : ∀ (g : Arrow.{v_1, u_1} Cᵒᵖ) (e : L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op), L.mapArrow.essImage f
Tactic: obtain ⟨g, ⟨e⟩⟩ : ∃ (g : _), Nonempty (L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op) :=
      ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} E
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
h₁ : StrictUniversalPropertyFixedTarget.{v₁, u₁, v₂, u₂, v₄, u₄} L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget.{v₂, u₂, v₃, u₃, v₄, u₄} L₂ W₂ E
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : Functor.{v₁, v₄, u₁, u₄} C₁ E
hF : W₃.IsInvertedBy F
⊢ W₂.IsInvertedBy (h₁.lift (W := W₁) F ⋯)
have refine : (W₃.map L₁).IsInvertedBy (h₁.lift (W := W₁) F sorry)
Tactic: refine MorphismProperty.IsInvertedBy.of_le _ _ _ ?_ hW₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} E
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
h₁ : StrictUniversalPropertyFixedTarget.{v₁, u₁, v₂, u₂, v₄, u₄} L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget.{v₂, u₂, v₃, u₃, v₄, u₄} L₂ W₂ E
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : Functor.{v₁, v₄, u₁, u₄} C₁ E
hF : W₃.IsInvertedBy F
⊢ (L₁ ⋙ L₂) ⋙ h₂.lift (W := W₂) (h₁.lift (W := W₁) F ⋯) ⋯ = F
have rw : L₁ ⋙ L₂ ⋙ h₂.lift (W := W₂) (h₁.lift (W := W₁) F sorry) sorry = F
Tactic: rw [Functor.assoc, h₂.fac, h₁.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} E
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
h₁ : StrictUniversalPropertyFixedTarget.{v₁, u₁, v₂, u₂, v₄, u₄} L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget.{v₂, u₂, v₃, u₃, v₄, u₄} L₂ W₂ E
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : Functor.{v₁, v₄, u₁, u₄} C₁ E
hF : W₃.IsInvertedBy F
rw : L₁ ⋙ L₂ ⋙ h₂.lift (W := W₂) (h₁.lift (W := W₁) F ⋯) ⋯ = F
⊢ (L₁ ⋙ L₂) ⋙ h₂.lift (W := W₂) (h₁.lift (W := W₁) F ⋯) ⋯ = F
have rw₁ : L₁ ⋙ h₁.lift (W := W₁) F sorry = F
Tactic: rw [Functor.assoc, h₂.fac, h₁.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} E
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
h₁ : StrictUniversalPropertyFixedTarget.{v₁, u₁, v₂, u₂, v₄, u₄} L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget.{v₂, u₂, v₃, u₃, v₄, u₄} L₂ W₂ E
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : Functor.{v₁, v₄, u₁, u₄} C₁ E
hF : W₃.IsInvertedBy F
rw : L₁ ⋙ L₂ ⋙ h₂.lift (W := W₂) (h₁.lift (W := W₁) F ⋯) ⋯ = F
rw₁ : L₁ ⋙ h₁.lift (W := W₁) F ⋯ = F
⊢ (L₁ ⋙ L₂) ⋙ h₂.lift (W := W₂) (h₁.lift (W := W₁) F ⋯) ⋯ = F
have rw₂ : F = F
Tactic: rw [Functor.assoc, h₂.fac, h₁.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
⊢ W₂ ≤ W₂'.inverseImage E₂.functor
have eq : (W₂.isoClosure.map E₂.functor).inverseImage E₂.functor = W₂.isoClosure
Tactic: have eq := W₂.isoClosure.inverseImage_map_eq_of_isEquivalence E₂.functor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
eq : (W₂.isoClosure.map E₂.functor).inverseImage E₂.functor = W₂.isoClosure
⊢ W₂ ≤ W₂'.inverseImage E₂.functor
have eq₁ : (W₂.map E₂.functor).inverseImage E₂.functor = W₂.isoClosure
Tactic: rw [MorphismProperty.map_isoClosure] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
eq : (W₂.map E₂.functor).inverseImage E₂.functor = W₂.isoClosure
⊢ W₂ ≤ W₂'.inverseImage E₂.functor
have rw : W₂ ≤ W₂.isoClosure
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
⊢ (L₁ ⋙ L₂).IsLocalization W₃
have this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
Tactic: have := LocalizerMorphism.IsLocalizedEquivalence.of_equivalence Φ (by rfl)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
⊢ (L₁ ⋙ L₂).IsLocalization W₃
have hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
Tactic: have hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q) := by
    simpa only [← MorphismProperty.IsInvertedBy.iff_comp _ _ E₃.inverse,
      MorphismProperty.IsInvertedBy.iff_of_iso W₃ iso] using hW₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
⊢ (L₁ ⋙ L₂).IsLocalization W₃
have hW₂₃' : W₂' ≤ W₃.map W₁.Q
Tactic: have hW₂₃' : W₂' ≤ W₃.map W₁.Q := (MorphismProperty.monotone_map E₂.functor hW₂₃).trans
    (by simpa only [W₃.map_map]
      using le_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
⊢ (W₁.Q ⋙ W₂'.Q).IsLocalization W₃
have refine_1 : StrictUniversalPropertyFixedTarget (W₁.Q ⋙ W₂'.Q) W₃ W₂'.Localization
Tactic: refine IsLocalization.mk' _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
refine_1 : StrictUniversalPropertyFixedTarget (W₁.Q ⋙ W₂'.Q) W₃ W₂'.Localization
⊢ (W₁.Q ⋙ W₂'.Q).IsLocalization W₃
have refine_2 : StrictUniversalPropertyFixedTarget (W₁.Q ⋙ W₂'.Q) W₃ W₃.Localization
Tactic: refine IsLocalization.mk' _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
⊢ (L₁ ⋙ L₂).IsLocalization W₃
have this₁ : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃
Tactic: have : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃ := by
    refine IsLocalization.mk' _ _ ?_ ?_
    all_goals
      exact (StrictUniversalPropertyFixedTarget.comp
        (strictUniversalPropertyFixedTargetQ W₁ _)
        (strictUniversalPropertyFixedTargetQ W₂' _) W₃ hW₃' hW₁₃ hW₂₃')
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₁, u₁} C₁
inst_3 : L₁.IsLocalization W₁
inst_4 : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
⊢ W₂ ≤ W₃.map L₁
have rw : W₃.map L₁ ≤ W₃.map L₁
Tactic: rw [hW₂₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Composition (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₁, u₁} C₁
inst_3 : L₁.IsLocalization W₁
inst_4 : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
⊢ L₂.IsLocalization W₂
have this : (L₁ ⋙ W₂.Q).IsLocalization W₃
Tactic: have : (L₁ ⋙ W₂.Q).IsLocalization W₃ :=
      comp L₁ W₂.Q W₁ W₂ W₃ (fun X Y f hf => Localization.inverts W₂.Q W₂ _
        (by simpa only [hW₂₃] using W₃.map_mem_map _ _ hf)) hW₁₃
        (by rw [hW₂₃])
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (hypothesis)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X Y : LocQuiver W
g : Y.obj (W := W) ⟶ X.obj (W := W)
hg : W g
⊢ G.obj (X.obj (W := W)) ⟶ G.obj (Y.obj (W := W))
have this : IsIso (G.map g)
Tactic: haveI := hG g hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X Y : C
f₁ f₂ : Quiver.Hom (V := Paths (LocQuiver W)) (LocQuiver.mk (W := W) X) (LocQuiver.mk (W := W) Y)
r : relations W f₁ f₂
⊢ (liftToPathCategory (W := W) G hG).map f₁ = (liftToPathCategory (W := W) G hG).map f₂
have id : ∀ ⦃X_1 Y : Paths (LocQuiver W)⦄,
  (liftToPathCategory (W := W) G hG).map (ψ₁ W (𝟙 X)) = (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X))
Tactic: rcases r with ⟨⟩
Cleared hypotheses: Y, f₁, f₂, r
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X Y : C
f₁ f₂ : Quiver.Hom (V := Paths (LocQuiver W)) (LocQuiver.mk (W := W) X) (LocQuiver.mk (W := W) Y)
r : relations W f₁ f₂
id :
  ∀ ⦃X_1 Y : Paths (LocQuiver W)⦄,
    (liftToPathCategory (W := W) G hG).map (ψ₁ W (𝟙 X)) = (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X))
⊢ (liftToPathCategory (W := W) G hG).map f₁ = (liftToPathCategory (W := W) G hG).map f₂
have comp : ∀ ⦃X_1 Y_1 : Paths (LocQuiver W)⦄ {Y_2 : C} (f : X ⟶ Y_2) (g : Y_2 ⟶ Y),
  (liftToPathCategory (W := W) G hG).map (ψ₁ W (f ≫ g)) = (liftToPathCategory (W := W) G hG).map (ψ₁ W f ≫ ψ₁ W g)
Tactic: rcases r with ⟨⟩
Cleared hypotheses: f₁, f₂, r