mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
⊢ ∃ A a, IsGalois A ∧ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a

Tactic:
obtain ⟨A, u, a, h1, h2, h3⟩ := fiber_in_connected_component F (selfProd F X)
    (mkSelfProdFib F X)

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ ∃ A a, IsGalois A ∧ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
X A : C
f : A ⟶ X
a : (F.obj A).obj
left✝ : IsGalois A
⊢ (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (t.app A)) a) =
    (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (s.app A)) a)

Tactic:
h A

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
X A : C
f : A ⟶ X
a : (F.obj A).obj
left✝ : IsGalois A
⊢ (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (s.app A)) a) =
    (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (s.app A)) a)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c : C
⊢ 𝟙 c ∈ discrete.arrows c c

Tactic:
by constructor

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (P.decompId_i ≫ P.complement.decompId_p) ≫ biprod.inr = 0

Tactic:
refine (?_ =≫ _).trans zero_comp

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ P.decompId_i ≫ P.complement.decompId_p = 0
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (P.complement.decompId_i ≫ P.decompId_p) ≫ biprod.inl = 0

Tactic:
refine (?_ =≫ _).trans zero_comp

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ P.complement.decompId_i ≫ P.decompId_p = 0
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
C : Type u_3
K : Type u_5
inst✝² : Category.{v_1, u_5} K
inst✝¹ : Category.{v_3, u_1} J
inst✝ : Category.{v_5, u_3} C
F F' : K ⥤ J
e : F ≅ F'
⊢ preservesLimit F = preservesLimit F'

Tactic:
by
  ext G
  simp_rw [preservesLimit_iff]
  exact ⟨fun h ↦ preservesLimit_of_iso_diagram _ e,
    fun h ↦ preservesLimit_of_iso_diagram _ e.symm⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst✝³ : Category.{v_1, u_5} K
inst✝² : Category.{v_2, u_6} K'
inst✝¹ : Category.{v_3, u_1} J
inst✝ : Category.{v_5, u_3} C
e : K ≌ K'
⊢ preservesLimitsOfShape K = preservesLimitsOfShape K'

Tactic:
ext G
  simp only [preservesLimitsOfShape_iff]
  exact ⟨fun _ ↦ preservesLimitsOfShape_of_equiv e _,
    fun _ ↦ preservesLimitsOfShape_of_equiv e.symm _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
| shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map (F.map g).unop ≫ c'.ι.app (op X) ≫ f)

Tactic:
shrinkYonedaEquiv_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
| (ConcreteCategory.hom ((c'.ι.app (op X) ≫ f).app (op (unop (F.1 X')))))
    (shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map (F.map g).unop))
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
⊢ Nonempty (IsLimit (P.mapCone c)) ↔ (MorphismProperty.single (coconePtToShrinkYoneda c hc')).isLocal P

Tactic:
rw [Types.isLimit_iff_bijective_sectionOfCone,
    MorphismProperty.isLocal_single_iff_bijective,
    ← Function.Bijective.of_comp_iff' (coconeCompShrinkYonedaHomEquiv hc').symm.bijective,
    ← Function.Bijective.of_comp_iff _ shrinkYonedaEquiv.bijective]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
⊢ Function.Bijective
      ((⇑(coconeCompShrinkYonedaHomEquiv hc').symm ∘ Types.sectionOfCone (P.mapCone c)) ∘ ⇑shrinkYonedaEquiv) ↔
    Function.Bijective fun g ↦ coconePtToShrinkYoneda c hc' ≫ g
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
⊢ weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.fst ≫ f =
    (weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.snd) ≫ g

Tactic:
weakEqualizer.condition

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
⊢ weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.snd ≫ g =
    (weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.snd) ≫ g
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : Mon (C ⥤ C)
X : C
⊢ η.app (M.X.obj X) ≫ μ.app X = 𝟙 ((𝟭 C).obj (M.X.obj X))

Tactic:
simpa [-MonObj.mul_one] using! congrArg (fun t ↦ t.app X) (mul_one M.X)

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
B : D
⊢ coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      coequalizer.desc ((adj.homEquiv (G.obj B) B).symm (𝟙 (G.obj B))) ⋯ =
    coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      coequalizer.desc (adj.counit.app B) ⋯

Tactic:
simp [Adjunction.homEquiv_counit]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ Q.X ◁ η ≫ P.X ◁ Q.actRight

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X Q.X (𝟙_ C)).hom

Tactic:
rw [← whiskerLeft_comp, actRight_one]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ (ρ_ Q.X).hom

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X Q.X (𝟙_ C)).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ▷ T.X ≫
    (α_ R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X).hom

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ actRight P Q

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| actLeft P Q

Tactic:
rw [associator_naturality_middle]

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X (P.X ⊗ Q.X) T.X).hom ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ actRight P Q

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| actLeft P Q
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
this : IsIso ((reflectorAdjunction i).unit.app (𝟙_ C)) := ofReflective._proof_1 i
⊢ (asEmptyCone (𝟙_ C)).pt ≅ (i.mapCone (asEmptyCone ((reflector i).obj (𝟙_ C)))).pt

Tactic:
exact asIso ((reflectorAdjunction i).unit.app (𝟙_ C))

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
⊢ ∃ c, Nonempty (f ⟶ p.toCostructuredArrow.obj c)

pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
j : J
g₁ g₂ : f ⟶ p.toCostructuredArrow.obj j
⊢ ∃ c' t, g₁ ≫ p.toCostructuredArrow.map t = g₂ ≫ p.toCostructuredArrow.map t

Tactic:
· obtain ⟨j, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit f.hom
    exact ⟨j, ⟨CostructuredArrow.homMk (ObjectProperty.homMk g)⟩⟩

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
j : J
g₁ g₂ : f ⟶ p.toCostructuredArrow.obj j
⊢ ∃ c' t, g₁ ≫ p.toCostructuredArrow.map t = g₂ ≫ p.toCostructuredArrow.map t
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
P : ObjectProperty D
F : C ⥤ D
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : F.IsEquivalence
X : C
x✝ : P.ind.inverseImage F X
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (F.obj X)
h : ∀ (i : J), P (pres.diag.obj i)
⊢ F.asEquivalence.inverse.obj (F.obj X) ≅ X

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
P : ObjectProperty D
F : C ⥤ D
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : F.IsEquivalence
X : C
x✝ : P.ind.inverseImage F X
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (F.obj X)
h : ∀ (i : J), P (pres.diag.obj i)
j : J
⊢ P.inverseImage F (((pres.map F.asEquivalence.inverse).ofIso ?refine_1).diag.obj j)

Tactic:
· exact (F.asEquivalence.unitIso.app X).symm

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
P : ObjectProperty D
F : C ⥤ D
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : F.IsEquivalence
X : C
x✝ : P.ind.inverseImage F X
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (F.obj X)
h : ∀ (i : J), P (pres.diag.obj i)
j : J
⊢ P.inverseImage F (((pres.map F.asEquivalence.inverse).ofIso (F.asEquivalence.unitIso.app X).symm).diag.obj j)
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
h : LeftHomotopy f g
⊢ Hom.left (f - g) - Hom.left 0 = u.hom ≫ h.hom

Tactic:
simp [← h.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
h : LeftHomotopy (f - g) 0
⊢ Hom.left f - Hom.left g = u.hom ≫ h.hom

Tactic:
simp [← h.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ f g : u ⟶ v
h : LeftHomotopy f g
⊢ Hom.left g - Hom.left f = u.hom ≫ (-h.hom)

Tactic:
simp [← h.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
h : RightHomotopy f g
⊢ Hom.right (f - g) - Hom.right 0 = h.hom ≫ v.hom

Tactic:
simp [← h.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
h : RightHomotopy (f - g) 0
⊢ Hom.right f - Hom.right g = h.hom ≫ v.hom

Tactic:
simp [← h.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ f g : u ⟶ v
h : RightHomotopy f g
⊢ Hom.right g - Hom.right f = (-h.hom) ≫ v.hom

Tactic:
simp [← h.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ : u ⟶ v
f g : v ⟶ w
h : RightHomotopy f g
e : u ⟶ v
⊢ Hom.right (e ≫ f) - Hom.right (e ≫ g) = (Hom.right e ≫ h.hom) ≫ w.hom

Tactic:
simp [← h.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g✝ : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
w : Arrow V
g : v ⟶ w
h : RightHomotopy (f ≫ g) 0
⊢ biprod.inr ≫ biprod.desc (Hom.left g) h.hom ≫ w.hom = biprod.inr ≫ (cokernel f).hom ≫ Hom.right g

Tactic:
simp [← h.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
⊢ biproduct.ι (fun a ↦ s (f a)) k ≫
      (fun z ↦ biproduct.matrix fun j k ↦ if h : f j = g k then z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩ ≫ eqToHom ⋯ else 0)
          ((fun z i j k ↦ eqToHom ⋯ ≫ biproduct.components z ↑k ↑j ≫ eqToHom ⋯) z) ≫
        biproduct.π (fun b ↦ s (g b)) j =
    biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j

Tactic:
simp only [biproduct.matrix_π, biproduct.ι_desc]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
⊢ (if h : f k = g j then (eqToHom ⋯ ≫ biproduct.components z k j ≫ eqToHom ⋯) ≫ eqToHom ⋯ else 0) =
    biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case pos
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 𝟙 (s (f b))

pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0

Tactic:
· cases h
    simp

Goal state after:
case neg
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ j_1,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩

Tactic:
rw [Finset.sum_eq_single j]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = j then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩

case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ j →
      ((if h : i = i then if h' : h ▸ j = b then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) =
        0

case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ j ∉ Finset.univ →
    ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j then eqToHom ⋯ else 0 else 0) =
      0
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
g₁ g₂ : Y ⟶ Z
h : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
⊢ g₁ = g₂

Tactic:
obtain ⟨j₁, g₁, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₁
      obtain ⟨j₂, g₂, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₂
      dsimp at h ⊢
      obtain ⟨j₃, u, v, huv⟩ :=
        IsCardinalPresentable.exists_eq_of_isColimit κ p.isColimit (f ≫ g₁) (f ≫ g₂)
          (by simpa)
      simp only [Category.assoc] at huv
      rw [← p.w u, ← p.w v, reassoc_of% ((p.prop_diag_obj j₃ _ hf).1 huv)]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: case refine_2
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
this : OrderTop ↑S := { top := ⟨m, ⋯⟩, le_top := ⋯ }
k : K
⊢ α k ≤ ⟨S, ⋯⟩

Tactic:
· simp only [← Subtype.coe_le_coe]
      exact subset_trans (Set.subset_iUnion_of_subset k (subset_refl _)) Set.subset_union_left

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
j : κ.ord.ToType
this : NoMaxOrder κ.ord.ToType
⊢ ¬IsMax j

Tactic:
exact not_isMax j

Goal state after: