mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
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

Tactic:
rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def, assoc,
    ← comp_whiskerRight_assoc, enrichedId_π, ← whisker_exchange_assoc,
    id_whiskerLeft, assoc, assoc, Iso.inv_hom_id_assoc]

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
⊢ end_.π (diagram V F₁ F₂) j ≫
      (λ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv ≫
        eId V (F₁.obj j) ▷ ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    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₂
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

Tactic:
enrichedComp_π,

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₂ ≫
        (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₂) j) ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a'✝ ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
⊢ ∀ (y : a'✝ ⟶ a), (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ ≫ ψ

Tactic:
intro π ⟨hπ, hπ_comp⟩

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a'✝ ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a'✝ ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π = τ ≫ ψ
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: case h.refine_2
𝒮 : 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 b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ ∀ (y : c ⟶ a), (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom

Tactic:
intro π ⟨hπ, hπ_comp⟩

Goal state after:
case h.refine_2
𝒮 : 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 b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π = τ' ≫ Φ.hom
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₄
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

Tactic:
enrichedComp_π,

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₄ ≫
      (end_.π (diagram V F₁ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj 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₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫
      end_.π (diagram V F₁ F₃) j ▷ end_ (diagram V F₃ F₄) ≫
        ((diagram V F₁ F₃).obj (Opposite.op j)).obj j ◁ end_.π (diagram V F₃ F₄) j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j)

Tactic:
← comp_whiskerRight_assoc,

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₃ ≫ end_.π (diagram V F₁ F₃) j) ▷ enrichedHom V F₃ F₄ ≫
      ((diagram V F₁ F₃).obj (Opposite.op j)).obj j ◁ end_.π (diagram V F₃ F₄) j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj 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₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    (enrichedComp V F₁ F₂ F₃ ≫ end_.π (diagram V F₁ F₃) j) ▷ enrichedHom V F₃ F₄ ≫
      ((diagram V F₁ F₃).obj (Opposite.op j)).obj j ◁ end_.π (diagram V F₃ F₄) j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j)

Tactic:
enrichedComp_π,

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 ≫
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j)) ▷
        enrichedHom V F₃ F₄ ≫
      ((diagram V F₁ F₃).obj (Opposite.op j)).obj j ◁ end_.π (diagram V F₃ F₄) j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj 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₄
j : J
| enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄ ≫ end_.π (diagram V F₁ F₄) j

Tactic:
enrichedComp_π,

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₂ ◁ enrichedComp V F₂ F₃ F₄ ≫
    (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₄) j) ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj 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₄
j : J
| enrichedHom V F₁ F₂ ◁ (enrichedComp V F₂ F₃ F₄ ≫ end_.π (diagram V F₂ F₄) j) ≫
    end_.π (diagram V F₁ F₂) j ▷ ((diagram V F₂ F₄).obj (Opposite.op j)).obj j ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)

Tactic:
enrichedComp_π,

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₂ ◁
      ((end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
        eComp V (Opposite.unop (F₂.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j)) ≫
    end_.π (diagram V F₁ F₂) j ▷ ((diagram V F₂ F₄).obj (Opposite.op j)).obj j ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := ⋯
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ ≫ φ' ≫ φ = φ ≫ 𝟙 b

Tactic:
simp only [← assoc, inv_hom, comp_id, id_comp]

Goal state after:
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✝
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

Tactic:
simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, end_.lift_π,
      Under.map_obj_right, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
      eHomWhiskerLeft_id, comp_id, assoc]

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✝
⊢ enrichedHomπ V (Under.forget X✝ ⋙ F₁) (Under.forget X✝ ⋙ F₂) ((Under.map (f ≫ g)).obj j) =
    enrichedHomπ V (Under.forget X✝ ⋙ F₁) (Under.forget X✝ ⋙ F₂) ((Under.map f).obj ((Under.map g).obj 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✝¹ : HasFunctorEnrichedHom V F₂ F₃
inst✝ : HasFunctorEnrichedHom V F₁ F₃
j j' : J
f : j ⟶ j'
k : Under j'
⊢ (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
        precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))) ≫
      (end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂)) k ⊗ₘ
          end_.π (diagram V (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)) k) ≫
        eComp V (F₁.obj k.right) (F₂.obj k.right) (F₃.obj k.right) =
    enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
      precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)) ≫
        end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k

Tactic:
tensorHom_comp_tensorHom_assoc

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✝¹ : HasFunctorEnrichedHom V F₂ F₃
inst✝ : HasFunctorEnrichedHom V F₁ F₃
j j' : J
f : j ⟶ j'
k : Under j'
⊢ (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ≫
          end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂)) k ⊗ₘ
        precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)) ≫
          end_.π (diagram V (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)) k) ≫
      eComp V (F₁.obj k.right) (F₂.obj k.right) (F₃.obj k.right) =
    enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
      precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)) ≫
        end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k
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₂)
⊢ ∀ (Y : D₂), η.app (F'.obj Y) ≫ F'.map (ε.app Y) = 𝟙 (F'.obj Y)

Tactic:
suffices F'.leftUnitor.inv ≫ whiskerLeft F' η ≫ (Functor.associator _ _ _).inv ≫
      whiskerRight ε F' ≫ F'.rightUnitor.hom = 𝟙 _ from
        fun Y₂ ↦ by simpa using congr_app this Y₂

Goal state after:
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₂)
⊢ F'.leftUnitor.inv ≫ F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom = 𝟙 F'
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
⊢ ∃ g, g • x = y

Tactic:
by
    /- We show that the `G`-orbit of `x` is a non-initial subobject of `X` and hence by
    connectedness, the orbit equals `X.V`. -/
    let T : Set X.V := MulAction.orbit G x
    have : Fintype T := Fintype.ofFinite T
    let : MulAction G (FintypeCat.of T) := inferInstanceAs <| MulAction G
      ↑(MulAction.orbit G x)
    let T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of T)
    let i : T' ⟶ X := ⟨FintypeCat.homMk Subtype.val, fun _ ↦ rfl⟩
    have : Mono i := ConcreteCategory.mono_of_injective _ (Subtype.val_injective)
    have : IsIso i := by
      apply IsConnected.noTrivialComponent T' i
      apply (not_initial_iff_fiber_nonempty (Action.forget _ _) T').mpr
      exact Set.Nonempty.coe_sort (MulAction.nonempty_orbit x)
    have hb : Function.Bijective i.hom := by
      apply (ConcreteCategory.isIso_iff_bijective i.hom).mp
      exact map_isIso (forget₂ _ FintypeCat) i
    obtain ⟨⟨y', ⟨g, (hg : g • x = y')⟩⟩, (hy' : y' = y)⟩ := hb.surjective y
    use g
    exact hg.trans hy'

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

Goal state before:
pp: case intro
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
ι : Type u_1
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), Nonempty (F.obj (X i)).obj
val✝ : Fintype ι
f : ι → FintypeCat := fun i ↦ F.obj (X i)
⊢ Nonempty (F.obj (∏ᶜ X)).obj

Tactic:
let i : F.obj (∏ᶜ X) ≅ ∏ᶜ f := PreservesProduct.iso F _

Goal state after:
case intro
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
ι : Type u_1
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), Nonempty (F.obj (X i)).obj
val✝ : Fintype ι
f : ι → FintypeCat := fun i ↦ F.obj (X i)
i : F.obj (∏ᶜ X) ≅ ∏ᶜ f := PreservesProduct.iso F X
⊢ Nonempty (F.obj (∏ᶜ X)).obj
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
obtain ⟨ι, hf, f, t, hc⟩ := has_decomp_connected_components' Y
  let i' (j : ι) : f j ⟶ (functorToAction F).obj X := Sigma.ι f j ≫ t.hom ≫ i
  choose gZ gf gu _ _ h using fun i ↦ exists_lift_of_mono_of_isConnected F X (f i) (i' i)
  let is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i => (functorToAction F).obj (gZ i) :=
    PreservesCoproduct.iso (functorToAction F) gZ
  let u' : ∐ f ≅ ∐ fun i => (functorToAction F).obj (gZ i) := Sigma.mapIso gu
  have heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i := by
    simp only [Iso.trans_inv, Iso.symm_inv, Category.assoc]
    rw [← Iso.inv_comp_eq]
    refine Sigma.hom_ext _ _ (fun j ↦ ?_)
    suffices (functorToAction F).map (gf j) = (gu j).inv ≫ i' j by
      simpa [is2, u']
    simp only [h, Iso.inv_hom_id_assoc]
  refine ⟨∐ gZ, Sigma.desc gf, t.symm ≪≫ u' ≪≫ is2.symm, ?_, by simp [heq]⟩
  · exact mono_of_mono_map (functorToAction F) (heq ▸ mono_comp _ _)

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ ∃ a, (functorToAction F).map a = f

Tactic:
have : IsIso ((functorToAction F).map ψ) := by
      simp only [map_comp, hgvi, Category.assoc, ψ]
      have : IsIso (i ≫ (functorToAction F).map prod.fst) := by
        suffices h : IsIso (𝟙 ((functorToAction F).obj X)) by simpa [i, u]
        infer_instance
      apply IsIso.comp_isIso

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this✝ : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this : IsIso ((functorToAction F).map ψ)
⊢ ∃ a, (functorToAction F).map a = f