awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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 ≫ (uniq W.Q L W).functor.map (W.Q.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]
-- 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
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
rw₈ :
  e.hom.app Y =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ (uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y
⊢ 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.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]
-- 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
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
rw₈ :
  e.hom.app Y =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ (uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y
rw₉ : e.hom.app Y = (uniq W.Q L W).functor.map ((isoOfHom W.Q W f hf).inv ≫ W.Q.map f) ≫ e.hom.app Y
⊢ 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 (𝟙 (W.Q.obj Y)) ≫ 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]
-- 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
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
rw₈ :
  e.hom.app Y =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ (uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y
rw₉ : e.hom.app Y = (uniq W.Q L W).functor.map ((isoOfHom W.Q W f hf).inv ≫ W.Q.map f) ≫ e.hom.app Y
rw₁₀ : e.hom.app Y = (uniq W.Q L W).functor.map (𝟙 (W.Q.obj Y)) ≫ e.hom.app Y
⊢ 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.obj (W.Q.obj Y)) ≫ 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]
-- 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
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
rw₈ :
  e.hom.app Y =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ (uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y
rw₉ : e.hom.app Y = (uniq W.Q L W).functor.map ((isoOfHom W.Q W f hf).inv ≫ W.Q.map f) ≫ e.hom.app Y
rw₁₀ : e.hom.app Y = (uniq W.Q L W).functor.map (𝟙 (W.Q.obj Y)) ≫ e.hom.app Y
rw₁₁ : e.hom.app Y = 𝟙 ((uniq W.Q L W).functor.obj (W.Q.obj Y)) ≫ e.hom.app Y
⊢ 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 = 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]
-- 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
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
⊢ P = ⊤
have hP : P.inverseImage (uniq W.Q L W).functor = ⊤
Tactic: have hP : P.inverseImage (uniq W.Q L W).functor = ⊤ :=
    Construction.morphismProperty_eq_top _
      (fun _ _ f ↦ (P.arrow_mk_iso_iff
        (((Functor.mapArrowFunctor _ _).mapIso e).app (Arrow.mk f))).2 (h₁ f))
      (fun X Y f hf ↦ by
        refine (P.arrow_mk_iso_iff (Arrow.isoMk (e.app _) (e.app _) ?_)).2 (h₂ f hf)
        dsimp
        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
hP : P.inverseImage (uniq W.Q L W).functor = ⊤
⊢ P = ⊤
have rw : (P.inverseImage (uniq W.Q L W).functor).map (uniq W.Q L W).functor = ⊤
Tactic: rw [← P.map_inverseImage_eq_of_isEquivalence (uniq W.Q L W).functor, hP,
    MorphismProperty.map_top_eq_top_of_essSurj_of_full]
-- 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
hP : P.inverseImage (uniq W.Q L W).functor = ⊤
rw : (P.inverseImage (uniq W.Q L W).functor).map (uniq W.Q L W).functor = ⊤
⊢ P = ⊤
have rw₁ : MorphismProperty.map ⊤ (uniq W.Q L W).functor = ⊤
Tactic: rw [← P.map_inverseImage_eq_of_isEquivalence (uniq W.Q L W).functor, hP,
    MorphismProperty.map_top_eq_top_of_essSurj_of_full]
-- 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
hP : P.inverseImage (uniq W.Q L W).functor = ⊤
rw : (P.inverseImage (uniq W.Q L W).functor).map (uniq W.Q L W).functor = ⊤
rw₁ : MorphismProperty.map ⊤ (uniq W.Q L W).functor = ⊤
⊢ P = ⊤
have rw₂ : Eq (α := MorphismProperty.{v_2, u_2} D) ⊤ ⊤
Tactic: rw [← P.map_inverseImage_eq_of_isEquivalence (uniq W.Q L W).functor, hP,
    MorphismProperty.map_top_eq_top_of_essSurj_of_full]
-- 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
inst_2 : L.IsLocalization ⊤
⊢ IsGroupoid.{v_2, u_2} D
have rw : Eq (α := MorphismProperty.{v_2, u_2} D) (MorphismProperty.isomorphisms D) ⊤
Tactic: rw [isGroupoid_iff_isomorphisms_eq_top]
-- 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
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
⊢ W.Q.map f = W.Q.map g ↔ L.map f = L.map g
have mp : W.Q.map f = W.Q.map g → L.map f = L.map g
Tactic: constructor
-- 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
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
mp : W.Q.map f = W.Q.map g → L.map f = L.map g
⊢ W.Q.map f = W.Q.map g ↔ L.map f = L.map g
have mpr : L.map f = L.map g → W.Q.map f = W.Q.map g
Tactic: constructor
-- 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
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
⊢ L.map f = L.map g
have mp : e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map f ≫ e.hom.app Y =
  e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map g ≫ e.hom.app Y
Tactic: rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
-- 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
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
⊢ e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map f ≫ e.hom.app Y =
    e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map g ≫ e.hom.app Y
have mp : e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y =
  e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map g) ≫ e.hom.app Y
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
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
⊢ e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y =
    e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map g) ≫ e.hom.app Y
have mp : e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map g) ≫ e.hom.app Y =
  e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map g) ≫ e.hom.app Y
Tactic: rw [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
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
⊢ W.Q.map f = W.Q.map g
have mpr : e.inv.app X ≫ (L ⋙ (Localization.uniq L W.Q W).functor).map f ≫ e.hom.app Y =
  e.inv.app X ≫ (L ⋙ (Localization.uniq L W.Q W).functor).map g ≫ e.hom.app Y
Tactic: rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
-- 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
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
⊢ e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map f) ≫ e.hom.app Y =
    e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map g) ≫ e.hom.app Y
have mpr : e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map g) ≫ e.hom.app Y =
  e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map g) ≫ e.hom.app Y
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ F₁ = F₂
have h₁ : obj curry F₁ = obj curry F₂
Tactic: apply Functor.curry_obj_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ obj curry F₁ = obj curry F₂
have h₁ : W₁.Q ⋙ obj curry F₁ = W₁.Q ⋙ obj curry F₂
Tactic: apply Construction.uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ W₁.Q ⋙ obj curry F₁ = W₁.Q ⋙ obj curry F₂
have h₁ : (W₁.Q ⋙ obj curry F₁).flip = (W₁.Q ⋙ obj curry F₂).flip
Tactic: apply Functor.flip_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ (W₁.Q ⋙ obj curry F₁).flip = (W₁.Q ⋙ obj curry F₂).flip
have h₁ : W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip = W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip
Tactic: apply Construction.uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip = W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip
have h₁ : (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip).flip = (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip).flip
Tactic: apply Functor.flip_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip).flip = (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip).flip
have h₁ : obj uncurry (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip).flip = obj uncurry (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip).flip
Tactic: apply Functor.uncurry_obj_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
inst_5 : W₂.ContainsIdentities
hF : (W₁.prod W₂).IsInvertedBy F
x x_1 : C₁
f₁ : x ⟶ x_1
hf₁ : W₁ f₁
⊢ IsIso ((obj curry F).map f₁)
have this : ∀ (X₂ : C₂), IsIso (((obj curry F).map f₁).app X₂)
Tactic: haveI : ∀ (X₂ : C₂), IsIso (((curry.obj F).map f₁).app X₂) :=
      fun X₂ => hF _ ⟨hf₁, MorphismProperty.id_mem _ _⟩