mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ δ L (R.obj c) (R.obj X✝) ≫ L.obj (R.obj c) ◁ (L.map (R.map x✝) ≫ adj.counit.app Y✝) ≫ adj.counit.app c ▷ Y✝ =
    δ L (R.obj c) (R.obj X✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X✝) ≫ c ◁ x✝

Tactic:
Adjunction.counit_naturality,

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ δ L (R.obj c) (R.obj X✝) ≫ L.obj (R.obj c) ◁ (adj.counit.app X✝ ≫ x✝) ≫ adj.counit.app c ▷ Y✝ =
    δ L (R.obj c) (R.obj X✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X✝) ≫ c ◁ x✝
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f = g

Tactic:
← cancel_mono (terminal.from A)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ terminal.from A = g ≫ terminal.from A
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 (uncurry (ihomUncurry x y z ≫ ihomCurry x y z)) = uncurry (uncurry (𝟙 ((ihom y).obj ((ihom x).obj z))))

Tactic:
simp only [uncurry_natural_left, uncurry_uncurry_ihomCurry, Functor.id_obj, uncurry_id_eq_ev]

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 ◁ ihomUncurry x y z ≫ (α_ x y ((ihom (x ⊗ y)).obj z)).inv ≫ (ihom.ev (x ⊗ y)).app z =
    uncurry ((ihom.ev y).app ((ihom x).obj 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✝¹ : MonoidalClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ ihom A ⋙ reflector i ⋙ i ≅ i ⋙ ihom A
B : D
A : C
⊢ i.essImage (A ⟹ i.obj B)

Tactic:
exact ⟨_, ⟨(h A).app B⟩⟩

Goal state after:
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✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
⊢ ExponentialIdeal i

Tactic:
let ir := reflectorAdjunction i
  let L : C ⥤ D := reflector i
  let η : 𝟭 C ⟶ L ⋙ i := ir.unit
  let ε : i ⋙ L ⟶ 𝟭 D := ir.counit
  apply ExponentialIdeal.mk'
  intro B A
  let q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B := by
    apply MonoidalClosed.curry (ir.homEquiv _ _ _)
    apply _ ≫ (ir.homEquiv _ _).symm ((ihom.ev A).app (i.obj B))
    exact prodComparison L A _ ≫ (_ ◁ (ε.app _)) ≫ inv (prodComparison _ _ _)
  have : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B) := by
    dsimp
    rw [← curry_natural_left, curry_eq_iff, uncurry_id_eq_ev, ← ir.homEquiv_naturality_left,
      ir.homEquiv_apply_eq, Category.assoc, Category.assoc,
      prodComparison_natural_whiskerLeft_assoc, ← whiskerLeft_comp_assoc,
      ir.left_triangle_components, whiskerLeft_id, Category.id_comp]
    apply IsIso.hom_inv_id_assoc
  have : IsSplitMono (η.app (A ⟹ i.obj B)) := IsSplitMono.mk' ⟨_, this⟩
  apply mem_essImage_of_unit_isSplitMono

Goal state after:
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).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).hom

Tactic:
prodComparisonIso_hom i ((reflector i).obj A) ((reflector i).obj B)

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
⊢ (reflectorAdjunction i).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)
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
⊢ (bijection i A B ((reflector i).obj A ⊗ (reflector i).obj B))
      ((bijection i A B ((reflector i).obj A ⊗ (reflector i).obj B)).symm
        (𝟙 ((reflector i).obj A ⊗ (reflector i).obj B))) =
    𝟙 ((reflector i).obj A ⊗ (reflector i).obj B)

Tactic:
Equiv.apply_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).obj A ⊗ (reflector i).obj B) = 𝟙 ((reflector i).obj A ⊗ (reflector i).obj B)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (β_ (F.obj x) (H.obj z)).hom ≫
          G.obj y ◁ (unit H F).app (z, x) ≫
            (unit G (H ⊛ F)).app (y, z ⊗ x) ≫ (G ⊛ H ⊛ F).map ((α_ y z x).inv ≫ (β_ (y ⊗ z) x).hom ≫ (α_ x y z).inv) =
    (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (unit F H).app (x, z) ≫
          G.obj y ◁ (braiding F H).hom.app (x ⊗ z) ≫
            (unit G (H ⊛ F)).app (y, x ⊗ z) ≫ (G ⊛ H ⊛ F).map ((α_ y x z).inv ≫ (β_ y x).hom ▷ z)

Tactic:
← whiskerLeft_comp_assoc

Goal state after:
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x)) ≫
          (unit G (H ⊛ F)).app (y, z ⊗ x) ≫ (G ⊛ H ⊛ F).map ((α_ y z x).inv ≫ (β_ (y ⊗ z) x).hom ≫ (α_ x y z).inv) =
    (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (unit F H).app (x, z) ≫
          G.obj y ◁ (braiding F H).hom.app (x ⊗ z) ≫
            (unit G (H ⊛ F)).app (y, x ⊗ z) ≫ (G ⊛ H ⊛ F).map ((α_ y x z).inv ≫ (β_ y x).hom ▷ z)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
Iso.cancel_iso_inv_left

Goal state after:
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝¹ : IsFiltered J
inst✝ : ∀ (j : J), IsFiltered (I j)
j : J
⊢ Nonempty (Total P)

Tactic:
obtain ⟨i⟩ : Nonempty (I j) := IsFiltered.nonempty

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝¹ : IsFiltered J
inst✝ : ∀ (j : J), IsFiltered (I j)
j : J
i : I j
⊢ Nonempty (Total P)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
⊢ sourceLocalClosure K P ≤ Q

Tactic:
intro X Y f hf
  induction hf with
  | of f hf => exact h _ hf
  | of_iso f g e _ hf => rwa [Q.arrow_mk_iso_iff e.symm]
  | comp f hf R hR g hg ih => apply IsLocalAtSource.comp hR _ hg ih
  | of_presieve f R hR h ih => apply IsLocalAtSource.of_forall_comp hR fun U g hg ↦ ih _ _ hg

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

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
X Y : C
g : X ⟶ Y
inst✝¹ : HasPushouts C
inst✝ : P.IsStableUnderCobaseChange
f : Under X
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J f
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
i : J
⊢ P.underObj ((pres.map (Under.pushout g)).diag.obj i)

Tactic:
exact P.pushout_inr _ _ (hpres i)

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

Goal state before:
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
h : Epi (F.map f)
Z : D
u v : F.obj Y ⟶ Z
huv : (fun g ↦ G.map (F.map f) ≫ g) (G.map u) = (fun g ↦ G.map (F.map f) ≫ g) (G.map v)
⊢ G.map u = G.map v

Tactic:
simp only [← G.map_comp, G.map_injective_iff, cancel_epi] at huv

Goal state after:
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
h : Epi (F.map f)
Z : D
u v : F.obj Y ⟶ Z
huv : u = v
⊢ G.map u = G.map v
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst✝¹ : Mono i
inst✝ : IsArtinianObject Y
⊢ IsArtinianObject X

Tactic:
rw [isArtinianObject_iff_antitone_chain_condition]
  intro f
  obtain ⟨n, hn⟩ := antitone_chain_condition_of_isArtinianObject
    ⟨fun n ↦ (Subobject.map i).obj (f n),
      fun _ _ h ↦ (Subobject.map i).monotone (f.2 h)⟩
  exact ⟨n, fun m hm ↦ Subobject.map_obj_injective i (hn m hm)⟩

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

Goal state before:
pp: 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
⊢ localEpi (fun x ↦ x ∈ Set.range G.obj) f ↔ (MorphismProperty.epimorphisms D).inverseImage F f

Tactic:
rw [localEpi_mem_range_iff_epi adj]

Goal state after:
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) ↔ (MorphismProperty.epimorphisms D).inverseImage F f
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasZeroObject C
⊢ isNoetherianObject 0

Tactic:
by
    rw [← isNoetherianObject.is_iff]
    exact isNoetherianObject_of_isZero (isZero_zero C)

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

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.inr ≫ biprod.desc 0 f = biprod.inr ≫ biprod.snd ≫ f

Tactic:
simp only [biprod.inr_desc, BinaryBicone.inr_snd_assoc]

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: α β : PartOrdEmb
f : α ⟶ β
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget PartOrdEmb).map f))
⊢ IsIso f

Tactic:
let e : α ≃o β :=
      { toEquiv := Equiv.ofBijective _ hf
        map_rel_iff' := by simp }

Goal state after:
α β : PartOrdEmb
f : α ⟶ β
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget PartOrdEmb).map f))
e : ↑α ≃o ↑β :=
  let __Equiv := Equiv.ofBijective (⇑(ConcreteCategory.hom ((forget PartOrdEmb).map f))) hf;
  { toEquiv := __Equiv, map_rel_iff' := ⋯ }
⊢ IsIso f
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: 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

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').ι
⊢ ((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'⟩

Tactic:
· intro hj
              simp at hj

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'⟩
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ ObjectProperty.singleton PUnit.{u + 1} ≤ isCardinalPresentable (Type u) κ

Tactic:
simp only [ObjectProperty.singleton_le_iff,
      CategoryTheory.isCardinalPresentable_iff, isCardinalPresentable_iff]

Goal state after:
X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ HasCardinalLT PUnit.{u + 1} κ
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ Presieve.IsSheaf (coherentTopology C) P

Tactic:
simp only [coherentTopology, Presieve.isSheaf_coverage]

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ ∀ {X : C}, ∀ R ∈ (coherentCoverage C).coverings X, Presieve.IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
⊢ IsSheafFor (yoneda.obj W) R

Tactic:
have : IsIso (Sigma.desc (Cofan.inj (Cofan.mk X π))) := hi

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ IsSheafFor (yoneda.obj W) R
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
⊢ IsSheafFor F R

Tactic:
have : IsIso (Sigma.desc (Cofan.inj (Cofan.mk X π))) := hi

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ IsSheafFor F R
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))

Tactic:
specialize h E

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ S.arrows (F.preimage (g₀ ≫ π))

Tactic:
obtain ⟨W, g₁, g₂, h₁, h₂⟩ := H₂
      rw [h₂]
      convert! S.downward_closed h₁ (F.preimage (g₀ ≫ g₂))
      exact F.map_injective (by simp)

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

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
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)
i₁ i₂ : ι
⊢ pullHom' hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯ = hom i₁ i₂

Tactic:
simp [pullHom'_eq_pullHom hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ (𝟙 _)]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
Y : C
k : (cylinder f g).I₁ i j
⊢ pullback.snd
        (pullback.map (cylinderf f g i.snd) (cylinderf f g j.snd) (E.f i.fst) (E.f j.fst)
          (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
          (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      E.toPullback k.down =
    (cylinder f g).toPullback k ≫
      pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯

Tactic:
simp only [cylinder_Y, cylinder_f, toPullback_cylinder, pullback.condition]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S✝ : ?m.2
S : C
inst✝ : HasPullbacks C
X Y : J.HOneHypercover S
f g : X.as ⟶ Y.as
⊢ ∃ W h, h ≫ (toHOneHypercover J S).map f = h ≫ (toHOneHypercover J S).map g

Tactic:
obtain ⟨W, h, ⟨H⟩⟩ := OneHypercover.exists_nonempty_homotopy f g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S✝ : ?m.2
S : C
inst✝ : HasPullbacks C
X Y : J.HOneHypercover S
f g : X.as ⟶ Y.as
W : J.OneHypercover S
h : W.Hom X.as
H : Homotopy (Hom.comp h f) (Hom.comp h g)
⊢ ∃ W h, h ≫ (toHOneHypercover J S).map f = h ≫ (toHOneHypercover J S).map g
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j : (Over X)ᵒᵖ
⊢ uncurry
      (end_.lift (fun j ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯ ≫
        enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) =
    g.app j

Tactic:
simp only [uncurry_curry, end_.lift_π]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j : (Over X)ᵒᵖ
⊢ g.app (op (Over.mk (Under.mk (unop j).hom.op).hom.unop)) = g.app j