mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C ⊕ C'
f : x ⟶ y
⊢ x = y

Tactic:
by
    cases f with
    | inl x y f => rw [(by assumption : IsDiscrete C).eq_of_hom f]
    | inr x y f => rw [(by assumption : IsDiscrete C').eq_of_hom f]

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✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
⊢ (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      (ρ_ (((diagram V F₁ F₂).obj (Opposite.op i)).obj i)).inv ▷ ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
        (((diagram V F₁ F₂).obj (Opposite.op i)).obj i ◁ (eHomEquiv V) (F₂.map f)) ▷
            ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (F₂.obj j) ▷
              ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj j) (F₃.obj j) =
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
      eHomWhiskerRight V (F₁.map f) (F₃.obj j)

Tactic:
have := end_.condition (diagram 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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫ ((diagram V F₁ F₂).obj (Opposite.op i)).map f =
    end_.π (diagram V F₁ F₂) j ≫ ((diagram V F₁ F₂).map f.op).app j
⊢ (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      (ρ_ (((diagram V F₁ F₂).obj (Opposite.op i)).obj i)).inv ▷ ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
        (((diagram V F₁ F₂).obj (Opposite.op i)).obj i ◁ (eHomEquiv V) (F₂.map f)) ▷
            ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (F₂.obj j) ▷
              ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj j) (F₃.obj j) =
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
      eHomWhiskerRight V (F₁.map f) (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✝⁵ : 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:
by
  ext j
  dsimp
  rw [enriched_assoc]

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

Goal state before:

Tactic:
(X.ρ g⁻¹ ≫ f.hom) x
          = ((Y.ρ g⁻¹ * Y.ρ g)).hom y.val := by rw [f.comm, FintypeCat.comp_apply, h]; rfl
        _ = y.val := by
          simp [← map_mul, inv_mul_cancel, Action.ρ_one, FintypeCat.id_hom]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
⊢ σ = τ

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
X : C
x : (F.obj X).obj
⊢ (ConcreteCategory.hom (σ.hom.app X)) x = (ConcreteCategory.hom (τ.hom.app X)) x
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
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
⊢ t = s

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
X : C
x : (F.obj X).obj
⊢ (ConcreteCategory.hom (t.app X)) x = (ConcreteCategory.hom (s.app X)) x
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 A : C
a : (F.obj A).obj
isGalois✝² : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝¹ : IsGalois B
u : A ⟶ X
v : B ⟶ X
h : (ConcreteCategory.hom (F.map u)) a = (ConcreteCategory.hom (F.map v)) b
Z : C
z : (F.obj Z).obj
isGalois✝ : IsGalois Z
f :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj
hf :
  (ConcreteCategory.hom (F.map f)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).pt
h✝ : True
g :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).obj
hg :
  (ConcreteCategory.hom (F.map g)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).pt
⊢ (ConcreteCategory.hom (F.map u)) (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).pt =
    (ConcreteCategory.hom (F.map v)) ((ConcreteCategory.hom (F.map g)) z)

Tactic:
hg,

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝² : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝¹ : IsGalois B
u : A ⟶ X
v : B ⟶ X
h : (ConcreteCategory.hom (F.map u)) a = (ConcreteCategory.hom (F.map v)) b
Z : C
z : (F.obj Z).obj
isGalois✝ : IsGalois Z
f :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj
hf :
  (ConcreteCategory.hom (F.map f)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).pt
h✝ : True
g :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).obj
hg :
  (ConcreteCategory.hom (F.map g)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).pt
⊢ (ConcreteCategory.hom (F.map u)) (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).pt =
    (ConcreteCategory.hom (F.map v)) (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).pt
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)

Tactic:
obtain ⟨ι, hf, f, u, hc⟩ := has_decomp_connected_components' X

Goal state after:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
g h : G
⊢ NatIso.ofComponents (isoOnObj F (g * h)) ⋯ =
    NatIso.ofComponents (isoOnObj F g) ⋯ * NatIso.ofComponents (isoOnObj F h) ⋯

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
g h : G
X : C
x : (F.obj X).obj
⊢ (ConcreteCategory.hom ((NatIso.ofComponents (isoOnObj F (g * h)) ⋯).hom.app X)) x =
    (ConcreteCategory.hom ((NatIso.ofComponents (isoOnObj F g) ⋯ * NatIso.ofComponents (isoOnObj F h) ⋯).hom.app X)) x
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : (X : C) → MulAction G (F.obj X).obj
inst✝³ : IsNaturalSMul F G
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
t : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).obj
φ : Aut X
hg :
  g • (ConcreteCategory.hom (F.map φ.hom)) y = (ConcreteCategory.hom (t.app X)) ((ConcreteCategory.hom (F.map φ.hom)) y)
this : Function.Injective ⇑(ConcreteCategory.hom (F.map φ.hom))
⊢ g • (ConcreteCategory.hom (F.map φ.hom)) y = (ConcreteCategory.hom (F.map φ.hom)) ((ConcreteCategory.hom (t.app X)) y)

Tactic:
hg,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : (X : C) → MulAction G (F.obj X).obj
inst✝³ : IsNaturalSMul F G
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
t : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).obj
φ : Aut X
hg :
  g • (ConcreteCategory.hom (F.map φ.hom)) y = (ConcreteCategory.hom (t.app X)) ((ConcreteCategory.hom (F.map φ.hom)) y)
this : Function.Injective ⇑(ConcreteCategory.hom (F.map φ.hom))
⊢ (ConcreteCategory.hom (t.app X)) ((ConcreteCategory.hom (F.map φ.hom)) y) =
    (ConcreteCategory.hom (F.map φ.hom)) ((ConcreteCategory.hom (t.app X)) y)
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
⊢ ∃ a, (toAut F G) a = t

Tactic:
let c : Set G := ⋂ i, cl i

Goal state after:
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
⊢ ∃ a, (toAut F G) a = t
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : FiberFunctor F
g : Aut F
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
⊢ g = 1

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : FiberFunctor F
g : Aut F
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
X : C
x : (F.obj X).obj
⊢ (ConcreteCategory.hom (g.hom.app X)) x = (ConcreteCategory.hom ((Iso.hom 1).app X)) x
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ ∀ {X Y : Symmetrify V} (f : X ⟶ Y),
    (Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (reverse f) =
      reverse ((Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)

Tactic:
· rintro X Y f
    simp only [← Functor.toPrefunctor_comp, Prefunctor.comp_map, Paths.of_map]
    change Φ.map (Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
      Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
    have := Functor.map_inv Φ ((Quotient.functor redStep).toPrefunctor.map f.toPath)
    convert! this <;> simp only [Groupoid.inv_eq_inv]

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

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d✝ : D
c d : C
g : c ⟶ d
ec : φ.obj c = d✝
ed : φ.obj d = d✝
eg : g ∈ S.arrows c d
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d✝

Tactic:
exact ⟨c, ⟨mem_objs_of_src S eg, ec⟩⟩

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

Goal state before:
pp: case refine_1
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
⊢ (if x : m < n + 1 then M m else N m) = if x : m < n then M m else N m

pp: case refine_2
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
h' : m < n + 1
⊢ (if x : m < n + 1 then M m else N m) = M m

pp: case refine_3
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
h' : m < n + 1
⊢ N m = if x : m < n then M m else N m

pp: case refine_4
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
h' : ¬m < n + 1
⊢ (if x : m < n + 1 then M m else N m) = if x : m < n then M m else N m

Tactic:
all_goals split_ifs; try rfl; try lia

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

Goal state before:
pp: case assoc
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ U✝ V✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ ((f✝.comp g✝).comp h✝) = projectMapAux f✝¹ (f✝.comp (g✝.comp h✝))

Tactic:
| assoc =>

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (project f✝).map f ▷ (project f✝).obj x✝ ≫ (Iso.refl ((project f✝).obj Y✝ ⊗ (project f✝).obj x✝)).hom =
    (Iso.refl ((project f✝).obj X✝ ⊗ (project f✝).obj x✝)).hom ≫ (project f✝).map (f ▷ x✝)

Tactic:
induction f using Quotient.recOn

Goal state after:
case f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (project f).map ⟦a✝⟧ ▷ (project f).obj x✝ ≫ (Iso.refl ((project f).obj Y✝ ⊗ (project f).obj x✝)).hom =
    (Iso.refl ((project f).obj X✝ ⊗ (project f).obj x✝)).hom ≫ (project f).map (⟦a✝⟧ ▷ x✝)

case h
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ b✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p✝ : a✝ ≈ b✝
⊢ ⋯ = ⋯
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (project f✝).map f ▷ (project f✝).obj x✝ ≫ (Iso.refl ((project f✝).obj Y✝ ⊗ (project f✝).obj x✝)).hom =
    (Iso.refl ((project f✝).obj X✝ ⊗ (project f✝).obj x✝)).hom ≫ (project f✝).map (f ▷ x✝)

Tactic:
induction f using Quotient.recOn
        all_goals aesop

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
⊢ (project f✝).obj x✝ ◁ (project f✝).map f ≫ (Iso.refl ((project f✝).obj x✝ ⊗ (project f✝).obj Y✝)).hom =
    (Iso.refl ((project f✝).obj x✝ ⊗ (project f✝).obj X✝)).hom ≫ (project f✝).map (x✝ ◁ f)

Tactic:
induction f using Quotient.recOn

Goal state after:
case f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (project f).obj x✝ ◁ (project f).map ⟦a✝⟧ ≫ (Iso.refl ((project f).obj x✝ ⊗ (project f).obj Y✝)).hom =
    (Iso.refl ((project f).obj x✝ ⊗ (project f).obj X✝)).hom ≫ (project f).map (x✝ ◁ ⟦a✝⟧)

case h
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
a✝ b✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p✝ : a✝ ≈ b✝
⊢ ⋯ = ⋯
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
⊢ (project f✝).obj x✝ ◁ (project f✝).map f ≫ (Iso.refl ((project f✝).obj x✝ ⊗ (project f✝).obj Y✝)).hom =
    (Iso.refl ((project f✝).obj x✝ ⊗ (project f✝).obj X✝)).hom ≫ (project f✝).map (x✝ ◁ f)

Tactic:
induction f using Quotient.recOn
        all_goals aesop

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso (adj.toMonad.forget.map ((comparisonAdjunction adj).unit.app X))

Tactic:
change IsIso ((comparisonAdjunction adj).unit.app X).f

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso ((comparisonAdjunction adj).unit.app X).f
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso (adj.toMonad.forget.map ((comparisonAdjunction adj).unit.app X))

Tactic:
change IsIso ((comparisonAdjunction adj).unit.app X).f

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso ((comparisonAdjunction adj).unit.app X).f
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
d₁✝ d₂✝ : Dᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : Cᵒᵖ
f : unop d₂✝ ⟶ unop d₁✝
g : unop c₂✝ ⟶ unop c₁✝
h : unop c₄✝ ⟶ unop c₃✝
⊢ (Quiver.Hom.unop (op f) ⊙ᵣₘ (op g ⊗ₘ op h).unop).op ≫ (αᵣ (unop d₂✝) (unop c₂✝) (unop c₄✝)).symm.op.hom =
    (αᵣ (unop d₁✝) (unop c₁✝) (unop c₃✝)).symm.op.hom ≫
      ((Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op.unop ⊙ᵣₘ Quiver.Hom.unop (op h)).op

Tactic:
by
        apply Quiver.Hom.unop_inj
        have := (αᵣ (unop _) (unop _) (unop _)).inv ≫=
          MonoidalRightAction.actionAssocIso_hom_naturality f g h
        simp only [Iso.inv_hom_id_assoc] at this
        simp [← this]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom =
    (αₗ N N Y).hom ≫ N ⊴ₗ ((e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom) ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom

Tactic:
have : μ[N] ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) =
        ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ[M] ⊵ₗ X := by
      rw [actionHom_def', action_exchange, ← comp_actionHomLeft_assoc, IsMonHom.mul_hom,
        comp_actionHomLeft, Category.assoc, ← action_exchange, actionHom_def']
      nth_rw 2 [action_exchange]
      rw [Category.assoc]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
this : μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X
⊢ μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom =
    (αₗ N N Y).hom ≫ N ⊴ₗ ((e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom) ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom