mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q Q' : ObjectProperty C
h : Q ≤ Q'
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), ofObjectProperty P Q f → ofObjectProperty P Q' f

Tactic:
_

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q Q' : ObjectProperty C
h : Q ≤ Q'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ofObjectProperty P Q f✝ → ofObjectProperty P Q' f✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
C : Type u_3
inst✝ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
⊢ ∀ [inst : Category.{w₂, w₁} J], PreservesLimitsOfShape J F

Tactic:
_

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesLimitsOfShape J F
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
C : Type u_3
inst✝ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
⊢ ∀ [inst : Category.{w₂, w₁} J], PreservesColimitsOfShape J F

Tactic:
_

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape J F
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteLimits V
J✝ : Type
⊢ ∀ [inst : SmallCategory J✝] [FinCategory J✝],
    PreservesLimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
_

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
inst✝¹ : HasFiniteLimits V
J✝ : Type
inst✝ : SmallCategory J✝
⊢ ∀ [FinCategory J✝], PreservesLimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
inst✝¹ : HasFiniteLimits V
J✝ : Type
inst✝ : SmallCategory J✝
⊢ ∀ [FinCategory J✝], PreservesLimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
_

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : HasFiniteLimits V
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteColimits V
J✝ : Type
⊢ ∀ [inst : SmallCategory J✝] [FinCategory J✝],
    PreservesColimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
_

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
inst✝¹ : HasFiniteColimits V
J✝ : Type
inst✝ : SmallCategory J✝
⊢ ∀ [FinCategory J✝], PreservesColimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
inst✝¹ : HasFiniteColimits V
J✝ : Type
inst✝ : SmallCategory J✝
⊢ ∀ [FinCategory J✝], PreservesColimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
_

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : HasFiniteColimits V
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesColimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this : Abelian D := abelian L P
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), PreservesLimit (parallelPair f 0) L

Tactic:
_

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this : Abelian D := abelian L P
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), PreservesLimit (parallelPair f 0) L
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this : Abelian D := abelian L P
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), PreservesColimit (parallelPair f 0) L

Tactic:
_

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this : Abelian D := abelian L P
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), PreservesColimit (parallelPair f 0) L
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
h : H.FullyFaithful
this✝ : H.Full
this : H.Faithful
⊢ IsIso t.adj₁.unit

Tactic:
by
      rw [t.isIso_unit_iff_isIso_counit]
      infer_instance

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

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

Tactic:
by
    rintro a b c f g h i ⟨η⟩ ⟨θ⟩
    exact Quot.sound (Rel.whisker_exchange η θ)

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
⊢ ∀ (f_1 : f ⟶ g),
    (𝟭 (a ⟶ b)).map f_1 ≫ ((λ_ g).symm ≪≫ normalizeIso nil g).hom =
      ((λ_ f).symm ≪≫ normalizeIso nil f).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map f_1

Tactic:
η

Goal state after:
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ (𝟭 (a ⟶ b)).map η ≫ ((λ_ g).symm ≪≫ normalizeIso nil g).hom =
    ((λ_ f).symm ≪≫ normalizeIso nil f).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map η
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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), Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ

Tactic:
η

Goal state after:
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), Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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),
    Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
      (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv

Tactic:
η

Goal state after:
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
⊢ Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
    (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ : FreeBicategory B
⊢ ∀ {b c : FreeBicategory B} {f g : a✝ ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv

Tactic:
_

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ : FreeBicategory B
⊢ ∀ {c : FreeBicategory B} {f g : a✝ ⟶ b✝} (η : f ⟶ g) (h : b✝ ⟶ c),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ : FreeBicategory B
⊢ ∀ {c : FreeBicategory B} {f g : a✝ ⟶ b✝} (η : f ⟶ g) (h : b✝ ⟶ c),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv

Tactic:
_

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
⊢ ∀ {f g : a✝ ⟶ b✝} (η : f ⟶ g) (h : b✝ ⟶ c✝),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
⊢ ∀ {f g : a✝ ⟶ b✝} (η : f ⟶ g) (h : b✝ ⟶ c✝),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv

Tactic:
_

Goal state after:
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 : a✝ ⟶ b✝} (η : f✝ ⟶ g) (h : b✝ ⟶ c✝),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f✝ ≫ h))).hom ≫
        Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 : a✝ ⟶ b✝} (η : f✝ ⟶ g) (h : b✝ ⟶ c✝),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f✝ ≫ h))).hom ≫
        Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv

Tactic:
_

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
⊢ ∀ (η : f✝ ⟶ g✝) (h : b✝ ⟶ c✝),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f✝ ≫ h))).hom ≫
        Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g✝ ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
⊢ ∀ (η : f✝ ⟶ g✝) (h : b✝ ⟶ c✝),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f✝ ≫ h))).hom ≫
        Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g✝ ≫ h))).inv

Tactic:
η

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
⊢ ∀ (h : b✝ ⟶ c✝),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f✝ ≫ h))).hom ≫
        Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g✝ ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
        F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv

Tactic:
rw [← cancel_epi (F.mapComp' f₀₂ f₂₃ f).hom, Iso.hom_inv_id]

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ 𝟙 (F.map f) =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
          F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X✝ : Type u
C✝ : Cat
C : Cat
X : Type u
⊢ (connectedComponents.obj C ⟶ X) ≃ (C ⟶ typeToCat.obj X)

Tactic:
by
      refine TypeCat.homEquiv.trans ?_
      exact (ConnectedComponents.typeToCatHomEquiv _ _).trans
        (Functor.equivCatHom _ _)

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

Goal state before:
pp: X : Type u
C : Cat
x✝² x✝¹ : Type u
x✝ : x✝² ⟶ x✝¹
⊢ (typeToCat ⋙ connectedComponents).map x✝ ≫
      ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x✝¹)) (𝟙 typeToCat.obj x✝¹).toFunctor =
    ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x✝²)) (𝟙 typeToCat.obj x✝²).toFunctor ≫ (𝟭 (Type u)).map x✝

Tactic:
ext xcc
          obtain ⟨x, h⟩ := Quotient.exists_rep xcc
          cat_disch

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

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

Tactic:
refine ⟨fun ⟨w, hw, h⟩ ↦ ?_, fun h ↦ ⟨b, Part.mem_toOption.mp h.symm, rfl⟩⟩
            rw [Subtype.ext_iff] at h
            dsimp at h
            rw [h]
            rw [← Part.mem_toOption, mem_def] at hw
            exact hw.symm

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
by
    let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
    rw [WellFounded.fixF_eq] at h₂
    simp only [Part.mem_assert_iff] at h₂
    obtain ⟨h₂, h₃⟩ := h₂
    split at h₃
    next e => simp only [Part.mem_some_iff] at h₃; subst b; exact Or.inl ⟨h₂, e⟩
    next e => exact Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
X✝ : C₂
⊢ ∀ ⦃Y : C₂⦄ (f : X✝ ⟶ Y), W₂ f → IsIso ((prodLift₁ F hF).flip.map f)

Tactic:
_

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
X✝ Y✝ : C₂
⊢ ∀ (f : X✝ ⟶ Y✝), W₂ f → IsIso ((prodLift₁ F hF).flip.map f)
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
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
⊢ g₁ ≫ Sigma.desc e = g₂ ≫ Sigma.desc e

Tactic:
by
  apply_fun ((Sigma.desc fun a ↦ pullback.fst g₁ (Sigma.ι X a)) ≫ ·) using
    (fun a b ↦ (cancel_epi _).mp)
  ext a
  simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_ι_app]
  rw [← Category.assoc, pullback.condition]
  simp only [Category.assoc, colimit.ι_desc, Cofan.mk_ι_app]
  apply_fun ((Sigma.desc fun a ↦ pullback.fst (pullback.fst _ _ ≫ g₂) (Sigma.ι X a)) ≫ ·)
    using (fun a b ↦ (cancel_epi _).mp)
  ext b
  simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_ι_app]
  simp only [← Category.assoc]
  rw [(Category.assoc _ _ g₂), pullback.condition]
  simp only [Category.assoc, colimit.ι_desc, Cofan.mk_ι_app]
  rw [← Category.assoc]
  apply h
  apply_fun (pullback.fst g₁ (Sigma.ι X a) ≫ ·) at hg
  rw [← Category.assoc, pullback.condition] at hg
  simp only [Category.assoc, colimit.ι_desc, Cofan.mk_ι_app] at hg
  apply_fun ((Sigma.ι (fun a ↦ pullback _ _) b) ≫ (Sigma.desc fun a ↦
    pullback.fst (pullback.fst _ _ ≫ g₂) (Sigma.ι X a)) ≫ ·) at hg
  simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_ι_app] at hg
  simp only [← Category.assoc] at hg
  rw [(Category.assoc _ _ g₂), pullback.condition] at hg
  simpa using hg

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ (λ_ Y).hom =
    L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y

Tactic:
simp only [← tensorHom_id, ← id_tensorHom, ← tensor_comp, comp_id, id_comp,
    ← tensor_comp_assoc, id_comp]
  congr 3
  exact (comp_id _).symm

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst✝ : p.IsHomLift f ψ
⊢ R = S

Tactic:
rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]

Goal state after:
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
g h : M
x : J.obj (SingleObj.star M)
⊢ (ConcreteCategory.hom (J.map (g * h))) x = (ConcreteCategory.hom (J.map h ≫ J.map g)) x

Tactic:
← SingleObj.comp_as_mul

Goal state after:
M G : Type v
inst✝¹ : Monoid M
inst✝ : Group G
J : SingleObj M ⥤ Type u
g h : M
x : J.obj (SingleObj.star M)
⊢ (ConcreteCategory.hom (J.map (h ≫ g))) x = (ConcreteCategory.hom (J.map h ≫ J.map g)) x

case y
M G : Type v
inst✝¹ : Monoid M
inst✝ : Group G
J : SingleObj M ⥤ Type u
g h : M
x : J.obj (SingleObj.star M)
⊢ SingleObj M
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : X ⟶ Y
⊢ Mono (F.map f) → Mono f

Tactic:
_

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : X ⟶ Y
a✝ : Mono (F.map f)
⊢ Mono f
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ Nonempty (IsInitial (F.obj X)) ↔ IsEmpty (F.obj X).obj

Tactic:
exact Concrete.initial_iff_empty_of_preserves_of_reflects (F.obj X)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := ⋯
this✝ : FiberFunctor F' := ⋯
this : (functorToContAction F').EssSurj
f✝ : Aut F ≃ₜ* Aut F' := ⋯
equiv : ContAction FintypeCat (Aut F') ≌ ContAction FintypeCat (Aut F) := ⋯
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ((functorToContAction F).map f ≫
          (ObjectProperty.isoMk Action.IsContinuous
              (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj Y✝)) ⋯)).hom).hom.hom =
    ((ObjectProperty.isoMk Action.IsContinuous
              (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X✝)) ⋯)).hom ≫
          (functorToContAction F' ⋙ equiv.functor).map f).hom.hom

Tactic:
exact FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (F.map f)

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ F.preimage (eqToHom ⋯ ≫ (x✝¹ ≫ x✝) ≫ eqToHom ⋯) =
    F.preimage (eqToHom ⋯ ≫ x✝¹ ≫ eqToHom ⋯) ≫ F.preimage (eqToHom ⋯ ≫ x✝ ≫ eqToHom ⋯)

Tactic:
simp [← preimage_comp]

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

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

Tactic:
· rintro ⟨a, b, g, rfl, rfl, hg, rfl⟩; rw [← eq_conj_eqToHom]; constructor; exact hg

Goal state after:
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
hφ' : im φ hφ = ⊤
⊢ Function.Surjective φ.obj

Tactic:
rintro d
  rw [← mem_im_objs_iff _ hφ, hφ']
  apply mem_top_objs

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

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d : D
⊢ 𝟙 d ∈ (map φ hφ S).arrows d d

Tactic:
by
      obtain ⟨c, rfl⟩ := obj_surjective_of_im_eq_top φ hφ hφ' d
      change Map.Arrows φ hφ S _ _ (𝟙 _); rw [← Functor.map_id]
      constructor; exact Sn.wide c

Goal state after: