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

Goal state before:
pp: ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
f :
  s.pt ⟶
    { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt
h : ∀ (j : Discrete ι), f ≫ { hom := ↾fun x ↦ x j.as, comm := ⋯ } = s.π.app j
x : s.pt.V
j : ι
⊢ (ConcreteCategory.hom f.hom) x j = (ConcreteCategory.hom (f ≫ { hom := ↾fun x ↦ x { as := j }.as, comm := ⋯ }).hom) x

Tactic:
rfl

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

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v g x : G
⊢ ↑g * (↑x * (↑v)⁻¹) = g • (↑x * (↑v)⁻¹)

Tactic:
rfl

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

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : Fintype (G ⧸ H)
h : N ≤ H
g a✝ : G
⊢ (ConcreteCategory.hom
        ((ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g ≫ FintypeCat.homMk (Quotient.lift (fun x ↦ ⟦x⟧) ⋯)))
      ⟦a✝⟧ =
    (ConcreteCategory.hom
        (FintypeCat.homMk (Quotient.lift (fun x ↦ ⟦x⟧) ⋯) ≫ (ofMulAction G (FintypeCat.of (G ⧸ H))).ρ g))
      ⟦a✝⟧

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ Z✝ : Action V G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := F.map (f ≫ g).hom, comm := ⋯ } = { hom := F.map f.hom, comm := ⋯ } ≫ { hom := F.map g.hom, comm := ⋯ }

Tactic:
by ext; simp only [Action.comp_hom, F.map_comp]

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁴ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝³ : ConcreteCategory V FV
inst✝² : HasForget₂ V TopCat
G : Type u_4
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
X : Action V G
g h : G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ g * X.ρ h))) x =
    (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ h ≫ X.ρ g))) x

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
⊢ ⋯.hom ≫ ⋯.hom = s✝.inl

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
⊢ ⋯.hom ≫ ⋯.hom = s✝.inr

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
m✝ : Subobject.mk (pushout.desc a.arrow b.arrow ⋯) ⟶ s✝.pt
x✝¹ : ⋯.hom ≫ m✝ = s✝.inl
x✝ : ⋯.hom ≫ m✝ = s✝.inr
⊢ m✝ = ⋯.hom

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ Xᘁ.ρ h = X.ρ (inv h)ᘁ

pp: case x
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

pp: case y
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ (ᘁX).ρ h = ᘁX.ρ (inv h)

pp: case x
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H

pp: case y
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H

Tactic:
rfl

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✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝¹ : G
x✝ : (leftRegular G ⊗ X).V
⊢ (ConcreteCategory.hom (X.ρ x✝.1⁻¹)) x✝.2 = (ConcreteCategory.hom (1 x✝¹)) ((ConcreteCategory.hom (X.ρ x✝.1⁻¹)) x✝.2)

Tactic:
rfl

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

Goal state before:
pp: case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
⊢ (Fin.consEquiv fun x ↦ G)
      ({ toFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1)) g.2),
            left_inv := ⋯, right_inv := ⋯ }
          (((Fin.consEquiv fun a ↦ G).symm f).1, ((Fin.consEquiv fun a ↦ G).symm f).2 0, fun i ↦
            (((Fin.consEquiv fun a ↦ G).symm f).2 i.castSucc)⁻¹ * ((Fin.consEquiv fun a ↦ G).symm f).2 i.succ)).2
      0 =
    (f 0)⁻¹ * f 1

Tactic:
rfl

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

Goal state before:
pp: case succ.succ
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
i✝ : Fin n
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
⊢ (Fin.consEquiv fun x ↦ G)
      ({ toFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1)) g.2),
            left_inv := ⋯, right_inv := ⋯ }
          (((Fin.consEquiv fun a ↦ G).symm f).1, ((Fin.consEquiv fun a ↦ G).symm f).2 0, fun i ↦
            (((Fin.consEquiv fun a ↦ G).symm f).2 i.castSucc)⁻¹ * ((Fin.consEquiv fun a ↦ G).symm f).2 i.succ)).2
      i✝.succ =
    (f i✝.castSucc.succ)⁻¹ * f i✝.succ.succ

Tactic:
rfl

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

Goal state before:
pp: case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) 0 = g

Tactic:
rfl

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

Goal state before:
pp: case succ.succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
i : Fin (n + 1)
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) i.succ = (g • Fin.partialProd f) i.succ

Tactic:
simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using! congrFun (hn (g * f 0) (Fin.tail f)) i

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
⊢ IsIso t.adj₁.unit ↔ IsIso t.adj₂.counit

Tactic:
by
  let adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
  constructor
  · intro h
    let idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso t.adj₁.unit).symm
    exact t.adj₂.isIso_counit_of_iso (idAdj.rightAdjointUniq id)
  · intro h
    let adjId : F ⋙ G ⊣ 𝟭 C := adj.ofNatIsoRight (asIso t.adj₂.counit)
    exact t.adj₁.isIso_unit_of_iso (adjId.leftAdjointUniq id)

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
⊢ Epi (t.rightToLeft.app X) ↔ Epi (H.map (t.adj₁.unit.app X))

Tactic:
rw [← epi_comp_iff_of_isIso _ (t.adj₂.unit.app (F.obj X)), rightToLeft_app_adj₂_unit_app]

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

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 : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
⊢ (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint

Tactic:
refine ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft ?_).isLeftAdjoint
    exact Functor.isoWhiskerLeft L (Comonad.comparisonForget (comonadicAdjunction F)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ (f ≫ g) ≫ h = (f' ≫ g') ≫ h'

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ f' ≫ g' ≫ h' = f ≫ g ≫ h

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ f ≫ g ≫ h = f' ≫ g' ≫ h'

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ (f' ≫ g') ≫ h' = (f ≫ g) ≫ h

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h✝ : b✝ ⟶ c✝
η✝ : Hom₂ f✝ g✝
ih : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (Hom.comp f✝ h✝) = normalizeAux x✝ (Hom.comp g✝ h✝)

Tactic:
apply congr_arg₂ _ (congr_fun ih _) rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.id
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.associator
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
x✝ : Path a a✝
⊢ normalizeAux x✝ ((f✝ ≫ g✝) ≫ h✝) = normalizeAux x✝ (f✝ ≫ g✝ ≫ h✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.associator_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ g✝ ≫ h✝) = normalizeAux x✝ ((f✝ ≫ g✝) ≫ h✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.right_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ 𝟙 b✝) = normalizeAux x✝ f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.right_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ (f✝ ≫ 𝟙 b✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.left_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (𝟙 a✝ ≫ f✝) = normalizeAux x✝ f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.left_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ (𝟙 a✝ ≫ f✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case mk.mk
B : Type u
inst✝ : Quiver B
a b c : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
θ✝ : g ⟶ h
θ : Hom₂ g h
i : b ⟶ c
⊢ Quot.map (Hom₂.whisker_right i) ⋯ (Quot.mk Rel η ≫ Quot.mk Rel θ) =
    Quot.map (Hom₂.whisker_right i) ⋯ (Quot.mk Rel η) ≫ Quot.map (Hom₂.whisker_right i) ⋯ (Quot.mk Rel θ)

Tactic:
exact Quot.sound (Rel.comp_whisker_right i η θ)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case id
B : Type u
inst✝ : Quiver B
b c a✝ a : B
f : Hom a a✝
⊢ normalizeAux nil (f.comp (Hom.id a✝)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.id a✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case of
B : Type u
inst✝ : Quiver B
b c a✝ b✝ : B
f✝ : a✝ ⟶ b✝
a : B
f : Hom a a✝
⊢ normalizeAux nil (f.comp (Hom.of f✝)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.of f✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case nil
B : Type u
inst✝ : Quiver B
a b : B
⊢ (inclusionPath a a ⋙ (normalize B).mapFunctor a a).obj { as := nil } = (𝟭 (Discrete (Path a a))).obj { as := nil }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case cons
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih : normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ }) = a✝¹
⊢ ((inclusionPath a c✝ ⋙ (normalize B).mapFunctor a c✝).obj { as := a✝¹.cons a✝ }).as =
    ((𝟭 (Discrete (Path a c✝))).obj { as := (normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ })).cons a✝ }).as

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case f.f
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
a✝¹ : Hom₂ f g
a✝ : Hom₂ g h
⊢ Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝¹ ≫ Quot.mk Rel a✝) =
    Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝¹) ≫ Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case f.h
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
θ : g ⟶ h
a✝¹ : Hom₂ f g
a✝ b✝ : Hom₂ g h
p✝ : Rel a✝ b✝
⊢ ⋯ = ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case h
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
a✝ b✝ : Hom₂ f g
p✝ : Rel a✝ b✝
⊢ ⋯ = ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case h
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
a✝ b✝ : Hom₂ g h
p✝ : Rel a✝ b✝
⊢ ⋯ = ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β

Tactic:
θ.naturality_naturality

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (θ.naturality f ≫ θ.app a ◁ H.map₂ β) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
G H : B ⥤ᵒᵖᴸ C
θ : OplaxTrans G H
a : B
a' : C
f : a' ⟶ G.obj a
⊢ f ◁ θ.naturality (𝟙 a) ≫ f ◁ θ.app a ◁ H.mapId a =
    f ◁ G.mapId a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv

Tactic:
by
  simp_rw [← whiskerLeft_comp, naturality_id]

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

Goal state before:
pp: case mk.mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Wₗ Wᵣ : MorphismProperty C
c c' : C
S S' : Span Wₗ Wᵣ c c'
hom✝¹ : S.apex ⟶ S'.apex
hom_l✝¹ : hom✝¹ ≫ S'.l = S.l
hom_r✝¹ : hom✝¹ ≫ S'.r = S.r
hom✝ : S.apex ⟶ S'.apex
hom_l✝ : hom✝ ≫ S'.l = S.l
hom_r✝ : hom✝ ≫ S'.r = S.r
h : { hom := hom✝¹, hom_l := hom_l✝¹, hom_r := hom_r✝¹ }.hom = { hom := hom✝, hom_l := hom_l✝, hom_r := hom_r✝ }.hom
⊢ { hom := hom✝¹, hom_l := hom_l✝¹, hom_r := hom_r✝¹ } = { hom := hom✝, hom_l := hom_l✝, hom_r := hom_r✝ }

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} J✝
J : Type ?u.6
inst✝ : Category.{v_1, ?u.6} J
X : Type u_1
f : ConnectedComponents J → X
x✝ : ConnectedComponents J
x : J
h : ⟦x⟧ = x✝
⊢ liftFunctor J (functorToDiscrete X f) ⟦x⟧ = f ⟦x⟧

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h ↦ { obj := x, property := ⋯ }
hf : ∀ a ∈ l, Zigzag a j₂
⊢ ({ obj := j₁, property := hj₁ } :: List.pmap f l hf).getLast ⋯ = { obj := j₂, property := ⋯ }

Tactic:
grind

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

