awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
inst_3 : Category.{v_5, u_5} H
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
inst_4 : L₂.IsLocalization W₂
inst_5 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F G : Functor.{v_4, v_5, u_4, u_5} D₂ H
α : F ⟶ G
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
      (α.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
⊢ IsIso α
have this : ∀ (X₂ : D₂), IsIso (α.app X₂)
Tactic: have : ∀ (X₂ : D₂), IsIso (α.app X₂) := fun X₂ => by
      have := Φ.essSurj_of_hasLeftResolutions L₂
      rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]
      apply hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_5 : W₂'.RespectsIso
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_6 : T.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
Y₂ : D₂
⊢ Nonempty (B.RightResolution (W₁ := W₁') (W₂ := W₂') Y₂)
have obtain : ∀ (X₂ : C₂) (e : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂), Nonempty (B.RightResolution (W₁ := W₁') (W₂ := W₂') Y₂)
Tactic: obtain ⟨X₂, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := R.functor) Y₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_5 : W₂'.RespectsIso
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_6 : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
Y₂ : D₂
⊢ Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)
have obtain : ∀ (X₂ : C₂) (e : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂), Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)
Tactic: obtain ⟨X₂, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := R.functor) Y₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_8 : B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
⊢ Nonempty (T.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
have obtain : ∀ (X₁ : C₁) (e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')),
  Nonempty (T.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
Tactic: obtain ⟨X₁, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage L.functor ρ.X₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_8 : B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
X₁ : C₁
e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')
⊢ W₂
    (R.functor (W₁ := W₂) (W₂ := W₂').preimage
      (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁))
have simp : W₂' (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁)
Tactic: simp only [← R.inverseImage_eq, MorphismProperty.inverseImage_iff, Functor.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_8 : B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
X₁ : C₁
e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')
⊢ W₂' (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁)
have refine : Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁) ≅
  Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂'))
Tactic: refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_8 : B.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
⊢ Nonempty (T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
have obtain : ∀ (X₁ : C₁) (e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')),
  Nonempty (T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
Tactic: obtain ⟨X₁, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage L.functor ρ.X₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_8 : B.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
X₁ : C₁
e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')
⊢ W₂
    (R.functor (W₁ := W₂) (W₂ := W₂').preimage
      (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂')))
have simp : W₂' (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂'))
Tactic: simp only [← R.inverseImage_eq, MorphismProperty.inverseImage_iff, Functor.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_8 : B.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
X₁ : C₁
e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')
⊢ W₂' (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂'))
have refine : Arrow.mk (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂')) ≅
  Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂'))
Tactic: refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)
have mp : HasSmallLocalizedHom W X Y → Small.{w, v₂} (L.obj X ⟶ L.obj Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
mp : HasSmallLocalizedHom W X Y → Small.{w, v₂} (L.obj X ⟶ L.obj Y)
⊢ HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)
have mpr : Small.{w, v₂} (L.obj X ⟶ L.obj Y) → HasSmallLocalizedHom W X Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y
have rw : Small.{v₂, v₂} (L.obj X ⟶ L.obj Y)
Tactic: rw [hasSmallLocalizedHom_iff W L]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y'
have simp : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y')
Tactic: simp only [hasSmallLocalizedHom_iff W W.Q]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X Y'
have simp : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y')
Tactic: simp only [hasSmallLocalizedHom_iff W W.Q]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y
have simp : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y)
Tactic: simp only [hasSmallLocalizedHom_iff W W.Q]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
L' : Functor.{v₁, v₃, u₁, u₃} C D'
inst_4 : L'.IsLocalization W
G : Functor.{v₂, v₃, u₂, u₃} D D'
e : L ⋙ G ≅ L'
X Y : C
inst_5 : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (equiv W L' : (a : SmallHom W X Y) → L'.obj X ⟶ L'.obj Y)
      ((Equiv.symm (equiv W L) : (a : L.obj X ⟶ L.obj Y) → SmallHom W X Y) f) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y
have dsimp : (homEquiv W W.Q L' : (a : W.Q.obj X ⟶ W.Q.obj Y) → L'.obj X ⟶ L'.obj Y)
    ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
      ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y)
        ((homEquiv W L W.Q : (a : L.obj X ⟶ L.obj Y) → W.Q.obj X ⟶ W.Q.obj Y) f : W.Q.obj X ⟶ W.Q.obj Y))) =
  e.inv.app X ≫ G.map f ≫ e.hom.app Y
Tactic: dsimp [equiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
L' : Functor.{v₁, v₃, u₁, u₃} C D'
inst_4 : L'.IsLocalization W
G : Functor.{v₂, v₃, u₂, u₃} D D'
e : L ⋙ G ≅ L'
X Y : C
inst_5 : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W W.Q L' : (a : W.Q.obj X ⟶ W.Q.obj Y) → L'.obj X ⟶ L'.obj Y)
      ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
        ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y)
          ((homEquiv W L W.Q : (a : L.obj X ⟶ L.obj Y) → W.Q.obj X ⟶ W.Q.obj Y) f : W.Q.obj X ⟶ W.Q.obj Y))) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y
have rw : ((homEquiv W L L' : Equiv.{v₂ + 1, v₃ + 1} (L.obj X ⟶ L.obj Y) (L'.obj X ⟶ L'.obj Y)) :
      (a : L.obj X ⟶ L.obj Y) → L'.obj X ⟶ L'.obj Y)
    f =
  e.inv.app X ≫ G.map f ≫ e.hom.app Y
Tactic: rw [Equiv.symm_apply_apply, homEquiv_trans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y Z : C
inst_3 : HasSmallLocalizedHom W X Y
inst_4 : HasSmallLocalizedHom W Y Z
inst_5 : HasSmallLocalizedHom W X Z
α : SmallHom W X Y
β : SmallHom W Y Z
this_1 : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := ⋯
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := ⋯
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
    ((equiv W L : (a : SmallHom W X Z) → L.obj X ⟶ L.obj Z) (α.comp (W := W) β) : L.obj X ⟶ L.obj Z)
    (CategoryStruct.comp (Y := L.obj Y) ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y) α)
        ((equiv W L : (a : SmallHom W Y Z) → L.obj Y ⟶ L.obj Z) β) :
      L.obj X ⟶ L.obj Z)
have obtain : ∀ (α : W.Q.obj X ⟶ W.Q.obj Y),
  Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
    ((equiv W L : (a : SmallHom W X Z) → L.obj X ⟶ L.obj Z)
        (comp (W := W)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
              (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
            α)
          β) :
      L.obj X ⟶ L.obj Z)
    (CategoryStruct.comp (Y := L.obj Y)
        ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
              (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
            α))
        ((equiv W L : (a : SmallHom W Y Z) → L.obj Y ⟶ L.obj Z) β) :
      L.obj X ⟶ L.obj Z)
Tactic: obtain ⟨α, rfl⟩ := (equivShrink _).surjective α
Cleared hypotheses: α
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y Z : C
inst_3 : HasSmallLocalizedHom W X Y
inst_4 : HasSmallLocalizedHom W Y Z
inst_5 : HasSmallLocalizedHom W X Z
β : SmallHom W Y Z
this_1 : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := ⋯
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := ⋯
α : W.Q.obj X ⟶ W.Q.obj Y
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
    ((equiv W L : (a : SmallHom W X Z) → L.obj X ⟶ L.obj Z)
        (comp (W := W)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
              (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
            α)
          β) :
      L.obj X ⟶ L.obj Z)
    (CategoryStruct.comp (Y := L.obj Y)
        ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
              (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
            α))
        ((equiv W L : (a : SmallHom W Y Z) → L.obj Y ⟶ L.obj Z) β) :
      L.obj X ⟶ L.obj Z)
have obtain : ∀ (β : W.Q.obj Y ⟶ W.Q.obj Z),
  Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
    ((equiv W L : (a : SmallHom W X Z) → L.obj X ⟶ L.obj Z)
        (comp (W := W) (Y := Y)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
              (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
            α)
          ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
              (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
            β)) :
      L.obj X ⟶ L.obj Z)
    (CategoryStruct.comp (Y := L.obj Y)
        ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
              (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
            α))
        ((equiv W L : (a : SmallHom W Y Z) → L.obj Y ⟶ L.obj Z)
          ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
              (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
            β)) :
      L.obj X ⟶ L.obj Z)
Tactic: obtain ⟨β, rfl⟩ := (equivShrink _).surjective β
Cleared hypotheses: β
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y Z T : C
inst_1 : HasSmallLocalizedHom W X Y
inst_2 : HasSmallLocalizedHom W X Z
inst_3 : HasSmallLocalizedHom W X T
inst_4 : HasSmallLocalizedHom W Y Z
inst_5 : HasSmallLocalizedHom W Y T
inst_6 : HasSmallLocalizedHom W Z T
α : SmallHom W X Y
β : SmallHom W Y Z
γ : SmallHom W Z T
⊢ Eq (α := SmallHom W X T) (comp (W := W) (α.comp (W := W) β) γ) (α.comp (W := W) (β.comp (W := W) γ))
have a : Eq (α := W.Q.obj X ⟶ W.Q.obj T)
  ((equiv W W.Q : (a : SmallHom W X T) → W.Q.obj X ⟶ W.Q.obj T) (comp (W := W) (α.comp (W := W) β) γ) :
    W.Q.obj X ⟶ W.Q.obj T)
  ((equiv W W.Q : (a : SmallHom W X T) → W.Q.obj X ⟶ W.Q.obj T) (α.comp (W := W) (β.comp (W := W) γ)) :
    W.Q.obj X ⟶ W.Q.obj T)
Tactic: apply (equiv W W.Q).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
inst_3 : HasSmallLocalizedHom W X Y
inst_4 : HasSmallLocalizedHom W X Y
e : SmallHom W X Y
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Y)
    ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
        ((chgUniv (W := W) : (a : SmallHom W X Y) → SmallHom W X Y) e) :
      L.obj X ⟶ L.obj Y)
    ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y) e : L.obj X ⟶ L.obj Y)
have obtain : ∀ (f : W.Q.obj X ⟶ W.Q.obj Y),
  Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Y)
    ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
        ((chgUniv (W := W) : (a : SmallHom W X Y) → SmallHom W X Y)
          ((Equiv.symm (equiv W W.Q) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y) f : SmallHom W X Y)) :
      L.obj X ⟶ L.obj Y)
    ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
        ((Equiv.symm (equiv W W.Q) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y) f) :
      L.obj X ⟶ L.obj Y)
Tactic: obtain ⟨f, rfl⟩ := (equiv W W.Q).symm.surjective e
Cleared hypotheses: e