awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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)
⊢ (liftToPathCategory (W := W) G hG).map f₁ = (liftToPathCategory (W := W) G hG).map f₂
have Winv₁ : ∀ ⦃X_1 Y : Paths (LocQuiver W)⦄ {Y : C} (w : X ⟶ Y) (hw : W w),
  (liftToPathCategory (W := W) G hG).map (ψ₁ W w ≫ ψ₂ W w hw) = (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))
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)
Winv₁ :
  ∀ ⦃X_1 Y : Paths (LocQuiver W)⦄ {Y : C} (w : X ⟶ Y) (hw : W w),
    (liftToPathCategory (W := W) G hG).map (ψ₁ W w ≫ ψ₂ W w hw) =
      (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X))
⊢ (liftToPathCategory (W := W) G hG).map f₁ = (liftToPathCategory (W := W) G hG).map f₂
have Winv₂ : ∀ ⦃X_1 Y : Paths (LocQuiver W)⦄ {X_2 : C} (w : X_2 ⟶ X) (hw : W w),
  (liftToPathCategory (W := W) G hG).map (ψ₂ W w hw ≫ ψ₁ W w) = (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 : X ⟶ Y
⊢ (W.Q ⋙ lift (W := W) G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have simp : (lift (W := W) G hG).map (W.Q.map f) = G.map f
Tactic: simp only [Functor.comp_map, eqToHom_refl, comp_id, id_comp]
-- 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 : X ⟶ Y
⊢ (lift (W := W) G hG).map (W.Q.map f) = G.map f
have dsimp : composePath (G.map f).toPath = G.map f
Tactic: dsimp [MorphismProperty.Q, Quot.liftOn, Quotient.functor]
-- 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 : X ⟶ Y
⊢ composePath (G.map f).toPath = G.map f
have rw : G.map f = G.map f
Tactic: rw [composePath_toPath]
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ G₁ = G₂
have refine_1 : ∀ (X : W.Localization), G₁.obj X = G₂.obj X
Tactic: refine Functor.ext ?_ ?_
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
refine_1 : ∀ (X : W.Localization), G₁.obj X = G₂.obj X
⊢ G₁ = G₂
have refine_2 : ∀ (X Y : W.Localization) (f : X ⟶ Y), G₁.map f = eqToHom sorry ≫ G₂.map f ≫ eqToHom sorry
Tactic: refine Functor.ext ?_ ?_
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
⊢ G₁ = G₂
have suffices : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
Tactic: suffices h' : Quotient.functor _ ⋙ G₁ = Quotient.functor _ ⋙ G₂ by
    refine Functor.ext ?_ ?_
    · rintro ⟨⟨X⟩⟩
      apply Functor.congr_obj h
    · rintro ⟨⟨X⟩⟩ ⟨⟨Y⟩⟩ ⟨f⟩
      apply Functor.congr_hom h'
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
⊢ Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
have refine_1 : (Quotient.functor (relations W) ⋙ G₁).obj = (Quotient.functor (relations W) ⋙ G₂).obj
Tactic: refine Paths.ext_functor ?_ ?_
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
refine_1 : (Quotient.functor (relations W) ⋙ G₁).obj = (Quotient.functor (relations W) ⋙ G₂).obj
⊢ Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
have refine_2 : ∀ (a b : LocQuiver W) (e : a ⟶ b),
  (Quotient.functor (relations W) ⋙ G₁).map e.toPath =
    eqToHom sorry ≫ (Quotient.functor (relations W) ⋙ G₂).map e.toPath ≫ eqToHom sorry
Tactic: refine Paths.ext_functor ?_ ?_
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
⊢ (Quotient.functor (relations W) ⋙ G₁).obj = (Quotient.functor (relations W) ⋙ G₂).obj
have refine_1 : ∀ (X : Paths (LocQuiver W)), (Quotient.functor (relations W) ⋙ G₁).obj X = (Quotient.functor (relations W) ⋙ G₂).obj X
Tactic: ext X
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X : Paths (LocQuiver W)
⊢ (Quotient.functor (relations W) ⋙ G₁).obj X = (Quotient.functor (relations W) ⋙ G₂).obj X
have refine_1 : ∀ (obj : C),
  (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) obj) =
    (Quotient.functor (relations W) ⋙ G₂).obj (LocQuiver.mk (W := W) obj)
Tactic: cases X
Cleared hypotheses: X
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw : W w
⊢ Eq (α :=
    (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) X) ⟶
      (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) Y))
    ((Quotient.functor (relations W) ⋙ G₁).map
      (Quiver.Hom.toPath
        (Sum.inr
          (Subtype.mk (p :=
            fun
              (f :
                LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
            W f) w hw))))
    (eqToHom ⋯ ≫
      (Quotient.functor (relations W) ⋙ G₂).map
          (Quiver.Hom.toPath
            (Sum.inr
              (Subtype.mk (p :=
                fun
                  (f :
                    LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶
                      LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
                W f) w hw))) ≫
        eqToHom ⋯)
have hw₁ : W.Q.map w = (wIso (W := W) w hw).hom
Tactic: have hw : W.Q.map w = (wIso w hw).hom := rfl
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
⊢ Eq (α :=
    (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) X) ⟶
      (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) Y))
    ((Quotient.functor (relations W) ⋙ G₁).map
      (Quiver.Hom.toPath
        (Sum.inr
          (Subtype.mk (p :=
            fun
              (f :
                LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
            W f) w hw_1))))
    (eqToHom ⋯ ≫
      (Quotient.functor (relations W) ⋙ G₂).map
          (Quiver.Hom.toPath
            (Sum.inr
              (Subtype.mk (p :=
                fun
                  (f :
                    LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶
                      LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
                W f) w hw_1))) ≫
        eqToHom ⋯)
have hw' : (W.Q ⋙ G₁).map w = eqToHom sorry ≫ (W.Q ⋙ G₂).map w ≫ eqToHom sorry
Tactic: have hw' := Functor.congr_hom h w
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
hw' : (W.Q ⋙ G₁).map w = eqToHom ⋯ ≫ (W.Q ⋙ G₂).map w ≫ eqToHom ⋯
⊢ Eq (α :=
    (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) X) ⟶
      (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) Y))
    ((Quotient.functor (relations W) ⋙ G₁).map
      (Quiver.Hom.toPath
        (Sum.inr
          (Subtype.mk (p :=
            fun
              (f :
                LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
            W f) w hw_1))))
    (eqToHom ⋯ ≫
      (Quotient.functor (relations W) ⋙ G₂).map
          (Quiver.Hom.toPath
            (Sum.inr
              (Subtype.mk (p :=
                fun
                  (f :
                    LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶
                      LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
                W f) w hw_1))) ≫
        eqToHom ⋯)
have hw'₁ : G₁.map (wIso (W := W) w hw_1).hom = eqToHom sorry ≫ G₂.map (wIso (W := W) w hw_1).hom ≫ eqToHom sorry
Tactic: simp only [Functor.comp_map, hw] at hw'
Cleared hypotheses: hw'
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
hw' : G₁.map (wIso (W := W) w hw_1).hom = eqToHom ⋯ ≫ G₂.map (wIso (W := W) w hw_1).hom ≫ eqToHom ⋯
⊢ Eq (α :=
    (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) X) ⟶
      (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) Y))
    ((Quotient.functor (relations W) ⋙ G₁).map
      (Quiver.Hom.toPath
        (Sum.inr
          (Subtype.mk (p :=
            fun
              (f :
                LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
            W f) w hw_1))))
    (eqToHom ⋯ ≫
      (Quotient.functor (relations W) ⋙ G₂).map
          (Quiver.Hom.toPath
            (Sum.inr
              (Subtype.mk (p :=
                fun
                  (f :
                    LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶
                      LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
                W f) w hw_1))) ≫
        eqToHom ⋯)
have refine_2 : G₁.obj (W.Q.obj Y) = G₂.obj (W.Q.obj Y)
Tactic: refine Functor.congr_inv_of_congr_hom _ _ _ ?_ ?_ hw'
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
hw' : G₁.map (wIso (W := W) w hw_1).hom = eqToHom ⋯ ≫ G₂.map (wIso (W := W) w hw_1).hom ≫ eqToHom ⋯
refine_2 : G₁.obj (W.Q.obj Y) = G₂.obj (W.Q.obj Y)
⊢ Eq (α :=
    (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) X) ⟶
      (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) Y))
    ((Quotient.functor (relations W) ⋙ G₁).map
      (Quiver.Hom.toPath
        (Sum.inr
          (Subtype.mk (p :=
            fun
              (f :
                LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
            W f) w hw_1))))
    (eqToHom ⋯ ≫
      (Quotient.functor (relations W) ⋙ G₂).map
          (Quiver.Hom.toPath
            (Sum.inr
              (Subtype.mk (p :=
                fun
                  (f :
                    LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶
                      LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
                W f) w hw_1))) ≫
        eqToHom ⋯)
have refine_2₁ : G₁.obj (W.Q.obj X) = G₂.obj (W.Q.obj X)
Tactic: refine Functor.congr_inv_of_congr_hom _ _ _ ?_ ?_ hw'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
⊢ P = ⊤
have h : ∀ (X Y : W.Localization) (f : X ⟶ Y), P f = ⊤ f
Tactic: funext X Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
⊢ P f = ⊤ f
have h : P f ↔ ⊤ f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
⊢ P f ↔ ⊤ f
have h : P f → ⊤ f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : P f → ⊤ f
⊢ P f ↔ ⊤ f
have h₁ : ⊤ f → P f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (hypothesis)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
⊢ P f
have this : G.Full
Tactic: haveI : G.Full := Quotient.full_functor _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this_1 : G.Full
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
⊢ P f
have rcases : ∀ (X : C) (f : Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X) ⟶ Y), ⊤ f → P f
Tactic: rcases X with ⟨⟨X⟩⟩
Cleared hypotheses: X, f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
Y : W.Localization
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this_1 : G.Full
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
X : C
f : Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X) ⟶ Y
h : ⊤ f
⊢ P f
have rcases : ∀ (Y : C)
  (f :
    Quiver.Hom (V := W.Localization) (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X))
      (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) Y))),
  ⊤ f → P f
Tactic: rcases Y with ⟨⟨Y⟩⟩
Cleared hypotheses: Y, f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
⊢ P f
have h : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
Tactic: suffices ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f) by
      rcases X with ⟨⟨X⟩⟩
      rcases Y with ⟨⟨Y⟩⟩
      simpa only [Functor.map_preimage] using this _ _ (G.preimage f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (p.cons g))
have h : P (G.map p' ≫ G.map g.toPath)
Tactic: rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map p' ≫ G.map g.toPath)
have h : P (G.map g.toPath)
Tactic: refine P.comp_mem _ _ hp ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map g.toPath)
have h : ∀ (g : X₂.obj (W := W) ⟶ X₃.obj (W := W)), P (X := G.obj X₂) (Y := G.obj X₃) (G.map (Quiver.Hom.toPath (Sum.inl g)))
Tactic: rcases g with (g | ⟨g, hg⟩)
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h_1 : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
h : ∀ (g : X₂.obj (W := W) ⟶ X₃.obj (W := W)), P (X := G.obj X₂) (Y := G.obj X₃) (G.map (Quiver.Hom.toPath (Sum.inl g)))
⊢ P (G.map g.toPath)
have h₁ : ∀ (g : X₃.obj (W := W) ⟶ X₂.obj (W := W)) (hg : W g),
  P (X := G.obj X₂) (Y := G.obj X₃)
    (G.map (Quiver.Hom.toPath (Sum.inr (Subtype.mk (p := fun (f : X₃.obj (W := W) ⟶ X₂.obj (W := W)) ↦ W f) g hg))))
Tactic: rcases g with (g | ⟨g, hg⟩)
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂ : Paths (LocQuiver W)
p : X₁ ⟶ X₂
⊢ P (G.map p)
have h : P (X := G.obj X₁) (G.map Quiver.Path.nil)
Tactic: induction p with
    | nil => simpa only [Functor.map_id] using hP₁ (𝟙 X₁.obj)
    | @cons X₂ X₃ p g hp =>
      let p' : X₁ ⟶ X₂ := p
      rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
      refine P.comp_mem _ _ hp ?_
      rcases g with (g | ⟨g, hg⟩)
      · apply hP₁
      · apply hP₂
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h_1 : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂ : Paths (LocQuiver W)
p : X₁ ⟶ X₂
h : P (X := G.obj X₁) (G.map Quiver.Path.nil)
⊢ P (G.map p)
have h₁ : ∀ {X₂ X₃ : Paths (LocQuiver W)} (p : Quiver.Path.{uC', uC} X₁ X₂) (g : X₂ ⟶ X₃) (hp : P (G.map p)), P (G.map (p.cons g))
Tactic: induction p with
    | nil => simpa only [Functor.map_id] using hP₁ (𝟙 X₁.obj)
    | @cons X₂ X₃ p g hp =>
      let p' : X₁ ⟶ X₂ := p
      rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
      refine P.comp_mem _ _ hp ?_
      rcases g with (g | ⟨g, hg⟩)
      · apply hP₁
      · apply hP₂
Cleared hypotheses: p