mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simp only [← Category.assoc]
    exact h (g₁ ≫ c.ι.app ⟨a₁⟩) (g₂ ≫ c.ι.app ⟨a₂⟩) (by simpa)

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
a b : α
hg :
  pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a) ≫ π a =
    pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b

Tactic:
simp only [← Category.assoc] at hg

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
a b : α
hg :
  (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    ((pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a)) ≫ g₂) ≫
      Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
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₂
g : 𝟙_ V ⟶ enrichedHom V F₁ F₂
i j : J
f : i ⟶ j
⊢ ((eHomEquiv V) (F₁.map f) ⊗ₘ g ≫ end_.π (diagram V F₁ F₂) j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j) =
    (g ≫ end_.π (diagram V F₁ F₂) i ⊗ₘ (eHomEquiv V) (F₂.map f)) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)

Tactic:
conv_rhs =>
          rw [tensorHom_def_assoc, MonoidalCategory.whiskerRight_id_assoc, assoc,
            enrichedHom_condition' V F₁ F₂ f]

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✝ : HasEnrichedHom V F₁ F₂
g : 𝟙_ V ⟶ enrichedHom V F₁ F₂
i j : J
f : i ⟶ j
⊢ ((eHomEquiv V) (F₁.map f) ⊗ₘ g ≫ end_.π (diagram V F₁ F₂) j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j) =
    (ρ_ (𝟙_ V)).hom ≫
      g ≫
        enrichedHomπ V F₁ F₂ j ≫
          (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
            ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit

Goal state before:
pp: K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
suffices Nonempty (limit (colimit (F.op ⋙ coyoneda).flip)) by
    obtain ⟨X, y, -⟩ := Types.jointly_surjective' (this.map (h (F.op ⋙ coyoneda)).some).some
    exact ⟨X, ⟨(limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) _).hom y⟩⟩

Goal state after:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
⊢ Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))
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
x : J.obj (SingleObj.star M)
⊢ 1 • x = x

Tactic:
by
    change J.map (𝟙 _) x = x
    simp

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

Goal state before:
pp: case neg
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
by_cases nhi : IsInitial X → False

Goal state after:
case pos
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

case neg
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ¬∀ (a : IsInitial X), False
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: 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)
⊢ ∃ I x,
    (∀ X ∈ I, IsConnected X) ∧ ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ⇑(autEmbedding F) ⁻¹' U

Tactic:
refine ⟨⋃ X, Set.range (ff X), Fintype.ofFinite _, ?_, ?_⟩

Goal state after:
case refine_1
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)
⊢ ∀ X ∈ ⋃ X, Set.range (ff X), IsConnected X

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
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: 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
h✝ : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
h : (autEmbedding F) σ X = 1
⊢ (autEmbedding F) σ X ∈ u X

Tactic:
by
      rw [h]
      exact (ho X XinI).right

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ f ≫ g ∈ S.arrows c e → g ∈ S.arrows d e

Tactic:
rintro h

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
⊢ g ∈ S.arrows d e
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d

Tactic:
rintro h

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
⊢ f ∈ S.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsWide → S.objs = univ

Tactic:
rintro h

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
⊢ S.objs = univ
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.objs = univ → S.IsWide

Tactic:
rintro h

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.objs = univ
⊢ S.IsWide
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S

Tactic:
rintro h

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : ∀ (c d : C), X c d ⊆ S.arrows c d
⊢ generatedNormal X ≤ S
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
c d : D
f : c ⟶ d
⊢ f ∈ (im φ hφ).arrows c d ↔ ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
convert! Map.arrows_iff φ hφ ⊤ f; simp only [Top.top, mem_univ, exists_true_left]

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

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯ ≫ f m

Tactic:
cases m with
  | zero =>
      have : n = 0 := by lia
      subst this
      simp [functorMap]
  | succ m =>
      rw [← functorMap_commSq_succ f (m + 1)]
      simp only [homOfLE_leOfHom, dite_eq_ite,
        Functor.ofOpSequence_map_homOfLE_succ]
      have : homOfLE (by lia : n ≤ m + 1 + 1) =
          homOfLE (by lia : n ≤ m + 1) ≫ homOfLE (by lia : m + 1 ≤ m + 1 + 1) := by simp
      rw [this, op_comp, Functor.map_comp]
      simp only [homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
        Category.assoc]
      congr 1
      exact functorMap_commSq_aux f (by lia) (by lia)

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

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n : ℕ
⊢ ∀ (b : ℕ),
    (((Functor.const ℕᵒᵖ).obj (∏ᶜ M)).map (homOfLE ⋯).op ≫
          Pi.map fun m ↦ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) b =
      ((Pi.map fun m ↦ if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
          (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) ≫
        Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) b

Tactic:
intro m

Goal state after:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
⊢ (((Functor.const ℕᵒᵖ).obj (∏ᶜ M)).map (homOfLE ⋯).op ≫
        Pi.map fun m ↦ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m =
    ((Pi.map fun m ↦ if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n : ℕ
⊢ ∀ (b : ℕ),
    ((Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
          (cone f).π.app (Opposite.op n)) ≫
        Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) b =
      s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) b

Tactic:
intro m

Goal state after:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
⊢ ((Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
        (cone f).π.app (Opposite.op n)) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
⊢ coendRel F ⟨j, x⟩ ⟨j', x'⟩ ↔ ∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x'

Tactic:
constructor
  · rintro ⟨f, x⟩
    exact ⟨f, x, by simp⟩
  · rintro ⟨f, y, rfl, rfl⟩
    exact coendRel.mk f y

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : A
⊢ φ.base.map ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) ≫
      (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ.left.obj x) ≫ F''.map (φ.left.map (α.left.app x)) =
    φ.base.map (α.base.app (F.obj x) ≫ (CatCommSq.iso F ψ'.left ψ'.base F').hom.app x) ≫
      (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ'.left.obj x)

Tactic:
← left_coherence_app,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : A
⊢ φ.base.map ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) ≫
      (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ.left.obj x) ≫ F''.map (φ.left.map (α.left.app x)) =
    φ.base.map ((CatCommSq.iso F ψ.left ψ.base F').hom.app x ≫ F'.map (α.left.app x)) ≫
      (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ'.left.obj x)
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f✝ : X ⟶ Y
x✝² : P.isLocal.transfiniteCompositionsOfShape J f✝
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f✝
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ hf.F.map f ≫ ↑σ (op x✝) = ↑σ (op x✝¹) ≫ 𝟙 Z

Tactic:
simpa only [Category.comp_id] using! σ.2 f.op

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

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro X Y ⟨f⟩

Goal state after:
case mk
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : Quotient (X.setoidHom Y)
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quotient.map₂ Hom.comp ⋯ ⟦Hom.id X⟧ (Quot.mk (⇑(X.setoidHom Y)) f) = Quot.mk (⇑(X.setoidHom Y)) f
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro X Y ⟨f⟩

Goal state after:
case mk
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : Quotient (X.setoidHom Y)
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quotient.map₂ Hom.comp ⋯ (Quot.mk (⇑(X.setoidHom Y)) f) ⟦Hom.id Y⟧ = Quot.mk (⇑(X.setoidHom Y)) f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x y : CatCommSqOver F G X
f : x ⟶ y
⊢ whiskerRight (whiskerRight f.fst ψ.left) F₁ ≫
      { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
            iso :=
              y.fst.associator ψ.left F₁ ≪≫
                y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (y.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight y.iso ψ.base ≪≫
                      y.snd.associator G ψ.base ≪≫
                        y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (y.snd.associator ψ.right G₁).symm }.iso.hom =
    { fst := x.fst ⋙ ψ.left, snd := x.snd ⋙ ψ.right,
            iso :=
              x.fst.associator ψ.left F₁ ≪≫
                x.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (x.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight x.iso ψ.base ≪≫
                      x.snd.associator G ψ.base ≪≫
                        x.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (x.snd.associator ψ.right G₁).symm }.iso.hom ≫
      whiskerRight (whiskerRight f.snd ψ.right) G₁

Tactic:
ext x
            simp [← Functor.map_comp_assoc]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : Mon (C ⥤ C)
X : C
⊢ M.X.map (μ.app X) ≫ μ.app X = μ.app (M.X.obj X) ≫ μ.app X

Tactic:
simpa [-MonObj.mul_assoc] using! congrArg (fun t ↦ t.app X) (mul_assoc M.X)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ eHomWhiskerRight C f Y = (pre f).app Y

Tactic:
change (λ_ _).inv ≫ curry' f ▷ _ ≫ comp X₁ X₂ Y = _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ (λ_ ((ihom X₂).obj Y)).inv ≫ curry' f ▷ (ihom X₂).obj Y ≫ comp X₁ X₂ Y = (pre f).app Y
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
⊢ (expComparison F A).whiskerBottom (pre (F.map f)) = (expComparison F A').whiskerTop (pre f)

Tactic:
unfold expComparison MonoidalClosed.pre
  have vcomp1 := mateEquiv_conjugateEquiv_vcomp
    (ihom.adjunction A) (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))
    ((prodComparisonNatIso F A).inv) (((curriedTensor D).map (F.map f)))
  have vcomp2 := conjugateEquiv_mateEquiv_vcomp
    (ihom.adjunction A) (ihom.adjunction A') (ihom.adjunction (F.obj A'))
    (((curriedTensor C).map f)) ((prodComparisonNatIso F A').inv)
  rw [← vcomp1, ← vcomp2]
  unfold TwoSquare.whiskerLeft TwoSquare.whiskerRight
  congr 1
  apply congr_arg
  ext B
  simp only [Functor.comp_obj, curriedTensor_obj_obj, prodComparisonNatIso_inv,
    NatTrans.comp_app, Functor.whiskerLeft_app, curriedTensor_map_app, NatIso.isIso_inv_app,
    Functor.whiskerRight_app, IsIso.eq_inv_comp, prodComparisonNatTrans_app]
  rw [← prodComparison_inv_natural_whiskerRight F f]
  simp

Goal state after: