mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
        η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))

Tactic:
η.naturality_id

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      ((λ_ (η.app a)).hom ≫ (ρ_ (η.app a)).inv ≫ η.app a ◁ G.mapId a) ▷ θ.app a ⊗≫
        η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ ((LeftLift.mk f adj.unit).whisker h).unit ≫ (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ▷ u =
    𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u)

Tactic:
dsimp only [whisker_lift, StructuredArrow.mk_right, whisker_unit,
          StructuredArrow.mk_hom_eq_self]
        bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ (fun f ↦ { hom := { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
      ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f) =
    f

Tactic:
ext (_ | _) : 4

Goal state after:
case none
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      none =
    ↑(ConcreteCategory.hom f.hom) none

case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦
            { hom := { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToTwoPFst.map f ≫
      { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦
              {
                hom :=
                  { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
ext (_ | _) : 4

Goal state after:
case none
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                  invFun := fun f ↦
                    {
                      hom :=
                        { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯,
                          map_snd := ⋯ } },
                  left_inv := ⋯, right_inv := ⋯ }.symm
              (f ≫ g)).hom)
      none =
    ↑(ConcreteCategory.hom
          (pointedToTwoPFst.map f ≫
              { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                    invFun := fun f ↦
                      {
                        hom :=
                          { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯,
                            map_snd := ⋯ } },
                    left_inv := ⋯, right_inv := ⋯ }.symm
                g).hom)
      none

case some
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
val✝ : X'✝.X
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                  invFun := fun f ↦
                    {
                      hom :=
                        { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯,
                          map_snd := ⋯ } },
                  left_inv := ⋯, right_inv := ⋯ }.symm
              (f ≫ g)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom
          (pointedToTwoPFst.map f ≫
              { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                    invFun := fun f ↦
                      {
                        hom :=
                          { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯,
                            map_snd := ⋯ } },
                    left_inv := ⋯, right_inv := ⋯ }.symm
                g).hom)
      (some val✝)
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ (fun f ↦ { hom := { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
      ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f) =
    f

Tactic:
ext (_ | _) : 4

Goal state after:
case none
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      none =
    ↑(ConcreteCategory.hom f.hom) none

case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦
            { hom := { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToTwoPSnd.map f ≫
      { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦
              {
                hom :=
                  { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
ext (_ | _) : 4

Goal state after:
case none
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                  invFun := fun f ↦
                    {
                      hom :=
                        { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                          map_snd := ⋯ } },
                  left_inv := ⋯, right_inv := ⋯ }.symm
              (f ≫ g)).hom)
      none =
    ↑(ConcreteCategory.hom
          (pointedToTwoPSnd.map f ≫
              { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                    invFun := fun f ↦
                      {
                        hom :=
                          { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                            map_snd := ⋯ } },
                    left_inv := ⋯, right_inv := ⋯ }.symm
                g).hom)
      none

case some
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
val✝ : X'✝.X
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                  invFun := fun f ↦
                    {
                      hom :=
                        { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                          map_snd := ⋯ } },
                  left_inv := ⋯, right_inv := ⋯ }.symm
              (f ≫ g)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom
          (pointedToTwoPSnd.map f ≫
              { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                    invFun := fun f ↦
                      {
                        hom :=
                          { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                            map_snd := ⋯ } },
                    left_inv := ⋯, right_inv := ⋯ }.symm
                g).hom)
      (some val✝)
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
𝒵 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
⊢ F.toFunctor ⋙ G.toFunctor ⋙ 𝒵.p = 𝒳.p

Tactic:
G.w,

Goal state after:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
𝒵 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
⊢ F.toFunctor ⋙ 𝒴.p = 𝒳.p
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = τ

Tactic:
apply IsStronglyCocartesian.ext p f φ (g ≫ h) <| by simp only [← assoc, fac]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map φ ≫ e.inv.app X₁ = s.π.app (StructuredArrow.mk φ)
eq : s.π.app (StructuredArrow.mk (φ ≫ L.map f)) = s.π.app (StructuredArrow.mk φ) ≫ F.map f
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map (φ ≫ L.map f) ≫ e.inv.app X₂ =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))

Tactic:
rw [assoc] at hφ

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ : s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y ≫ G.map φ ≫ e.inv.app X₁ = s.π.app (StructuredArrow.mk φ)
eq : s.π.app (StructuredArrow.mk (φ ≫ L.map f)) = s.π.app (StructuredArrow.mk φ) ≫ F.map f
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map (φ ≫ L.map f) ≫ e.inv.app X₂ =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : S.ShortExact
i : I
this : Mono S.f
⊢ (S.map (F i)).ShortExact

Tactic:
have := hS.epi_g

Goal state after:
case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : S.ShortExact
i : I
this✝ : Mono S.f
this : Epi S.g
⊢ (S.map (F i)).ShortExact
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map φ ≫ e.inv.app X₂ = s.π.app (StructuredArrow.mk φ)
this : IsIso (F.map w)
eq : s.π.app (StructuredArrow.mk φ) = s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ≫ F.map w
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      G.map (φ ≫ (Localization.isoOfHom L W w hw).inv) ≫ e.inv.app X₁ =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))

Tactic:
rw [assoc] at hφ

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ : s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y ≫ G.map φ ≫ e.inv.app X₂ = s.π.app (StructuredArrow.mk φ)
this : IsIso (F.map w)
eq : s.π.app (StructuredArrow.mk φ) = s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ≫ F.map w
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      G.map (φ ≫ (Localization.isoOfHom L W w hw).inv) ≫ e.inv.app X₁ =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))
Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj

Goal state before:
pp: M G : Type v
inst✝¹ : Monoid M
inst✝ : Group G
J : SingleObj M ⥤ Type u
g h : M
x : J.obj (SingleObj.star M)
⊢ (g * h) • x = g • h • x

Tactic:
change J.map (g * h) x = (J.map h ≫ J.map g) x

Goal state after:
M G : Type v
inst✝¹ : Monoid M
inst✝ : Group G
J : SingleObj M ⥤ Type u
g h : M
x : J.obj (SingleObj.star M)
⊢ (ConcreteCategory.hom (J.map (g * h))) x = (ConcreteCategory.hom (J.map h ≫ J.map g)) x
Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj

Goal state before:
pp: G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
| J.ColimitTypeRel ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y

Tactic:
rhs; rw [Setoid.comm']

Goal state after:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
| (MulAction.orbitRel G (J.obj (SingleObj.star G))) y x
Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj

Goal state before:
pp: G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
⊢ J.ColimitTypeRel ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y

Tactic:
conv => rhs; rw [Setoid.comm']
  change (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)
  grind

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
G' : Type ?u.28
hg : Group G'
hf : Fintype G'
he : Nonempty (G ≃* G')
⊢ PreservesColimitsOfShape (SingleObj G) F

Tactic:
exact Limits.preservesColimitsOfShape_of_equiv he.some.toSingleObjEquiv.symm F

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this✝¹ : Fintype ↑T
this✝ : MulAction G (FintypeCat.of ↑T).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := FintypeCat.homMk Subtype.val, comm := ⋯ }
this : Mono i
⊢ IsIso i

Tactic:
apply IsConnected.noTrivialComponent T' i

Goal state after:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
T : Set X.V.obj := ⋯
this✝¹ : Fintype ↑T
this✝ : MulAction G (FintypeCat.of ↑T).obj := ⋯
T' : Action FintypeCat G := ⋯
i : T' ⟶ X := ⋯
this : Mono i
⊢ ∀ (a : IsInitial T'), False
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∀ (σ : Aut F), (∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ⇑(autEmbedding F) ⁻¹' U

Tactic:
· refine fun σ h ↦ ha (fun X XinI ↦ ?_)
    suffices h : autEmbedding F σ X = 1 by
      rw [h]
      exact (ho X XinI).right
    have h : σ.hom.app X = 𝟙 (F.obj X) := by
      have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _
      ext x
      obtain ⟨⟨j⟩, a, ha : F.map _ a = x⟩ := Limits.FintypeCat.jointly_surjective
        (Discrete.functor (ff ⟨X, XinI⟩) ⋙ F) _ (Limits.isColimitOfPreserves F (h4 ⟨X, XinI⟩)) x
      rw [FintypeCat.id_apply, ← ha, NatTrans.naturality_apply]
      simp [h ⟨(ff _) j, ⟨Set.range (ff ⟨X, XinI⟩), ⟨⟨_, rfl⟩, ⟨j, rfl⟩⟩⟩⟩]
    exact Iso.ext h

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
⊢ ∃ X, Nonempty ((functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑V)))

Tactic:
have hn : Nonempty (F.obj <| (∏ᶜ fun X : I => X)) := nonempty_fiber_pi_of_nonempty_of_finite F _

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
⊢ ∃ X, Nonempty ((functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑V)))
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
⊢ IsLimit (pullbackCone f g pb)

Tactic:
refine PullbackCone.IsLimit.mk
    (fst := (pullbackCone f g pb).fst) (snd := (pullbackCone f g pb).snd) _
    (fun s ↦ (homPullbackEquiv f g pb hpb s.pt).2 ⟨(s.fst, s.snd), s.condition⟩)
    (fun s ↦ congrArg (·.1.fst)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s ↦ congrArg (·.1.snd)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s m h₁ h₂ ↦ ?_)

Goal state after:
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 : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
⊢ m = (homPullbackEquiv f g pb hpb s.pt).invFun ⟨(s.fst, s.snd), ⋯⟩
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁ ≫ f₁ = h.p

Tactic:
by
  simpa only [← hp₁, Category.assoc, h₁₃.hp₁, h.l.f_p] using h.l.f_p₁.symm =≫ f₁

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

Goal state before:
pp: case inst
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (Pi.map fun i ↦
      if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
apply +allowSynthFailures IsIso.epi_of_iso
    apply +allowSynthFailures Pi.map_isIso
    intro ⟨_, _⟩
    split
    all_goals infer_instance

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

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
r t : Cone F
i : r ≅ t
x✝ : IsWeakLimit r
⊢ (fun h ↦ h.ofIsoWeakLimit i.symm) ((fun h ↦ h.ofIsoWeakLimit i) x✝) = x✝

Tactic:
by simp [ofIsoWeakLimit]

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

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
r t : Cone F
i : r ≅ t
x✝ : IsWeakLimit t
⊢ (fun h ↦ h.ofIsoWeakLimit i) ((fun h ↦ h.ofIsoWeakLimit i.symm) x✝) = x✝

Tactic:
by simp [ofIsoWeakLimit]

Goal state after: