mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_2.refine_3
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
⊢ IsColimit { pt := Y, ι := Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X) }

pp: case refine_2.refine_4
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ P ({ app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j)

pp: case refine_2.refine_5
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ { app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j ≫
      (Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)).app j =
    f

Tactic:
·

Goal state after:
case refine_2.refine_3
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
⊢ IsColimit { pt := Y, ι := Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X) }
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_2.refine_4
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ P ({ app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j)

pp: case refine_2.refine_5
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ { app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j ≫
      (Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)).app j =
    f

Tactic:
·

Goal state after:
case refine_2.refine_4
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ P ({ app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_2.refine_5
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ { app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j ≫
      (Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)).app j =
    f

Tactic:
·

Goal state after:
case refine_2.refine_5
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ { app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j ≫
      (Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)).app j =
    f
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ sourceLocalClosure K P f → ∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)

pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ (∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)) → sourceLocalClosure K P f

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ sourceLocalClosure K P f → ∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ map ((ι C V D).map f) (𝟙 ((ι C V D).obj (𝟙_ D))) ≫ (ι C V D).map (ρ_ Y✝).hom =
    (ι C V D).map (ρ_ X✝).hom ≫ (ι C V D).map f

Tactic:
rw [ι_map_rightUnitor_hom_eq_rightUnitor_hom, ι_map_rightUnitor_hom_eq_rightUnitor_hom]

Goal state after:
C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ map ((ι C V D).map f) (𝟙 ((ι C V D).obj (𝟙_ D))) ≫
      (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj Y✝)).hom =
    (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj X✝)).hom ≫ (ι C V D).map f
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
x✝ : P.ind f
J : Type u_1
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
⊢ IsColimit { pt := Z, ι := s ≫ (Functor.const J).map i }

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
x✝ : P.ind f
J : Type u_1
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ t.app j ≫ (s ≫ (Functor.const J).map i).app j = f ≫ i

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
x✝ : P.ind f
J : Type u_1
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
⊢ IsColimit { pt := Z, ι := s ≫ (Functor.const J).map i }
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
x✝ : P.ind f
J : Type u_1
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ t.app j ≫ (s ≫ (Functor.const J).map i).app j = f ≫ i

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
x✝ : P.ind f
J : Type u_1
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ t.app j ≫ (s ≫ (Functor.const J).map i).app j = f ≫ i
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ (∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W) ↔
    ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)

pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ P.underObj ≤ ObjectProperty.isFinitelyPresentable (Under X)

Tactic:
·

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ (∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W) ↔
    ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
⊢ ∃ W u v, u ≫ v = g ∧ P (p ≫ u)

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
⊢ ∃ W u v, u ≫ v = g ∧ P.underObj W

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
⊢ ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.comp.refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ K.morphismProperty (pullback.snd g (E.f i))

pp: case refine_1.comp.refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P (E.f i ≫ f)

Tactic:
·

Goal state after:
case refine_1.comp.refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ K.morphismProperty (pullback.snd g (E.f i))
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
⊢ ∃ W u v, u ≫ v = g ∧ P.underObj W

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
⊢ ∃ W u v, u ≫ v = g ∧ P.underObj W
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.comp.refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P (E.f i ≫ f)

Tactic:
·

Goal state after:
case refine_1.comp.refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P (E.f i ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ P.underObj ≤ ObjectProperty.isFinitelyPresentable (Under X)

Tactic:
·

Goal state after:
case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ P.underObj ≤ ObjectProperty.isFinitelyPresentable (Under X)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y✝ : C
f : X ⟶ Y✝
inst✝ : IsFinitelyAccessibleCategory (Under X)
Y : Under X
hY : P.underObj Y
⊢ ObjectProperty.isFinitelyPresentable (Under X) Y

Tactic:
exact H _ hY

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ sourceLocalClosure K P f → ∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)

pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ (∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)) → sourceLocalClosure K P f

Tactic:
· intro h
    induction h with
    | of f hf => exact ⟨.singleton (𝟙 _), K.mem_coverings_of_isIso _, fun U g ⟨⟩ ↦ by simpa⟩
    | of_iso f g e hf h =>
      obtain ⟨R, hR, h⟩ := h
      rw [K.mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      refine ⟨_, (E.pushforward e.hom.left (K.mem_coverings_of_isIso _)).mem₀, ?_⟩
      intro U v ⟨i⟩
      dsimp
      simp only [Category.assoc, Arrow.w_mk_right, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom]
      rw [← Category.assoc, P.cancel_right_of_respectsIso]
      exact h _ _ ⟨i⟩
    | comp f hf R hR g hg ih =>
      obtain ⟨S, hS, h⟩ := ih
      rw [K.mem_iff_exists_zeroHypercover] at hS hR
      obtain ⟨E, rfl⟩ := hS
      obtain ⟨F, rfl⟩ := hR
      refine ⟨(E.pullback₁ g).presieve₀, (E.pullback₁ g).mem₀, ?_⟩
      intro U v ⟨i⟩
      dsimp
      rw [pullback.condition_assoc]
      refine RespectsLeft.precomp (Q := K.morphismProperty) _ ?_ _ ?_
      · obtain ⟨j⟩ := hg
        exact (F.pullback₂ (E.f i)).morphismProperty j
      · exact h _ _ ⟨i⟩
    | of_presieve f R hR h ih =>
      rw [K.mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      choose S hS h' using fun i : E.I₀ ↦ ih _ _ ⟨i⟩
      simp_rw [K.mem_iff_exists_zeroHypercover] at hS
      choose F hF using hS
      refine ⟨_, (E.bind F).mem₀, fun U g ⟨j⟩ ↦ ?_⟩
      dsimp
      rw [Category.assoc]
      exact h' _ _ _ (by simp [hF])

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ (∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)) → sourceLocalClosure K P f
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ (∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)) → sourceLocalClosure K P f

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ (∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)) → sourceLocalClosure K P f
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ (MonoOver X)ᵒᵖ
⊢ IsFiltered.IsEventuallyConstant G

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ (MonoOver X)ᵒᵖ
⊢ IsFiltered.IsEventuallyConstant G
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: case refine_1
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
h : localEpi (fun x ↦ x ∈ Set.range G.obj) (G.map (F.map f))
Z : D
u v : F.obj Y ⟶ Z
huv : F.map f ≫ u = F.map f ≫ v
⊢ u = v

pp: case refine_2
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ Epi (F.map f) → localEpi (fun x ↦ x ∈ Set.range G.obj) (G.map (F.map f))

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
h : localEpi (fun x ↦ x ∈ Set.range G.obj) (G.map (F.map f))
Z : D
u v : F.obj Y ⟶ Z
huv : F.map f ≫ u = F.map f ≫ v
⊢ u = v