Goal state before:
pp: X : Type u
C : Cat
x✝² x✝¹ : Cat
x✝ : x✝² ⟶ x✝¹
as✝ : objects.obj x✝²
⊢ ∀ (Y : ↑((objects ⋙ typeToCat).obj x✝²)) (f : { as := as✝ } ⟶ Y),
    ((objects ⋙ typeToCat).map x✝ ≫ x✝¹.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f ≍
      (x✝².typeToCatObjectsAdjCounitApp.toCatHom ≫ (𝟭 Cat).map x✝).toFunctor.map f

Tactic:
⟨_⟩

Goal state after:
X : Type u
C : Cat
x✝² x✝¹ : Cat
x✝ : x✝² ⟶ x✝¹
as✝¹ as✝ : objects.obj x✝²
⊢ ∀ (f : { as := as✝¹ } ⟶ { as := as✝ }),
    ((objects ⋙ typeToCat).map x✝ ≫ x✝¹.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f ≍
      (x✝².typeToCatObjectsAdjCounitApp.toCatHom ≫ (𝟭 Cat).map x✝).toFunctor.map f
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝¹ : Cat
x✝ : ↑x✝¹
⊢ (𝟭 ↑x✝¹).mapConnectedComponents ⟦x✝⟧ = ⟦x✝⟧

Tactic:
rfl

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

Goal state before:
pp: X : Type u
C : Cat
X✝ Y✝ Z✝ : Cat
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ (x✝².toFunctor ⋙ x✝¹.toFunctor).mapConnectedComponents ⟦x✝⟧ =
    x✝¹.toFunctor.mapConnectedComponents (x✝².toFunctor.mapConnectedComponents ⟦x✝⟧)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j k : J
hY : ConnectedComponents.objectProperty (Quotient.mk'' j) k
f : { obj := j, property := ⋯ }.obj ⟶ { obj := k, property := hY }.obj
⊢ Sigma.SigmaHom.mk { hom := f } = Sigma.SigmaHom.mk { hom := (decomposedTo J).map (Sigma.SigmaHom.mk { hom := f }) }

Tactic:
rfl

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

Goal state before:
pp: α β : PartialFun
e : α ≃ β
⊢ PFun.id α = 𝟙 α

Tactic:
rfl

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

Goal state before:
pp: α β : PartialFun
e : α ≃ β
⊢ PFun.id β = 𝟙 β

Tactic:
rfl

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

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ ∀ (x : ¬f.toFun a = Y.point) (x_1 : ¬g.toFun (f.toFun a) = Z.point),
    ⟨g.toFun (f.toFun a), ⋯⟩ = ⟨c, hc⟩ → c = g.toFun (f.toFun a)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
α✝ : Type u_7
f : α →. α✝
a : α
Dom✝ : Prop
get✝ : Dom✝ → α✝
⊢ Part.map id { Dom := Dom✝, get := get✝ } = { Dom := Dom✝, get := get✝ }

Tactic:
rfl

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

Goal state before:
pp: case none
X : PartialFun
⊢ ↑(ConcreteCategory.hom
          (partialFunToPointed.map
              ((NatIso.ofComponents
                      (fun X ↦
                        PartialFun.Iso.mk
                          { toFun := fun a ↦ ⟨some a, ⋯⟩, invFun := fun a ↦ Option.get ↑a ⋯, left_inv := ⋯,
                            right_inv := ⋯ })
                      ⋯).hom.app
                X) ≫
            (NatIso.ofComponents (fun X ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) ⋯).hom.app
              (partialFunToPointed.obj X)))
      none =
    ↑(ConcreteCategory.hom (𝟙 (partialFunToPointed.obj X))) none

Tactic:
rfl

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

Goal state before:
pp: case some
X : PartialFun
x : X
⊢ ↑(ConcreteCategory.hom
          ({ toFun := Option.elim' none fun a ↦ some ⟨some a, ⋯⟩, map_point := ⋯ } ≫
            (Pointed.Iso.mk (Equiv.optionSubtypeNe (partialFunToPointed.obj X).point) ⋯).hom))
      (some x) =
    ↑(ConcreteCategory.hom (𝟙 (partialFunToPointed.obj X))) (some x)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ y a, a ∈ g x✝ ∧ y ∈ f a) ↔ ∃ y, (∃ y_1, y_1 ∈ f y) ∧ y ∈ g x✝

Tactic:
grind

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
s : Set γ
⊢ (f.comp g).preimage s = g.preimage (f.preimage s)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
a✝ : γ
⊢ a✝ ∈ a.bind (f.comp g) ↔ a✝ ∈ (a.bind g).bind f

Tactic:
grind

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)

Tactic:
rfl

Goal state after: