mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
⊢ { l //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }

Tactic:
let hcᵢ := isLimitOfPreserves (Over.forget _ ⋙ (evaluation _ _).obj i) hc

Goal state after:
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
⊢ { l //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ #(X ⟶ yp) ≤ α

Tactic:
apply Cardinal.mk_le_of_injective _

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ (X ⟶ yp) → md

C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ Function.Injective ?m.137
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
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_4, u_2} J'
inst✝¹ : Category.{v_5, u_3} C
inst✝ : Category.{v_6, u_4} D
⊢ (preservesLimitsOfShape K).IsClosedUnderIsomorphisms

Tactic:
rw [preservesLimitsOfShape_eq_iSup]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
eₗ : x.fst ≅ y.fst
eᵣ : x.snd ≅ y.snd
w : F.map eₗ.hom ≫ y.iso.hom = x.iso.hom ≫ G.map eᵣ.hom
⊢ F.map eₗ.inv ≫ x.iso.hom = y.iso.hom ≫ G.map eᵣ.inv

Tactic:
by simpa using F.map eₗ.inv ≫= w.symm =≫ G.map eᵣ.inv

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (Δ ≫ (f ≫ inv f ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: 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)
⊢ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q =
    (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
erw [map_π_preserves_coequalizer_inv_colimMap (tensorLeft _)]
  simp only [Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
ψ : G ⊗ H ⟶ H
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
X : C
⊢ ∀ n ∈ (monoidHom φ X).range, ∀ (g : X ⟶ G), g * n * g⁻¹ ∈ (monoidHom φ X).range

Tactic:
rintro - ⟨x, rfl⟩ z

Goal state after:
case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
ψ : G ⊗ H ⟶ H
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
X : C
x : X ⟶ H
z : X ⟶ G
⊢ z * (monoidHom φ X) x * z⁻¹ ∈ (monoidHom φ X).range
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Functor

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : LeftRigidCategory C
X : C
⊢ (ᘁ𝟙 X).op.mop = 𝟙 { unmop := op ᘁX }

Tactic:
simp [leftAdjointMate_id]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W
⊢ P.ind X

Tactic:
· let incl : P.FullSubcategory ⥤ (isFinitelyPresentable.{w} C).FullSubcategory :=
      ObjectProperty.ιOfLE H
    have H (d : CostructuredArrow (isFinitelyPresentable.{w} C).ι X) : ∃ c,
        Nonempty (d ⟶ (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X).obj c) := by
      obtain ⟨W, u, v, huv, hW⟩ := hfac d.hom
      exact ⟨CostructuredArrow.mk (Y := FullSubcategory.mk _ hW) v,
        ⟨CostructuredArrow.homMk ⟨u⟩ huv⟩⟩
    have : (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X).Final :=
      Functor.final_of_exists_of_isFiltered_of_fullyFaithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X) H
    have : IsFiltered (CostructuredArrow P.ι X) :=
      .of_exists_of_isFiltered_of_fullyFaithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X) H
    obtain ⟨hc⟩ : P.ι.isDenseAt X :=
      Functor.IsDenseAt.of_final (F := (isFinitelyPresentable.{w} C).ι) incl
        (Functor.IsDense.isDenseAt _ _)
    have : EssentiallySmall.{w} (CostructuredArrow P.ι X) :=
      essentiallySmall_of_fully_faithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X)
    exact of_essentiallySmall_index ⟨_, _, hc⟩ fun Y ↦ Y.left.2

Goal state after:
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)
a b c d : D
this✝³ : DayConvolution (((ι C V D).obj a ⊛ (ι C V D).obj b) ⊛ (ι C V D).obj c) ((ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D ((a ⊗ b) ⊗ c) d
this✝² : DayConvolution ((ι C V D).obj a ⊛ (ι C V D).obj b) ((ι C V D).obj c ⊛ (ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D (a ⊗ b) (c ⊗ d)
this✝¹ : DayConvolution ((ι C V D).obj a ⊛ (ι C V D).obj b ⊛ (ι C V D).obj c) ((ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D (a ⊗ b ⊗ c) d
this✝ : DayConvolution ((ι C V D).obj a) ((ι C V D).obj b ⊛ (ι C V D).obj c ⊛ (ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D a (b ⊗ c ⊗ d)
this : DayConvolution ((ι C V D).obj a) (((ι C V D).obj b ⊛ (ι C V D).obj c) ⊛ (ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D a ((b ⊗ c) ⊗ d)
⊢ map (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj b) ((ι C V D).obj c)).hom (𝟙 ((ι C V D).obj d)) ≫
      (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj (b ⊗ c)) ((ι C V D).obj d)).hom ≫
        map (𝟙 ((ι C V D).obj a))
          (DayConvolution.associator ((ι C V D).obj b) ((ι C V D).obj c) ((ι C V D).obj d)).hom =
    (DayConvolution.associator ((ι C V D).obj (a ⊗ b)) ((ι C V D).obj c) ((ι C V D).obj d)).hom ≫
      (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj b) ((ι C V D).obj (c ⊗ d))).hom

Tactic:
exact DayConvolution.pentagon
        (ι C V D |>.obj a) (ι C V D |>.obj b) (ι C V D |>.obj c) (ι C V D |>.obj d)

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w✝³ : SmallCategory J₁
w✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = ((Functor.const J₂).map f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Under j₁ ⥤ C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend
    h.isoPushout.inv
hc' : IsColimit c' :=
  IsColimit.extendIso h.isoPushout.inv
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
k l : Under j₁
a : k ⟶ l
h2 : s₁.app l.right = s₁.app k.right ≫ D₁.map (Under.Hom.right a)
⊢ ((Functor.const (Under j₁)).obj X).map a ≫ s₁.app l.right ≫ pushout.inl ((Under.post D₁).obj l).hom f' =
    (s₁.app k.right ≫ pushout.inl ((Under.post D₁).obj k).hom f') ≫ D'.map a

Tactic:
simp [h2, D']

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
n : ℕ
α : u ⟶ v
⊢ L.map (n • α.left) ≫ v.hom = u.hom ≫ R.map (n • α.right)

Tactic:
by simp [Functor.map_nsmul, Preadditive.comp_nsmul, Preadditive.nsmul_comp]

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

Goal state before:
pp: case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝.left = -((↑x✝¹ + 1) • x✝.left)

Tactic:
simp [add_nsmul, add_zsmul]

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

Goal state before:
pp: case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝.right = -((↑x✝¹ + 1) • x✝.right)

Tactic:
simp [add_nsmul, add_zsmul]

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

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)

Tactic:
fconstructor

Goal state after:
case mp
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 → Nonempty (X ≅ Y)

case mpr
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ Nonempty (X ≅ Y) → finrank 𝕜 (X ⟶ Y) = 1
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
h : x' ≤ y'
⊢ x ≤ y

Tactic:
obtain ⟨l₁, a₁, b₁, hl₁⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hx

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
h : x' ≤ y'
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a₁)) x' = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b₁)) x
⊢ x ≤ y
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun j k ↦
          L.map ((embedding C).map (f j k)) ≫ (α.app (Y✝.X k)).hom ≫ ((embeddingLiftIso F).symm.app (Y✝.X k)).hom) ≫
        (additiveObjIsoBiproduct (lift F) Y✝).inv =
    (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.map fun b ↦ (α.app (X✝.X b)).hom) ≫
        (biproduct.map fun b ↦ ((embeddingLiftIso F).symm.app (X✝.X b)).hom) ≫
          (additiveObjIsoBiproduct (lift F) X✝).inv ≫ (lift F).map f

Tactic:
simp only [additiveObjIsoBiproduct_naturality']

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun j k ↦
          L.map ((embedding C).map (f j k)) ≫ (α.app (Y✝.X k)).hom ≫ ((embeddingLiftIso F).symm.app (Y✝.X k)).hom) ≫
        (additiveObjIsoBiproduct (lift F) Y✝).inv =
    (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.map fun b ↦ (α.app (X✝.X b)).hom) ≫
        (biproduct.map fun b ↦ ((embeddingLiftIso F).symm.app (X✝.X b)).hom) ≫
          (biproduct.matrix fun i j ↦ (lift F).map ((embedding C).map (f i j))) ≫
            (additiveObjIsoBiproduct (lift F) Y✝).inv
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ IsCardinalPresentable J κ' ↔ HasCardinalLT (↑J.obj) κ'

Tactic:
by
  refine ⟨fun _ ↦ ?_, fun hJ ↦ isCardinalPresentable_of_hasCardinalLT_of_le _ hJ h⟩
  obtain ⟨X, f, hf⟩ :=
    IsCardinalPresentable.exists_hom_of_isColimit κ' (isColimitCoconeWithTop J κ')
      (ObjectProperty.homMk (PartOrdEmb.ofHom WithTop.coeOrderHom))
  replace hf : OrderEmbedding.subtype (· ∈ X.1) ∘ f = WithTop.coeOrderHom := by
    ext x
    exact ConcreteCategory.congr_hom hf x
  refine X.2.1.of_injective f (Function.Injective.of_comp
    (f := OrderEmbedding.subtype (· ∈ X.1)) ?_)
  dsimp at hf ⊢
  rw [hf]
  exact WithTop.coe_injective

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
x✝ : IsIso (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
    · simpa [← cancel_mono (toSucc W Z)] using
        D₂.condition f hf (g₁ := g₁ ≫ toStep W Z) (g₂ := g₂ ≫ toStep W Z)
          (by simp [reassoc_of% h])
    · have hZ := IsIso.hom_inv_id (toSucc W Z)
      simp only [Category.assoc] at hZ
      exact ⟨D₁.ιRight f hf g ≫ pushout.inl _ _ ≫ fromStep W Z ≫ inv (toSucc W Z),
        by simp [← D₁.ιLeft_comp_t_assoc, pushout.condition_assoc, hZ]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case pos
κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
B : Set X
hB : HasCardinalLT (↑B) κ₂
⊢ B ⊆ φ₀ Y m B hB

pp: case neg
κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
B : Set X
hB : ¬HasCardinalLT (↑B) κ₂
⊢ B ⊆ B

Tactic:
· intro b hb
    obtain ⟨C, hC, hC'⟩ := hY' B hB ⟨{⟨b, hb⟩},
      hasCardinalLT_of_finite _ _ (IsRegular.aleph0_le Fact.out)⟩
    refine Set.subset_iUnion _ ⟨C, hC⟩ (Or.inl ?_)
    simp only [Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
    exact ⟨hb, @hC' ⟨b, hb⟩ (by simp)⟩

Goal state after:
case neg
κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
B : Set X
hB : ¬HasCardinalLT (↑B) κ₂
⊢ B ⊆ B
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
⊢ f₁ ≫ t ≫ IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t) = f₂ ≫ t ≫ IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t)

Tactic:
by simpa using IsFiltered.coeq_condition (f₁ ≫ t) (f₂ ≫ t)

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ ∃ α x, ∃ (_ : IsDirected α fun x1 x2 ↦ x1 ≤ x2) (_ : Nonempty α), ∃ F, F.Final

Tactic:
have := (isCardinalFiltered_aleph0_iff.{w} J).2 inferInstance
  obtain ⟨α, _, _, F, _⟩ := IsCardinalFiltered.exists_cardinal_directed J .aleph0
  have : IsFiltered α := by rwa [← isCardinalFiltered_aleph0_iff.{w}]
  exact ⟨α, _, IsFiltered.isDirectedOrder _, nonempty, F, inferInstance⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.GlobalSections

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
inst✝ : HasGlobalSectionsFunctor J A
F : Sheaf J A
c : Cone F.obj
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
⊢ f = ΓHomEquiv c.π

Tactic:
by
    replace hf : ((Functor.const Cᵒᵖ).map f) ≫ F.coneΓ.π = c.π := by ext j; exact hf j
    simpa [coneΓ, ← ΓHomEquiv_naturality_left_symm, Equiv.symm_apply_eq] using hf

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
⊢ Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun i ↦
        (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows) ≤
    (cylinder f g).sieve₀

Tactic:
rw [Sieve.generate_le_iff, PreZeroHypercover.sieve₀]

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
⊢ (Presieve.bindOfArrows E.X E.f fun i ↦
      (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows) ≤
    (Sieve.ofArrows (cylinder f g).X (cylinder f g).f).arrows