mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W : J ⥤ Type w
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasWeightedLimit W F₁
inst✝¹ : HasWeightedLimit W F₂
inst✝ : HasWeightedLimit W F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ W.weightedLimObjMap (f ≫ g) = W.weightedLimObjMap f ≫ W.weightedLimObjMap g

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
W : J ⥤ Type w
F : J ⥤ C
inst✝ : HasWeightedLimit W F
⊢ weightedLimFlipObjMap (𝟙 W) F = 𝟙 (W.weightedLimObjObj F)

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W W' W'' : J ⥤ Type w
g : W ⟶ W'
g' : W' ⟶ W''
F : J ⥤ C
inst✝² : HasWeightedLimit W F
inst✝¹ : HasWeightedLimit W' F
inst✝ : HasWeightedLimit W'' F
⊢ weightedLimFlipObjMap g' F ≫ weightedLimFlipObjMap g F = weightedLimFlipObjMap (g ≫ g') F

Tactic:
by
  cat_disch

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
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A) ≫ f) ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f

Tactic:
G.map_comp

Goal state after:
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
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
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
A : adj.toMonad.Algebra
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ G.map (adj.counit.app (F.obj A.A) ≫ coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))

Tactic:
G.map_comp

Goal state after:
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
A : adj.toMonad.Algebra
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ ∀ (j : J),
    (c.pt ◁ hc.lift { pt := 𝟙_ C, π := { app := fun X ↦ η, naturality := ⋯ } } ≫
          hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } }) ≫
        c.π.app j =
      (ρ_ c.pt).hom ≫ c.π.app j

Tactic:
simp [whiskerLeft_comp_tensorHom_assoc]

Goal state after:
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)
⊢ μ ▷ X P Q ≫ actLeft P Q = (α_ R.X R.X (X P Q)).hom ≫ R.X ◁ actLeft P Q ≫ actLeft P Q

Tactic:
by
  refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
  dsimp [X]
  slice_lhs 1 2 => rw [whisker_exchange]
  slice_lhs 2 3 => rw [whiskerLeft_π_actLeft]
  slice_lhs 1 2 => rw [associator_inv_naturality_left]
  slice_lhs 2 3 => rw [← comp_whiskerRight, left_assoc, comp_whiskerRight, comp_whiskerRight]
  slice_rhs 1 2 => rw [associator_naturality_right]
  slice_rhs 2 3 =>
    rw [← whiskerLeft_comp, whiskerLeft_π_actLeft,
      whiskerLeft_comp, whiskerLeft_comp]
  slice_rhs 4 5 => rw [whiskerLeft_π_actLeft]
  slice_rhs 3 4 => rw [associator_inv_naturality_middle]
  monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ uncurry (ihomCurry x y z ≫ ihomUncurry x y z) = uncurry (𝟙 ((ihom (x ⊗ y)).obj z))

Tactic:
rw [uncurry_natural_left, uncurry_id_eq_ev, uncurry_ihomUncurry]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ (x ⊗ y) ◁ ihomCurry x y z ≫
      (α_ x y ((ihom y).obj ((ihom x).obj z))).hom ≫ x ◁ (ihom.ev y).app ((ihom x).obj z) ≫ (ihom.ev x).app z =
    (ihom.ev (x ⊗ y)).app z
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
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      (((reflectorAdjunction i).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B) ≫
        (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) =
    prodComparison (reflector i) A B

Tactic:
Adjunction.homEquiv_symm_apply,

Goal state after:
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
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ (reflector i).map
        (((reflectorAdjunction i).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B) ≫
          (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) ≫
      (reflectorAdjunction i).counit.app ((reflector i).obj A ⊗ (reflector i).obj B) =
    prodComparison (reflector i) A B
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
⊢ inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
revert n

Goal state after:
C : Type u
X Y : F C
f : X ⟶ Y
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      𝒮 ▷ A ≫
        Δ ▷ A ≫
          (α_ A A A).hom ≫
            A ◁ A ◁ Δ ≫
              (α_ A A (A ⊗ A)).inv ≫
                ((α_ A A (A ⊗ A)).hom ≫
                    A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                  (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
simp only [Category.assoc, Iso.inv_hom_id_assoc]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      𝒮 ▷ A ≫
        Δ ▷ A ≫
          (α_ A A A).hom ≫
            A ◁ A ◁ Δ ≫
              A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv ≫ (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      Δ ▷ A ≫
        (α_ A A A).hom ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ (β_ A A).hom ≫
              A ◁ A ◁ (𝒮 ⊗ₘ 𝒮) ≫
                (α_ A A (A ⊗ A)).inv ≫
                  ((α_ A A (A ⊗ A)).hom ≫
                      A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                    (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
simp only [Category.assoc, Iso.inv_hom_id_assoc]

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      Δ ▷ A ≫
        (α_ A A A).hom ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ (β_ A A).hom ≫
              A ◁ A ◁ (𝒮 ⊗ₘ 𝒮) ≫
                A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv ≫ (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoidalCategory C
M : C
inst✝² : MonObj M
N : C
inst✝¹ : MonObj N
f : M ⟶ N
inst✝ : IsMonHom f
⊢ MonObj.mul ≫ f.mop = (f.mop ⊗ₘ f.mop) ≫ MonObj.mul

Tactic:
by
    apply mopEquiv C |>.fullyFaithfulInverse.map_injective
    simpa [-IsMonHom.mul_hom] using! IsMonHom.mul_hom f

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
⊢ P.localEpi.IsStableUnderCobaseChange

Tactic:
refine .mk' fun X Y S f g _ hg T hT u v huv ↦ ?_

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y S : C
f : X ⟶ S
g : X ⟶ Y
x✝ : HasPushout f g
hg : P.localEpi f
T : C
hT : P T
u v : pushout f g ⟶ T
huv : (fun g_1 ↦ pushout.inr f g ≫ g_1) u = (fun g_1 ↦ pushout.inr f g ≫ g_1) v
⊢ u = v
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
inst✝ : (i : I) → MonoidalCategory (C i)
A B X Y : (i : I) → C i
f : A ⟶ B
g : X ⟶ Y
i : I
⊢ (f ⊗ₘ g) i = (f ▷ X ≫ B ◁ g) i

Tactic:
simp [tensorHom_def, whiskerLeft]

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) = 0 ↔ IsEmpty (X ≅ Y)

Tactic:
rw [← not_nonempty_iff, ← not_congr (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y)]
  have := finrank_hom_simple_simple_le_one 𝕜 X Y
  lia

Goal state after:
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 i j ↦ L.map ((embedding C).map (f i j))) ≫
        (biproduct.map fun b ↦ (α.app (Y✝.X b)).hom) ≫
          (biproduct.map fun b ↦ ((embeddingLiftIso F).symm.app (Y✝.X b)).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 [biproduct.matrix_map_assoc, Category.assoc]

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) ≫
          (additiveObjIsoBiproduct (lift F) X✝).inv ≫ (lift F).map f
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
⊢ (succStruct W Z).prop ≤ W.isLocal.isLocal

Tactic:
rintro Z₀ _ _ ⟨_⟩
    exact isLocal_isLocal_toSucc W Z₀

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

Goal state before:
pp: case succ.refine_1
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
x✝¹ : ↑(Y (transfiniteIterate (φ Y m) j A) hj')
C : SetCardinalLT κ₁ ↑(transfiniteIterate (φ Y m) j A)
hC : C ∈ Y (transfiniteIterate (φ Y m) j A) hj'
x✝ : ↑(Subtype.val '' ↑↑⟨C, hC⟩)
c : X
hc : ∃ (x : c ∈ transfiniteIterate (φ Y m) j A), ⟨c, ⋯⟩ ∈ ↑C
⊢ ↑↑C

Tactic:
exact ⟨⟨c, hc.choose⟩, hc.choose_spec⟩

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

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝³ : Fact κ₁.IsRegular
inst✝² : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
h : ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
X : Type w
inst✝¹ : PartialOrder X
inst✝ : IsCardinalFiltered X κ₁
A : Set X
hA : HasCardinalLT (↑A) κ₂
⊢ ∃ B, A ⊆ B ∧ IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂

Tactic:
choose Y hY hY' using fun (B : Set X) hB ↦ h B hB
  have hY'' (B : Set X) (hB : HasCardinalLT B κ₂)
      (C : SetCardinalLT κ₁ B) (hC : C ∈ Y B hB) :
    ∃ (m : X), ∀ (b : B), b ∈ C.val → b ≤ m :=
      ⟨IsCardinalFiltered.max (fun (c : C.val) ↦ c.val.val) C.prop,
        fun b hb ↦ leOfHom (IsCardinalFiltered.toMax
          (fun (c : C.val) ↦ c.val.val) C.prop ⟨_, hb⟩)⟩
  choose m hm using hY''
  -- The expected subset `B` is obtained as the union over
  -- all `j : κ₁.ord.ToType` of the transfinite iterations
  -- of the map `φ`
  exact ⟨⋃ j, transfiniteIterate (φ Y m) j A, subset_iUnion Y m A,
    isCardinalFiltered_iUnion h₀ Y hY hY' m hm A hA,
    hasCardinalLT_iUnion _ (by simpa [hasCardinalLT_iff_cardinal_mk_lt])
      (hasCardinalLT_transfiniteIterate_φ h₀ Y hY m A hA)⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : IsCardinalLocallyPresentable C κ
inst✝ : IsSmall.{w, v, u} W
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
⊢ IsCardinalLocallyPresentable W.isLocal.FullSubcategory κ

Tactic:
have := isRightAdjoint_ι_isLocal W κ hW

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : IsCardinalLocallyPresentable C κ
inst✝ : IsSmall.{w, v, u} W
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
this : W.isLocal.ι.IsRightAdjoint
⊢ IsCardinalLocallyPresentable W.isLocal.FullSubcategory κ
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
⊢ ∃ T ∈ {S | ∃ α, ∃ (_ : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π},
    T.FactorsThruAlong (Presieve.ofArrows X₁ π₁) f

Tactic:
obtain ⟨β, _, X₂, π₂, h, i, ι, hh⟩ := Precoherent.pullback f α X₁ π₁ hS

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ ∃ T ∈ {S | ∃ α, ∃ (_ : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π},
    T.FactorsThruAlong (Presieve.ofArrows X₁ π₁) f
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → ↑x ⟶ m₁
X Y j : J
hj : D.P j
⊢ (D₃ D m₁).P ↑⟨j, hj⟩

Tactic:
· exact Or.inl hj

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α, ∃ (_ : Finite α), ∃ Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
x✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
        fun c => (H c.fst).2 c.snd⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
h₂ : Sieve.generate (Presieve.ofArrows ?m.50 ?m.51) ∈ (regularTopology C) X
⊢ (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π).EffectiveEpimorphic

Tactic:
by
    change Nonempty _
    rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
    exact fun W => regularTopology.isSheaf_yoneda_obj W _ h₂

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₂ : (sieve f f' i).arrows f₂
h₁ : (sieve f f' i).arrows (Over.homMk Y₁.hom ⋯)
fac : g₁ ≫ Over.homMk Y₁.hom ⋯ = g₂ ≫ f₂
⊢ f₂ = Over.homMk Y₂.hom ⋯

Tactic:
ext; simpa using Over.w f₂

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : J.IsLocalSite
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P P' : Cᵒᵖ ⥤ A
F : P ⟶ P'
⊢ (point J).presheafFiber.map F ≫ (pointPresheafFiberIso J P').hom = (pointPresheafFiberIso J P).hom ≫ F.app (op (⊤_ C))

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
N : Type u'
inst✝¹ : Category.{v', u'} N
p : N ⥤ C
inst✝ : InitiallySmall N
U V : N
g : V ⟶ U
X : C
f : p.obj U ⟶ X
⊢ fiberMk (p.map g ≫ f) = fiberMk f

Tactic:
by
  simp [fiberMk, ← dsimp% congr_hom (colimit.w (p.op ⋙ shrinkYoneda.{w}.obj X) g.op)
        (shrinkYonedaObjObjEquiv.symm f),
    fiber, shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ i g', g' ≫ f i = f' i'
i : ι
⊢ (Sieve.ofArrows X' f').arrows (f i)

Tactic:
rw [← h]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ i g', g' ≫ f i = f' i'
i : ι
⊢ (Sieve.ofArrows X f).arrows (f i)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M N : ↑(F.obj { as := op S })
⊢ Function.Bijective (F.toDescentData f).map ↔
    Function.Bijective
      (⇑(DescentData.subtypeCompatibleHomEquiv F f) ∘
        Presieve.Arrows.toCompatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯)

Tactic:
← Function.Bijective.of_comp_iff _ (presheafHomObjHomEquiv F).bijective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M N : ↑(F.obj { as := op S })
⊢ Function.Bijective (F.toDescentData f).map ↔
    Function.Bijective
      ((⇑(DescentData.subtypeCompatibleHomEquiv F f) ∘
          Presieve.Arrows.toCompatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯) ∘
        ⇑F.presheafHomObjHomEquiv)
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ (underlyingIso (pullback.snd 𝒞.truth (𝒞.χ i))).hom ≫ pullback.snd 𝒞.truth (𝒞.χ i) =
    ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow

Tactic:
underlyingIso_hom_comp_eq_mk

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ (Subobject.mk (pullback.snd 𝒞.truth (𝒞.χ i))).arrow = ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
A' : Type u_2
inst✝¹ : Category.{v_2, u_2} A'
B : Type u
inst✝ : Category.{v, u} B
F : A ⊕ A' ⥤ B
⊢ natTransOfWhiskerLeftInlInr (𝟙 (inl_ A A' ⋙ F)) (𝟙 (inr_ A A' ⋙ F)) = 𝟙 F

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
A' : Type u_2
inst✝¹ : Category.{v_2, u_2} A'
B : Type u
inst✝ : Category.{v, u} B
F G H : A ⊕ A' ⥤ B
η₁ : inl_ A A' ⋙ F ⟶ inl_ A A' ⋙ G
η₂ : inr_ A A' ⋙ F ⟶ inr_ A A' ⋙ G
ν₁ : inl_ A A' ⋙ G ⟶ inl_ A A' ⋙ H
ν₂ : inr_ A A' ⋙ G ⟶ inr_ A A' ⋙ H
⊢ natTransOfWhiskerLeftInlInr (η₁ ≫ ν₁) (η₂ ≫ ν₂) =
    natTransOfWhiskerLeftInlInr η₁ η₂ ≫ natTransOfWhiskerLeftInlInr ν₁ ν₂

Tactic:
by
  cat_disch

Goal state after: