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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
x✝ : Action V G
⊢ (λ_ ((F.mapAction G).obj x✝)).inv =
    (F.mapAction G).map (λ_ x✝).inv ≫
      { hom := δ F (𝟙_ (Action V G)).V x✝.V, comm := ⋯ } ≫ { hom := η F, comm := ⋯ } ▷ (F.mapAction G).obj x✝

Tactic:
by ext; simp

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
x✝ : Action V G
⊢ (ρ_ ((F.mapAction G).obj x✝)).inv =
    (F.mapAction G).map (ρ_ x✝).inv ≫
      { hom := δ F x✝.V (𝟙_ (Action V G)).V, comm := ⋯ } ≫ (F.mapAction G).obj x✝ ◁ { hom := η F, comm := ⋯ }

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

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
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
⊢ (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint

Tactic:
by
    refine ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint
    exact Functor.isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } })) ≫
      MonoidalCategoryStruct.whiskerRight (F.mapId { as := { as := () } }) (F.map (𝟙 { as := { as := () } })) =
    (MonoidalCategoryStruct.leftUnitor (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
simp only [tensorUnit_def, tensorObj_def, whiskerRight_def, Category.assoc, leftUnitor_def]
    rw [F.mapComp_id_left, unitors_equal, F.map₂_inv_hom_assoc]

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

Goal state before:
pp: case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
x✝ : ∃ a_1 ∈ f a, ⟨some b, hb⟩ = ⟨some a_1, ⋯⟩
w : Y✝
hw : w ∈ f a
h : ⟨some b, hb⟩ = ⟨some w, ⋯⟩
⊢ some b = (partialFunToPointed.map f).toFun (some a)

Tactic:
rw [Subtype.ext_iff] at h

Goal state after:
case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
x✝ : ∃ a_1 ∈ f a, ⟨some b, hb⟩ = ⟨some a_1, ⋯⟩
w : Y✝
hw : w ∈ f a
h : ↑⟨some b, hb⟩ = ↑⟨some w, ⋯⟩
⊢ some b = (partialFunToPointed.map f).toFun (some a)
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf ↦
      match e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p ↦
            WellFounded.fixF
              (fun a IH ↦
                Part.assert (f a).Dom fun hf ↦
                  match e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯)
              y ⋯)
          a' ⋯
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
simp only [Part.mem_assert_iff] at h₂

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  ∃ h,
    b ∈
      match e : (f a).get h with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        WellFounded.fixF
          (fun a IH ↦
            Part.assert (f a).Dom fun hf ↦
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          a' ⋯
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (↑f).preimage s = f ⁻¹' s

Tactic:
by 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
c : Cofan X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : C
e : c.pt ⟶ W✝
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt), g₁ ≫ hc.desc (Cofan.mk B π) = g₂ ≫ hc.desc (Cofan.mk B π) → g₁ ≫ e = g₂ ≫ e
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ c.ι.app { as := a₁ } ≫ e = g₂ ≫ c.ι.app { as := a₂ } ≫ e

Tactic:
by
    simp only [← Category.assoc]
    exact h (g₁ ≫ c.ι.app ⟨a₁⟩) (g₂ ≫ c.ι.app ⟨a₂⟩) (by simpa)

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

Goal state before:
pp: 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 G : A ⥤ C
H I : B ⥤ C
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ B
f : X ⟶ Y
⊢ ((F.sum' H).map f ≫
      match Y with
      | inl X => α.app X
      | inr X => β.app X) =
    (match X with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map f

Tactic:
cases f <;> simp

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

Goal state before:
pp: case h
𝒮 : 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.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ CommSq (p.map (φ ≫ ψ)) (eqToHom ?ha) (eqToHom ?hb) (f ≫ g)

Tactic:
rw [p.map_comp]

Goal state after:
case h
𝒮 : 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.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ CommSq (p.map φ ≫ p.map ψ) (eqToHom ?ha) (eqToHom ?hb) (f ≫ g)
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
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ (homEquiv V) (f ≫ g) = (λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫ enrichedComp V F₁ F₂ F₃

Tactic:
ext j

Goal state after:
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₂ F₃ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ (homEquiv V) (f ≫ g) ≫ end_.π (diagram V F₁ F₃) j =
    ((λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫ enrichedComp V F₁ F₂ F₃) ≫ end_.π (diagram V F₁ F₃) j
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
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂ =
    𝟙 (enrichedHom V F₁ F₂)

Tactic:
ext j

Goal state after:
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✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ ((λ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂) ≫
      end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
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
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫ enrichedComp V F₁ F₂ F₂ =
    𝟙 (enrichedHom V F₁ F₂)

Tactic:
ext j

Goal state after:
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✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ ((ρ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫ enrichedComp V F₁ F₂ F₂) ≫
      end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
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
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
⊢ (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
      enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄ =
    enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄

Tactic:
ext j

Goal state after:
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₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
⊢ ((α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
        enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄) ≫
      end_.π (diagram V F₁ F₄) j =
    (enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄) ≫ end_.π (diagram V F₁ F₄) j
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✝ : HasFunctorEnrichedHom V F₁ F₂
X : J
⊢ precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
      (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)) =
    𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂))

Tactic:
ext j

Goal state after:
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
⊢ precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
        (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)) ≫
      end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j =
    𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) ≫
      end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j
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✝ : HasFunctorEnrichedHom V F₁ F₂
X✝ Y✝ Z✝ : J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ precompEnrichedHom' V (Under.map (f ≫ g)) (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X✝ ⋙ F₁))
      (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X✝ ⋙ F₂)) =
    precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget X✝ ⋙ F₁))
        (Iso.refl (Under.map f ⋙ Under.forget X✝ ⋙ F₂)) ≫
      precompEnrichedHom' V (Under.map g) (Iso.refl (Under.map g ⋙ Under.forget Y✝ ⋙ F₁))
        (Iso.refl (Under.map g ⋙ Under.forget Y✝ ⋙ F₂))

Tactic:
ext j

Goal state after:
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✝ Y✝ Z✝ : J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : Under Z✝
⊢ precompEnrichedHom' V (Under.map (f ≫ g)) (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X✝ ⋙ F₁))
        (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X✝ ⋙ F₂)) ≫
      end_.π (diagram V (Under.forget Z✝ ⋙ F₁) (Under.forget Z✝ ⋙ F₂)) j =
    (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget X✝ ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget X✝ ⋙ F₂)) ≫
        precompEnrichedHom' V (Under.map g) (Iso.refl (Under.map g ⋙ Under.forget Y✝ ⋙ F₁))
          (Iso.refl (Under.map g ⋙ Under.forget Y✝ ⋙ F₂))) ≫
      end_.π (diagram V (Under.forget Z✝ ⋙ F₁) (Under.forget Z✝ ⋙ F₂)) j
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✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
m : s.pt ⟶ (coneFunctorEnrichedHom V F₁ F₂).pt
hm : ∀ (j : J), m ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j
⊢ m = lift s

Tactic:
ext j

Goal state after:
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₂)
m : s.pt ⟶ (coneFunctorEnrichedHom V F₁ F₂).pt
hm : ∀ (j : J), m ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j
j : J
⊢ m ≫ end_.π (diagram V F₁ F₂) j = lift s ≫ end_.π (diagram V F₁ F₂) j
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
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasFunctorEnrichedHom V F₂ F₃
inst✝³ : HasFunctorEnrichedHom V F₃ F₄
inst✝² : HasFunctorEnrichedHom V F₁ F₃
inst✝¹ : HasFunctorEnrichedHom V F₂ F₄
inst✝ : HasFunctorEnrichedHom V F₁ F₄
⊢ (α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)).inv ≫
      functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄ ≫ functorEnrichedComp V F₁ F₃ F₄ =
    functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄ ≫ functorEnrichedComp V F₁ F₂ F₄

Tactic:
ext j

Goal state after:
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₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasFunctorEnrichedHom V F₂ F₃
inst✝³ : HasFunctorEnrichedHom V F₃ F₄
inst✝² : HasFunctorEnrichedHom V F₁ F₃
inst✝¹ : HasFunctorEnrichedHom V F₂ F₄
inst✝ : HasFunctorEnrichedHom V F₁ F₄
j : J
⊢ ((α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)).inv ≫
          functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄ ≫ functorEnrichedComp V F₁ F₃ F₄).app
      j =
    (functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄ ≫ functorEnrichedComp V F₁ F₂ F₄).app j
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
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ (functorHomEquiv V) (f ≫ g) =
    (λ_ (𝟙_ (J ⥤ V))).inv ≫ ((functorHomEquiv V) f ⊗ₘ (functorHomEquiv V) g) ≫ functorEnrichedComp V F₁ F₂ F₃

Tactic:
ext j

Goal state after:
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₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ ((functorHomEquiv V) (f ≫ g)).app j =
    ((λ_ (𝟙_ (J ⥤ V))).inv ≫ ((functorHomEquiv V) f ⊗ₘ (functorHomEquiv V) g) ≫ functorEnrichedComp V F₁ F₂ F₃).app j
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
this : G'.leftUnitor.inv ≫ whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom = 𝟙 G'
Y₁ : D₁
⊢ G'.map (η.app Y₁) ≫ ε.app (G'.obj Y₁) = 𝟙 (G'.obj Y₁)

Tactic:
by simpa using congr_app this Y₁

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X Y : C
i : X ≅ Y
⊢ Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj

Tactic:
have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i)

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X Y : C
i : X ≅ Y
e : (F.obj X).obj ≃ (F.obj Y).obj
⊢ Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) (mkSelfProdFib F X) = t

Tactic:
by
  rw [← piComparison_comp_π]
  simp [← PreservesProduct.iso_hom, mkSelfProdFib]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
h : Nonempty (F.obj X).obj
⊢ ∃ A x, IsGalois A

Tactic:
obtain ⟨x⟩ := h

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
⊢ ∃ A x, IsGalois A
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
⊢ ∀ (i j : (PointedGaloisObject F)ᵒᵖ)
    (xi : (fun X ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj i))
    (xj : (fun X ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj j)),
    (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app i)) xi =
        (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) xi =
          (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) xj

Tactic:
· intro ⟨A, a, _⟩ ⟨B, b, _⟩ (u : (A : C) ⟶ X) (v : (B : C) ⟶ X) (h : F.map u a = F.map v b)
    obtain ⟨⟨Z, z, _⟩, ⟨f, hf⟩, ⟨g, hg⟩, _⟩ :=
      IsFilteredOrEmpty.cocone_objs (C := (PointedGaloisObject F)ᵒᵖ)
        ⟨{ obj := A, pt := a}⟩ ⟨{obj := B, pt := b}⟩
    refine ⟨⟨{ obj := Z, pt := z }⟩, ⟨f, hf⟩, ⟨g, hg⟩, ?_⟩
    apply evaluation_injective_of_isConnected F Z X z
    change F.map (f ≫ u) z = F.map (g ≫ v) z
    rw [map_comp, FintypeCat.comp_apply, hf, map_comp, FintypeCat.comp_apply, hg, h]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
⊢ t ∈ S

Tactic:
apply hU

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ⋯
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
⊢ t ∈ U
Module: Mathlib.CategoryTheory.IsoCat

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
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
x : C
⊢ (𝟭 C).obj x = (F ⋙ F.strictInv).obj x

Tactic:
by simp [strictInv]

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

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
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
x : D
⊢ (F.strictInv ⋙ F).obj x = (𝟭 D).obj x

Tactic:
by simp [strictInv]

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

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
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
x✝² x✝¹ : D
x✝ : x✝² ⟶ x✝¹
⊢ (F.strictInv ⋙ F).map x✝ = eqToHom ⋯ ≫ (𝟭 D).map x✝ ≫ eqToHom ⋯

Tactic:
by simp [strictInv]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f g : X ⟶ Y
h₁ : f.f = g.f
h₂ : ∀ (i : X.I), f.φ i ≫ eqToHom ⋯ = g.φ i
⊢ f = g

Tactic:
obtain ⟨f, F⟩ := f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
g : X ⟶ Y
f : X.I → Y.I
F : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₁ : { f := f, φ := F }.f = g.f
h₂ : ∀ (i : X.I), { f := f, φ := F }.φ i ≫ eqToHom ⋯ = g.φ i
⊢ { f := f, φ := F } = g