mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.TwoP

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
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:
by ext (_ | _) : 4 <;> rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
J✝ : Type v
inst✝ : Category.{v, v} J✝
F : J✝ ⥤ Cat
⊢ (limit.cone (F ⋙ objects)).pt ≅ (objects.mapCone (HasLimits.limitCone F)).pt

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : ChosenPullbacksAlong f
inst✝¹ : ChosenPullbacksAlong g
inst✝ : ChosenPullbacksAlong (f ≫ g)
⊢ Functor.whiskerRight (pullbackComp f g).hom (map (f ≫ g)) ≫ (mapPullbackAdj (f ≫ g)).counit =
    (mapPullbackAdj (f ≫ g)).counit

Tactic:
rw [pullbackComp, Adjunction.rightAdjointUniq_hom_counit]

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₁ X₂ X₃ : C
⊢ ((tensorBifunctor L W ε).map
            (((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                        (tensorBifunctor L W ε)).hom.app
                  X₁).app
              X₂)).app
        (L'.obj X₃) ≫
      ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                    (tensorBifunctor L W ε)).hom.app
              (((curriedTensor C).obj X₁).obj X₂)).app
          X₃ ≫
        L'.map ((((curriedAssociatorNatIso C).hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                        (tensorBifunctor L W ε)).inv.app
                  X₁).app
              (((curriedTensor C).obj X₂).obj X₃) ≫
            ((tensorBifunctor L W ε).obj (L'.obj X₁)).map
              (((Lifting₂.iso L' L' W W
                          (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                          (tensorBifunctor L W ε)).inv.app
                    X₂).app
                X₃) =
    ((tensorBifunctor L W ε).map (μ L W ε X₁ X₂).hom).app (L'.obj X₃) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ ((tensorBifunctor L W ε).obj (L'.obj X₁)).map (μ L W ε X₂ X₃).inv

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ (∂L X Y Z).hom = coprod.desc (X ◁ coprod.inl) (X ◁ coprod.inr)

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ (∂R X Y Z).hom = coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X)

Tactic:
rfl

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

Goal state before:
pp: case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
val✝ : A
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inl val✝)) = F.map (𝟙 val✝)

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ▷ X = coprod.inl ≫ (∂R X Y Z).hom

Tactic:
coprod_inl_rightDistrib_hom

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ▷ X = coprod.inl ▷ X
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
val✝ : B
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inr val✝)) = G.map (𝟙 val✝)

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : MonoidalClosed C
⊢ IsMonoidalDistrib C

Tactic:
apply SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ (∂L X Y Z).inv = uncurry (coprod.desc (curry coprod.inl) (curry coprod.inr))

Tactic:
← curry_eq_iff

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ curry (∂L X Y Z).inv = coprod.desc (curry coprod.inl) (curry coprod.inr)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ (𝟙 (𝟙_ (Dial C)) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
ext <;> simp; ext; simp; congr 1; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ (f ⊗ₘ 𝟙 (𝟙_ (Dial C))) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f

Tactic:
ext <;> simp; ext; simp; congr 1; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a b : α
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ e a =
    ((pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a)) ≫ g₂) ≫
      Sigma.desc e

Tactic:
rw [(Category.assoc _ _ g₂), pullback.condition]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a b : α
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ e a =
    (pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ Sigma.ι X b) ≫ Sigma.desc e
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ Pentagon Y₁ Y₂ Y₃ Y₄

Tactic:
dsimp [Pentagon]
    refine Eq.trans ?_ (((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫= this =≫
      (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)).trans ?_)
    · rw [← id_tensorHom, ← id_tensorHom, ← tensorHom_id, ← tensorHom_id, assoc, assoc,
        ← tensor_comp, ← associator_naturality, id_comp, ← comp_id e₁.hom,
        tensor_comp, ← associator_naturality_assoc, ← comp_id (𝟙 ((L').obj X₄)),
        ← tensor_comp_assoc, associator_naturality, comp_id, comp_id,
        ← tensor_comp_assoc, assoc, e₄.inv_hom_id, ← tensor_comp, e₁.inv_hom_id,
        ← tensor_comp, e₂.inv_hom_id, e₃.inv_hom_id, id_tensorHom_id, id_tensorHom_id, comp_id]
    · rw [assoc, associator_naturality_assoc, associator_naturality_assoc,
        ← tensor_comp, e₁.inv_hom_id, ← tensor_comp, e₂.inv_hom_id, ← tensor_comp,
        e₃.inv_hom_id, e₄.inv_hom_id, id_tensorHom_id, id_tensorHom_id, id_tensorHom_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝⁴ : HasCoproduct X
inst✝³ : EffectiveEpi (Sigma.desc π)
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W✝ : C
x✝² : (a : α) → X a ⟶ W✝
x✝¹ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), π a ≫ x✝ = x✝² a
⊢ x✝ = EffectiveEpi.desc (Sigma.desc π) (Sigma.desc x✝²) ⋯

Tactic:
apply EffectiveEpi.uniq (Sigma.desc π)

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝⁴ : HasCoproduct X
inst✝³ : EffectiveEpi (Sigma.desc π)
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W✝ : C
x✝² : (a : α) → X a ⟶ W✝
x✝¹ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), π a ≫ x✝ = x✝² a
⊢ Sigma.desc π ≫ x✝ = Sigma.desc x✝²
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
⊢ (eHomEquiv V) (τ.app i ≫ F₂.map f) = (eHomEquiv V) (τ.app j) ≫ eHomWhiskerRight V (F₁.map f) (F₂.obj j)

Tactic:
simp only [← NatTrans.naturality, eHomEquiv_comp, tensorHom_def', id_whiskerLeft,
        assoc, Iso.inv_hom_id_assoc, eHomWhiskerRight]

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 : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.obj a✝ = p.obj a✝

Tactic:
rfl

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 : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.obj b✝ = p.obj b✝

Tactic:
rfl

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 : 𝒮
hRS : R = S
b : 𝒳
hb : p.obj b = S
⊢ p.IsHomLift (eqToHom hRS) (𝟙 b)

Tactic:
by
  subst hRS hb; simp

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

Goal state before:
pp: case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
isHomLift'✝ : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (β.app a)
⊢ { toNatTrans := β.toNatTrans, isHomLift' := isHomLift'✝ } = β

Tactic:
rfl

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.IsCocartesian f φ
b' : 𝒳
ψ ψ' : b ⟶ b'
inst✝¹ : p.IsHomLift (𝟙 S) ψ
inst✝ : p.IsHomLift (𝟙 S) ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ ψ = ψ'

Tactic:
by
  rw [map_uniq p f φ (φ ≫ ψ) ψ rfl, map_uniq p f φ (φ ≫ ψ) ψ' h.symm]

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 : 𝒳 ⥤ 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
b' : 𝒳
φ' : a ⟶ b'
f : p.obj a ⟶ S
inst✝¹ : p.IsStronglyCocartesian f φ
g : S ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst✝ : p.IsHomLift (p.map φ') φ'
this : p.IsHomLift (f ≫ g) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
apply IsStronglyCocartesian.universal_property' f

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: case e_12
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasFunctorEnrichedHom V F₁ F₂
X : J
j : Under X
⊢ { left := j.left, right := j.right, hom := j.hom } = j

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: case e_a.e_a.e_12
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
this :
  enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) ≫
      eHomWhiskerLeft V (F₁.obj j) (F₂.map f) =
    enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) ≫ eHomWhiskerRight V (F₁.map f) (F₂.obj j')
⊢ Under.mk f = { left := (Under.mk (𝟙 j')).left, right := j', hom := f }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: case e_a.e_12
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
k : Under j
this :
  s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)) =
    s.π.app k.right
⊢ { left := (Under.mk (𝟙 k.right)).left, right := k.right, hom := k.hom } = k

Tactic:
rfl

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)
this : Nonempty (Grothendieck F)
⊢ IsFiltered (Grothendieck F)

Tactic:
apply IsFiltered.mk

Goal state after:
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)
⊢ (ConcreteCategory.hom (J.map g)) ((ConcreteCategory.hom (J.map h)) x) =
    (ConcreteCategory.hom (J.map g)) ((ConcreteCategory.hom (J.map h)) x)

Tactic:
rfl

Goal state after:
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)
⊢ (∃ g, y = g • x) ↔ ∃ g, g • x = y

Tactic:
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
X Y : C
f g : X ⟶ Y
x : (F.obj X).obj
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
⊢ (ConcreteCategory.hom (↾Subtype.val)) ⟨x, h⟩ = x

Tactic:
rfl

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

Goal state before:
pp: G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun X ↦ X.obj) X.V
h : (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (Y.ρ g).hom) ↑y
⊢ (ConcreteCategory.hom (Y.ρ g⁻¹)) ((ConcreteCategory.hom (Y.ρ g).hom) ↑y) =
    (ConcreteCategory.hom (Y.ρ g⁻¹ * Y.ρ g).hom) ↑y

Tactic:
rfl

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
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (↾fun p ↦ (↑p).1)) ⟨(a, b), h⟩ = a

Tactic:
rfl

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
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (↾fun p ↦ (↑p).2)) ⟨(a, b), h⟩ = b

Tactic:
rfl

Goal state after: