awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
E_1 : Type u_3
inst_2 : Category.{v_3, u_3} E_1
inst_3 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_4 : L.IsLocalization W
E : Type u_4
inst_5 : Category.{v_4, u_4} E
this : Full (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)
⊢ FullyFaithful (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)
have this₁ : Faithful (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)
Tactic: have := faithful_whiskeringLeft L W E
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), Eq (α := F₁.obj (L.obj X) ⟶ F₂.obj (L.obj X)) (τ.app (L.obj X)) (τ'.app (L.obj X))
⊢ τ = τ'
have this : L.EssSurj
Tactic: haveI := essSurj L W
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), Eq (α := F₁.obj (L.obj X) ⟶ F₂.obj (L.obj X)) (τ.app (L.obj X)) (τ'.app (L.obj X))
this : L.EssSurj
⊢ τ = τ'
have w : ∀ (Y : D), τ.app Y = τ'.app Y
Tactic: ext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), Eq (α := F₁.obj (L.obj X) ⟶ F₂.obj (L.obj X)) (τ.app (L.obj X)) (τ'.app (L.obj X))
this : L.EssSurj
Y : D
⊢ τ.app Y = τ'.app Y
have w : Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y) (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ.app Y)
  (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ'.app Y)
Tactic: rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), Eq (α := F₁.obj (L.obj X) ⟶ F₂.obj (L.obj X)) (τ.app (L.obj X)) (τ'.app (L.obj X))
this : L.EssSurj
Y : D
w :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y) (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ.app Y)
    (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ'.app Y)
⊢ τ.app Y = τ'.app Y
have w₁ : Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y)
  (τ.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
  (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ'.app Y)
Tactic: rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), Eq (α := F₁.obj (L.obj X) ⟶ F₂.obj (L.obj X)) (τ.app (L.obj X)) (τ'.app (L.obj X))
this : L.EssSurj
Y : D
w :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y) (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ.app Y)
    (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ'.app Y)
w₁ :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y)
    (τ.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
    (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ'.app Y)
⊢ τ.app Y = τ'.app Y
have w₂ : Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y)
  (τ.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
  (τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
Tactic: rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), Eq (α := F₁.obj (L.obj X) ⟶ F₂.obj (L.obj X)) (τ.app (L.obj X)) (τ'.app (L.obj X))
this : L.EssSurj
Y : D
w :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y) (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ.app Y)
    (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ'.app Y)
w₁ :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y)
    (τ.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
    (F₁.map (Iso.hom (L.objObjPreimageIso Y)) ≫ τ'.app Y)
w₂ :
  Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y)
    (τ.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
    (τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
⊢ τ.app Y = τ'.app Y
have w₃ : Eq (α := F₁.obj (L.obj (L.objPreimage Y)) ⟶ F₂.obj Y)
  (τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
  (τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (Iso.hom (L.objObjPreimageIso Y)))
Tactic: rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F : Functor.{v_1, v_3, u_1, u_3} C E
F' : Functor.{v_2, v_3, u_2, u_3} D E
h : Lifting L W F F'
X : C
⊢ Eq (α := F'.obj (L.obj X) ⟶ F'.obj (L.obj X)) ((liftNatTrans L W F F F' F' (𝟙 F)).app (L.obj X))
    (NatTrans.app (𝟙 F') (L.obj X))
have simp : Eq.{v_3 + 1} (α := F'.obj (L.obj X) ⟶ F'.obj (L.obj X)) (𝟙 ((L ⋙ F').obj X)) (𝟙 (F'.obj (L.obj X)))
Tactic: simp only [liftNatTrans_app, NatTrans.id_app, id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
W : MorphismProperty.{v_1, u_1} C
L₁ L₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : L₁ ≅ L₂
inst_2 : L₁.IsLocalization W
⊢ L₂.IsLocalization W
have h : W.IsInvertedBy L₁
Tactic: have h := Localization.inverts L₁ W
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
W : MorphismProperty.{v_1, u_1} C
L₁ L₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : L₁ ≅ L₂
inst_2 : L₁.IsLocalization W
h : W.IsInvertedBy L₁
⊢ L₂.IsLocalization W
have h₁ : W.IsInvertedBy L₂
Tactic: rw [MorphismProperty.IsInvertedBy.iff_of_iso W e] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
E : Type u_4
inst_2 : Category.{v_4, u_4} E
L' : Functor.{v_1, v_4, u_1, u_4} C E
eq : Equivalence.{v_2, v_4, u_2, u_4} D E
inst_3 : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy L'
have rw : W.IsInvertedBy (L ⋙ eq.functor)
Tactic: rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
E : Type u_4
inst_2 : Category.{v_4, u_4} E
L' : Functor.{v_1, v_4, u_1, u_4} C E
eq : Equivalence.{v_2, v_4, u_2, u_4} D E
inst_3 : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ L'.IsLocalization W
have h : W.IsInvertedBy L'
Tactic: have h : W.IsInvertedBy L' := by
    rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]
    exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
hW : W ≤ MorphismProperty.isomorphisms C
inst_2 : L.IsEquivalence
⊢ L.IsLocalization W
have this : IsLocalization (𝟭 C) W
Tactic: haveI : (𝟭 C).IsLocalization W := for_id W hW
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ P.inverseImage (uniq W.Q L W).functor (Construction.wInv (W := W) f hf)
have refine : (e.app Y).hom ≫ (Arrow.mk (isoOfHom L W f hf).inv).hom =
  (Arrow.mk ((uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf))).hom ≫ (e.app X).hom
Tactic: refine (P.arrow_mk_iso_iff (Arrow.isoMk (e.app _) (e.app _) ?_)).2 (h₂ f hf)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ (e.app Y).hom ≫ (Arrow.mk (isoOfHom L W f hf).inv).hom =
    (Arrow.mk ((uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf))).hom ≫ (e.app X).hom
have dsimp : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
have rw : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
Tactic: rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
rw : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
have rw₁ : (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
  ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
Tactic: rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
rw : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
rw₁ :
  (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
have rw₂ : e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
  ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
Tactic: rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
rw : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
rw₁ :
  (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₂ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
have rw₃ : e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
  (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
Tactic: rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
rw : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
rw₁ :
  (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₂ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₃ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
have rw₄ : e.hom.app Y ≫ 𝟙 (L.1 Y) = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
Tactic: rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
rw : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
rw₁ :
  (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₂ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₃ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
rw₄ :
  e.hom.app Y ≫ 𝟙 (L.1 Y) = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
have rw₅ : e.hom.app Y = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
Tactic: rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
rw : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
rw₁ :
  (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₂ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₃ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
rw₄ :
  e.hom.app Y ≫ 𝟙 (L.1 Y) = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
rw₅ : e.hom.app Y = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
have rw₆ : e.hom.app Y = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ L.map f
Tactic: rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (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
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
rw : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
rw₁ :
  (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₂ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₃ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
rw₄ :
  e.hom.app Y ≫ 𝟙 (L.1 Y) = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
rw₅ : e.hom.app Y = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
rw₆ : e.hom.app Y = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ L.map f
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
have rw₇ : e.hom.app Y = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ (W.Q ⋙ (uniq W.Q L W).functor).map f ≫ e.hom.app Y
Tactic: rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]