mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
this : ∑ x ∈ Finset.range (b - a), f (↑a + ↑(x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
⊢ ∑ x ∈ Finset.range (b - a), f ↑(a + (x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x

Tactic:
simp_all

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case coeq
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j j✝ j'✝ : C
hj₁ : filteredClosure f j✝
hj₂ : filteredClosure f j'✝
g g' : j✝ ⟶ j'✝
ih : ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := j✝, property := hj₁ }.obj
ih' : ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := j'✝, property := hj₂ }.obj
⊢ ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := coeq g g', property := ⋯ }.obj

Tactic:
| coeq hj₁ hj₂ g g' ih ih' =>

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : L.Initial
⊢ IsCofiltered (Comma L R)

Tactic:
have := L.initial_iff_isCofiltered_costructuredArrow.mp inferInstance

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : L.Initial
this : ∀ (d : T), IsCofiltered (CostructuredArrow L d)
⊢ IsCofiltered (Comma L R)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : L.Initial
⊢ (fst L R).Initial

Tactic:
have := L.initial_iff_isCofiltered_costructuredArrow.mp inferInstance

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : L.Initial
this : ∀ (d : T), IsCofiltered (CostructuredArrow L d)
⊢ (fst L R).Initial
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ HasCoseparator (ShrinkHoms.{u} C)

Tactic:
obtain ⟨G, -, hG⟩ := Abelian.has_injective_coseparator (separator (ShrinkHoms C))
    (isSeparator_separator _)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
G : ShrinkHoms.{u} C
hG : IsCoseparator G
⊢ HasCoseparator (ShrinkHoms.{u} C)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
this : P.monoModSerre f
⊢ P.isoModSerre f ↔ P.epiModSerre f

Tactic:
isoModSerre_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
this : P.monoModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.epiModSerre f
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Epi f
this : P.epiModSerre f
⊢ P.isoModSerre f ↔ P.monoModSerre f

Tactic:
isoModSerre_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Epi f
this : P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : P.epiModSerre f
⊢ P.isoModSerre f

Tactic:
rwa [isoModSerre_iff_of_mono]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
ha : a ∈ (ModuleCat.Hom.hom x.hom).range
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range

Tactic:
obtain ⟨a', ha'⟩ := ha
    obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective p).1 hp a'
    refine ⟨q a'', ?_⟩
    dsimp at ha' ⊢
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← H,
      ModuleCat.hom_comp, LinearMap.comp_apply, ha'', ha']

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q Q' : ObjectProperty C
h : Q ≤ Q'
⊢ ofObjectProperty P Q ≤ ofObjectProperty P Q'

Tactic:
intro _ _ _ ⟨hX, hY⟩
  exact ⟨hX, h _ hY⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ P.epiModSerre f

Tactic:
have hf : L.map (cokernel.π f) = 0 := by
      rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_zero]
    simpa [hf] using! map_comp_eq_zero_iff_of_epi_mono L P (cokernel.π f) (𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: V : Type (u + 1)
inst✝³ : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst✝² : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝¹ : ConcreteCategory V FV
G : Type u_3
inst✝ : Monoid G
X : Action V G
x : ToType X
⊢ 1 • x = x

Tactic:
change ConcreteCategory.hom (X.ρ 1) x = x
    simp

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
x y : N₁ ⋊[φ₁] G₁
h : (fn.comp (MulEquiv.toMonoidHom (φ₁ x.right))) y.left = ((MulEquiv.toMonoidHom (φ₂ (fg x.right))).comp fn) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.left = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).left

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
x y : N₁ ⋊[φ₁] G₁
h : (fn.comp (MulEquiv.toMonoidHom (φ₁ x.right))) y.left = ((MulEquiv.toMonoidHom (φ₂ (fg x.right))).comp fn) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.right = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).right

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
x y : N₁ ⋊[φ₁] G₁
h : (MulEquiv.trans (φ₁ x.right) fn) y.left = (fn.trans (φ₂ (fg x.right))) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.left = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).left

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
x y : N₁ ⋊[φ₁] G₁
h : (MulEquiv.trans (φ₁ x.right) fn) y.left = (fn.trans (φ₂ (fg x.right))) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩.right = (⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩).right

Tactic:
simp_all

Goal state after:
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
h : F.FullyFaithful
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : (F.mapAction G).obj X✝ ⟶ (F.mapAction G).obj Y✝
x✝ : G
⊢ F.map (X✝.ρ x✝) ≫ f.hom = f.hom ≫ F.map (Y✝.ρ x✝)

Tactic:
exact f.comm _

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : Abelian D := abelian L P
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.isoModSerre f

Tactic:
isoModSerre_iff

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : Abelian D := abelian L P
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f ∧ P.epiModSerre f
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
this : F.IsLeftAdjoint
x✝ : PreservesColimitsOfShape J (F ⋙ H)
K : J ⥤ D
⊢ PreservesColimit K H

Tactic:
let iso : (K ⋙ G) ⋙ F ≅ K :=
    Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ K.rightUnitor

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
this : F.IsLeftAdjoint
x✝ : PreservesColimitsOfShape J (F ⋙ H)
K : J ⥤ D
iso : (K ⋙ G) ⋙ F ≅ K := K.associator G F ≪≫ K.isoWhiskerLeft (asIso adj.counit) ≪≫ K.rightUnitor
⊢ PreservesColimit K H
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
F : Discrete WalkingPair ⥤ Subobject X
this : HasColimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
⊢ HasColimit F

Tactic:
apply hasColimit_of_iso (diagramIsoPair F)

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ T.map (T.η.app X.1) ≫ T.map s.π.f ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f

Tactic:
h₂,

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ T.map (T.η.app X.1) ≫ T.μ.app X.A ≫ s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: 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
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
⊢ G.map (t.adj₁.counit.app (H.obj X) ≫ t.rightToLeft.app X) = G.map (F.map (t.adj₂.counit.app X))

Tactic:
simp [← cancel_epi (t.adj₁.unit.app _)]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (f ≫ g) ⊗≫
          (η.naturality (f ≫ g) ≫ F.mapComp f g ▷ η.app c) ▷ θ.app c ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
          (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
          ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
            F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [θ.naturality_comp]
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((G.map (f.base.toLoc ≫ g.base.toLoc)).toFunctor.obj ((α.app { as := a.base }).toFunctor.obj a.fiber)) ≫
      (α.naturality (f.base.toLoc ≫ g.base.toLoc)).inv.toNatTrans.app a.fiber ≫
        (α.app { as := c.base }).toFunctor.map ((F.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app a.fiber) ≫
          ((F.map g.base.toLoc).toFunctor ⋙ (α.app { as := c.base }).toFunctor).map f.fiber ≫
            (α.app { as := c.base }).toFunctor.map g.fiber =
    (G.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app ((α.app { as := a.base }).toFunctor.obj a.fiber) ≫
      (G.map g.base.toLoc).toFunctor.map ((α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber) ≫
        (α.naturality g.base.toLoc).inv.toNatTrans.app ((F.map f.base.toLoc).toFunctor.obj a.fiber) ≫
          ((F.map g.base.toLoc).toFunctor ⋙ (α.app { as := c.base }).toFunctor).map f.fiber ≫
            (α.app { as := c.base }).toFunctor.map g.fiber

Tactic:
simp [naturality_comp_inv_app, ← Functor.map_comp, ← reassoc_of% Cat.Hom₂.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ F
f : X✝ ⟶ Y✝
⊢ (map (α ≫ β)).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (map α ⋙ map β).map f

Tactic:
dsimp
    simp only [comp_id, id_comp]
    ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ᶜ F
f : X✝ ⟶ Y✝
⊢ (map (α ≫ β)).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (map α ⋙ map β).map f

Tactic:
dsimp
    simp only [comp_id, id_comp]
    ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    (F.mapComp' f₀₁ f₁₃ f hf).hom ≫
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃

Tactic:
F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ _ h₀₂ h₁₃ hf

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
          (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
⊢ ∀ ⦃X Y : (i : I) × C i⦄ (f : X ⟶ Y),
    (Functor.sigma F).map f ≫ SigmaHom.mk ((α Y.fst).app Y.snd) =
      SigmaHom.mk ((α X.fst).app X.snd) ≫ (Functor.sigma G).map f

Tactic:
rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩
    change SigmaHom.mk _ = SigmaHom.mk _
    rw [(α i).naturality]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x ↦ (f a).get ⋯ = x → C a) ((f a).get ⋯)
      (fun b' e ↦
        have e := ⋯;
        hbase a ⋯)
      (fun a'' e ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' ↦
              fixInduction ⋯ fun a' h ih ↦
                Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e ↦
                    have e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e ↦
                    have e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hbase a fa

Tactic:
refine Eq.rec (motive := fun x e ↦
      Sum.casesOn x ?_ ?_ (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = hbase a fa) ?_
    (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm

Goal state after:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x ↦ (f a).get ⋯ = x → C a) (Sum.inl b)
      (fun b' e ↦
        have e := ⋯;
        hbase a ⋯)
      (fun a'' e ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' ↦
              fixInduction ⋯ fun a' h ih ↦
                Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e ↦
                    have e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e ↦
                    have e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hbase a fa
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
hif : IsIso (↾f)
⊢ ∃ f, graphFunctor.map f.hom = r

Tactic:
by
      use asIso (↾f)
      ext ⟨x, y⟩
      exact ⟨by aesop, fun hxy ↦ (h2 (f x) y).1 ⟨x, (hf x).2, hxy⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Cartesian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsCartesianDistributive C
A B Z : C
f g : Z ⟶ (pair A B).obj { as := WalkingPair.left }
he : f ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = g ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl
ι : A ⟶ A ⨿ B := coprod.inl
this✝ : Mono (Z ◁ ι)
this : lift (𝟙 Z) f = lift (𝟙 Z) g
⊢ f = g

Tactic:
simpa only [lift_snd] using this =≫ snd _ _

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom ≫ L'.map (X' ◁ (λ_ Y').hom) =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map ((ρ_ X').hom ▷ Y')
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
rw [← μ_natural_left, tensorHom_id, ← whiskerRight_comp_assoc,
    ← μ_natural_right, ← Iso.comp_inv_eq, assoc, assoc, assoc,
    Iso.hom_inv_id, comp_id, ← whiskerLeft_comp, ← h₂] at h₃

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫ L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom) =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)

Tactic:
by
  rw [← p.map_id]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift f (𝟙 a ≫ φ)

Tactic:
simp_all

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift f (𝟙 a ≫ φ)

Tactic:
by
  simp_all

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift f (φ ≫ 𝟙 b)

Tactic:
simp_all

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift f (φ ≫ 𝟙 b)

Tactic:
by
  simp_all

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift (𝟙 R ≫ f) φ

Tactic:
simp_all

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift (𝟙 R ≫ f) φ

Tactic:
by
  simp_all

Goal state after: