mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
⊢ ∀ {a : 𝒳} {R : 𝒮} (f : R ⟶ p.obj a), ∃ b φ, p.IsCartesian f φ

Tactic:
by
    intro a R f
    obtain ⟨b, φ, hφ⟩ := h a R f
    refine ⟨b, φ, inferInstance⟩

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

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.IsStronglyCocartesian f φ
S' S'' : 𝒮
b' b'' : 𝒳
f' : R ⟶ S'
f'' : R ⟶ S''
g : S ⟶ S'
g' : S' ⟶ S''
H : f' = f ≫ g
H' : f'' = f' ≫ g'
φ' : a ⟶ b'
φ'' : a ⟶ b''
inst✝¹ : p.IsStronglyCocartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ φ ≫ map p f φ H φ' ≫ map p f' φ' H' φ'' = φ''

Tactic:
simp only [fac_assoc, fac]

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

Goal state before:
pp: K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝² : SmallCategory J
x✝¹ : FinCategory J
F : J ⥤ K
x✝ : (j : Jᵒᵖ) → Unique ((colimit (F.op ⋙ coyoneda).flip).obj j) :=
  fun j ↦
    (colimitObjIsoColimitCompEvaluation (F.op ⋙ coyoneda).flip j ≪≫
          Coyoneda.colimitCoyonedaIso (F.op.obj j)).toEquiv.unique
⊢ ∀ (j j' : Jᵒᵖ) (f : j ⟶ j'), (ConcreteCategory.hom ((colimit (F.op ⋙ coyoneda).flip).map f)) default = default

Tactic:
subsingleton

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

Goal state before:
pp: case h
𝒮 : 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 φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
τ : a ⟶ b'
hτ : p.IsHomLift (f ≫ g) τ
⊢ (fun χ ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) (φ.inv ≫ τ)

Tactic:
simpa [← assoc] using (IsHomLift.comp p (isoOfIsoLift p f φ).inv (f ≫ g) φ.inv τ)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFiltered C
inst✝ : ∀ (c : C), IsFiltered ↑(F.obj c)
c : C
⊢ Nonempty (Grothendieck F)

Tactic:
obtain ⟨f⟩ : Nonempty (F.obj c) := IsFiltered.nonempty

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFiltered C
inst✝ : ∀ (c : C), IsFiltered ↑(F.obj c)
c : C
f : ↑(F.obj c)
⊢ Nonempty (Grothendieck F)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ c₁.inj val✝ ≫
      (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯).ι.app
        { as := WalkingPair.left } =
    s.inj (Sum.inl val✝)

Tactic:
simp only [Cofan.mk_ι_app, Cofan.IsColimit.fac]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ c₂.inj val✝ ≫
      (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯).ι.app
        { as := WalkingPair.right } =
    s.inj (Sum.inr val✝)

Tactic:
simp only [Cofan.mk_ι_app, Cofan.IsColimit.fac]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
x✝² x✝¹ : (PointedGaloisObject F)ᵒᵖ
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝ :
  Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ Opposite.op { obj := B, pt := b, isGalois := isGalois✝ }
f :
  (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })).obj
hf : (ConcreteCategory.hom (F.map f)) b = a
Y : C
g : A ⟶ Y
h : (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map f)) b) = (ConcreteCategory.hom (F.map g)) a
⊢ (ConcreteCategory.hom
          ((((incl F).op ⋙ coyoneda).map (Opposite.op { val := f, comp := hf }) ≫
                match Opposite.op { obj := B, pt := b, isGalois := isGalois✝ } with
                | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
                  { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }).app
            Y)).toFun
      g =
    (ConcreteCategory.hom
          (((match Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } with
                | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
                  { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }) ≫
                ((const (PointedGaloisObject F)ᵒᵖ).obj (F ⋙ FintypeCat.incl)).map
                  (Opposite.op { val := f, comp := hf })).app
            Y)).toFun
      g

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: case h
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : ↥s) (x : (F.obj (↑i).obj).obj), gs • x = (ConcreteCategory.hom (t.hom.app (↑i).obj)) x
X : PointedGaloisObject F
hXmem : X ∈ s
⊢ (gi X)⁻¹ • gs • X.pt = X.pt

Tactic:
hgs ⟨X, hXmem⟩,

Goal state after:
case h
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : ↥s) (x : (F.obj (↑i).obj).obj), gs • x = (ConcreteCategory.hom (t.hom.app (↑i).obj)) x
X : PointedGaloisObject F
hXmem : X ∈ s
⊢ (gi X)⁻¹ • (ConcreteCategory.hom (t.hom.app (↑⟨X, hXmem⟩).obj)) X.pt = X.pt
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
this : ∃ c, φ.obj c = d'
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'

Tactic:
obtain ⟨c', rfl⟩ := this

Goal state after:
case refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows (φ.obj c') (φ.obj c')
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝¹ : Fan fun x ↦ U
x✝ : α
⊢ { f := fun i a ↦ (x✝¹.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝¹.proj a).φ i } ≫ (U.powerFan α).proj x✝ =
    x✝¹.proj x✝

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Pi

Goal state before:
pp: I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
⊢ (F.map f ≫ fun i ↦ (c i).ι.app j') = (fun i ↦ (c i).ι.app j) ≫ ((Functor.const J).obj fun i ↦ (c i).pt).map f

Tactic:
by
        funext i
        exact (c i).ι.naturality f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁷ : FunLike F α β
f : F
inst✝⁶ : SemilatticeInf α
inst✝⁵ : OrderTop α
inst✝⁴ : SemilatticeInf β
inst✝³ : OrderTop β
inst✝² : InfTopHomClass F α β
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
K : J ⥤ α
⊢ ∀ (j : J),
    (finiteLimitCone (K ⋙ (↑f).toFunctor)).cone.π.app j =
      (eqToIso ⋯).hom ≫ ((↑f).toFunctor.mapCone (finiteLimitCone K).cone).π.app j

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
⊢ (fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p) = p

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁷ : FunLike F α β
f : F
inst✝⁶ : SemilatticeSup α
inst✝⁵ : OrderBot α
inst✝⁴ : SemilatticeSup β
inst✝³ : OrderBot β
inst✝² : SupBotHomClass F α β
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
K : J ⥤ α
⊢ ∀ (j : J),
    (finiteColimitCocone (K ⋙ (↑f).toFunctor)).cocone.ι.app j ≫ (eqToIso ⋯).hom =
      ((↑f).toFunctor.mapCocone (finiteColimitCocone K).cocone).ι.app j

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁴ : FunLike F α β
f : F
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : sInfHomClass F α β
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ α
⊢ ∀ (j : J),
    (limitCone (K ⋙ (↑f).toFunctor)).cone.π.app j =
      (eqToIso ⋯).hom ≫ ((↑f).toFunctor.mapCone (limitCone K).cone).π.app j

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁴ : FunLike F α β
f : F
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : sSupHomClass F α β
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ α
⊢ ∀ (j : J),
    (colimitCocone (K ⋙ (↑f).toFunctor)).cocone.ι.app j ≫ (eqToIso ⋯).hom =
      ((↑f).toFunctor.mapCocone (colimitCocone K).cocone).ι.app j

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : { p // p.1 ≫ f = p.2 ≫ g }
⊢ (fun m ↦ ⟨(m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd), ⋯⟩)
      ((fun s ↦
          { f := fun i ↦ ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩,
            φ := fun i ↦ (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯) })
        s) =
    s

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_9
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
e_4✝ : X = (pair X Y).obj { as := WalkingPair.left }
⊢ 0 = HasZeroObject.zeroIsTerminal.from ((pair X Y).obj { as := WalkingPair.left })

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_10
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
e_5✝ : Y = (pair X Y).obj { as := WalkingPair.right }
⊢ 0 = HasZeroObject.zeroIsTerminal.from ((pair X Y).obj { as := WalkingPair.right })

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_9
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsTerminal.from X

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_10
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsTerminal.from Y

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
e_4✝ : X = (pair X Y).obj { as := WalkingPair.left }
⊢ 0 = HasZeroObject.zeroIsInitial.to ((pair X Y).obj { as := WalkingPair.left })

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_8
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
e_5✝ : Y = (pair X Y).obj { as := WalkingPair.right }
⊢ 0 = HasZeroObject.zeroIsInitial.to ((pair X Y).obj { as := WalkingPair.right })

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_7
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsInitial.to X

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_8
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsInitial.to Y

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
inst✝ : HasWeakLimit F
j j' : J
hj : j = j'
⊢ π F j ≫ eqToHom ⋯ = π F j'

Tactic:
by
  subst hj
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : ¬IsMax j
hj' : hf.incl.app j ≫ g₁ = hf.incl.app j ≫ g₂
⊢ (fun g ↦ hf.F.map (homOfLE ⋯) ≫ g) (hf.incl.app (Order.succ j) ≫ g₁) =
    (fun g ↦ hf.F.map (homOfLE ⋯) ≫ g) (hf.incl.app (Order.succ j) ≫ g₂)

Tactic:
by simpa

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

Goal state before:
pp: case tensor
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
W✝ X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g'✝

Tactic:
hfg'

Goal state after:
case tensor
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
W✝ X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g'✝ = projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g'✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case ρ_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ ((f✝.whiskerRight unit).comp (ρ_hom Y✝)) = projectMapAux f✝¹ ((ρ_hom X✝).comp f✝)

Tactic:
| ρ_naturality =>

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
⊢ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂) =
    ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂)

Tactic:
by
  simp [curriedTensorPreIsoPost]

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
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₁
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 : Type u₁₀
inst✝ : Category.{v₁₀, u₁₀} X
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x y : CatCommSqOver F G X
f : x ⟶ y
⊢ ((transform X).obj (ψ.comp ψ')).map f ≫
      (mkIso (y.fst.associator ψ.left ψ'.left).symm (y.snd.associator ψ.right ψ'.right).symm ⋯).hom =
    (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯).hom ≫
      ((transform X).obj ψ ⋙ (transform X).obj ψ').map f

Tactic:
by ext <;> simp

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
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 : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U : X ⥤ Y
x y : CatCommSqOver F G Y
f : x ⟶ y
⊢ ((precompose F G).obj U ⋙ (transform X).obj ψ).map f ≫
      (mkIso (U.associator y.fst ψ.left) (U.associator y.snd ψ.right) ⋯).hom =
    (mkIso (U.associator x.fst ψ.left) (U.associator x.snd ψ.right) ⋯).hom ≫
      ((transform Y).obj ψ ⋙ (precompose F₁ G₁).obj U).map f

Tactic:
by ext <;> simp

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
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 : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
x y : CatCommSqOver F G Y
f : x ⟶ y
⊢ ((transform Y).obj ψ ⋙ (precompose F₁ G₁).obj U).map f ≫
      (mkIso (U.associator y.fst ψ.left).symm (U.associator y.snd ψ.right).symm ⋯).hom =
    (mkIso (U.associator x.fst ψ.left).symm (U.associator x.snd ψ.right).symm ⋯).hom ≫
      ((precompose F G).obj U ⋙ (transform X).obj ψ).map f

Tactic:
by ext <;> simp

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

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝ : Type u
⊢ (ofTypeFunctor m).map ({ app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝ =
    { app := fun X ↦ ↾joinM, naturality := ⋯ }.app ((ofTypeFunctor m).obj x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝

Tactic:
ext; exact joinM_map_joinM _

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasCoequalizerOfIsSplitPair G
inst✝ : PreservesColimitOfIsSplitPair G
A✝ B✝ : D
f g : A✝ ⟶ B✝
x✝ : G.IsSplitPair f g
this : HasCoequalizer f g
⊢ ReflectsColimit (parallelPair f g) G

Tactic:
apply reflectsColimit_of_reflectsIsomorphisms

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ ReflectsColimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))) G

Tactic:
apply reflectsColimit_of_reflectsIsomorphisms

Goal state after: