mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᵒᵖᴸ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
Γ : h ⟶ i
⊢ whiskerLeft f Γ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g Γ

Tactic:
by ext; exact whisker_exchange _ _

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᵒᵖᴸ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ

Tactic:
by ext; exact whisker_exchange _ _

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
⊢ h ◁ adj.unit ⊗≫ τ ▷ u = s.unit

Tactic:
simpa [bicategoricalComp] using LeftLift.w τ₀

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
⊢ ((LeftLift.mk h η').whisker g).unit ≫ ((t.whisker h).unit ≫ f ◁ σ) ▷ u =
    ((LeftLift.mk h η').whisker g).unit ≫ s.unit ▷ u

Tactic:
have Hσ : t.extension ◁ η' ⊗≫ σ ▷ u  = 𝟙 _ ⊗≫ τ := by
        simpa [bicategoricalComp] using (H' _).fac (.mk _ <| (ρ_ _).hom ≫ τ)
      dsimp only [LeftLift.whisker_lift, StructuredArrow.mk_right, LeftLift.whisker_unit,
        StructuredArrow.mk_hom_eq_self, whisker_extension, whisker_unit]
      calc _
        _ = (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = t.unit ▷ (𝟙 c) ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv := by
          rw [Hσ]
          dsimp only [τ]
          bicategory
        _ = _ := by
          rw [IsKan.fac_assoc]
          dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
          bicategory

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a ⋯

Tactic:
rw [WellFounded.fixF_eq]
        -- Porting note: used to be simp [h₁, h₂]
        apply Part.mem_assert h₁
        split
        next e =>
          injection h₂.symm.trans e with h; simp [h]
        next e =>
          injection h₂.symm.trans e

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: J : Type u_1
K : Type u_2
X✝ Y✝ : Discrete J × Discrete K
x✝ : X✝ ⟶ Y✝
f₁ : X✝.1.as = Y✝.1.as
f₂ : X✝.2.as = Y✝.2.as
⊢ { as := (X✝.1.as, X✝.2.as) } = { as := (Y✝.1.as, Y✝.2.as) }

Tactic:
rw [f₁, f₂]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.EnrichedCat

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u₁
inst✝¹ : EnrichedCategory V D
E : Type u₂
inst✝ : EnrichedCategory V E
F G : EnrichedFunctor V C D
H I : EnrichedFunctor V D E
α : F ⟶ G
β : H ⟶ I
X : C
⊢ (whiskerLeft F β ≫ whiskerRight α I).out.app X = (whiskerRight α H ≫ whiskerLeft G β).out.app X

Tactic:
simp only [EnrichedFunctor.forget_obj, EnrichedFunctor.comp_obj,
    EnrichedFunctor.category_comp_out, NatTrans.comp_app, whiskerLeft_out_app,
    whiskerRight_out_app]

Goal state after:
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u₁
inst✝¹ : EnrichedCategory V D
E : Type u₂
inst✝ : EnrichedCategory V E
F G : EnrichedFunctor V C D
H I : EnrichedFunctor V D E
α : F ⟶ G
β : H ⟶ I
X : C
⊢ β.out.app (ForgetEnrichment.of V (F.obj («to» V X))) ≫
      homOf V (homTo V (α.out.app X) ≫ I.map (F.obj («to» V X)) (G.obj («to» V X))) =
    homOf V (homTo V (α.out.app X) ≫ H.map (F.obj («to» V X)) (G.obj («to» V X))) ≫
      β.out.app (ForgetEnrichment.of V (G.obj («to» V X)))
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ F.map (A.str ≫ strInv h) = (A.str ≫ strInv h) ≫ A.str

Tactic:
rw [Category.assoc, F.map_comp, strInv, ← Hom.h]

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

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

Tactic:
have inv_hom : φ ≫ φ' = 𝟙 a := fac p (p.map φ) φ _ (𝟙 a)

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
Module: Mathlib.CategoryTheory.Limits.FintypeCat

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
X : ι → FintypeCat
x : (i : ι) → (X i).obj
i : ι
⊢ (productEquiv X) ((productEquiv X).symm x) i = x i

Tactic:
Equiv.apply_symm_apply

Goal state after:
ι : Type u_1
inst✝ : Finite ι
X : ι → FintypeCat
x : (i : ι) → (X i).obj
i : ι
⊢ x i = x i
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
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom (F.map prod.fst)) ((fiberBinaryProductEquiv F X Y).symm (x, y)) = x

Tactic:
by
  simp only [fiberBinaryProductEquiv]
  change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.fst) _ = _
  erw [PreservesLimitPair.iso_inv_fst, Types.binaryProductIso_inv_comp_fst]
  rfl

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

Goal state before:
pp: case refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ ∀ (y : Aut B),
    (fun τ ↦ f ≫ τ.hom = σ.hom ≫ f) y →
      y =
        (evaluationEquivOfIsGalois F B ((ConcreteCategory.hom (F.map f)) a)).symm
          ((ConcreteCategory.hom (F.map (σ.hom ≫ f))) a)

Tactic:
intro τ hτ

Goal state after:
case refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
τ : Aut B
hτ : f ≫ τ.hom = σ.hom ≫ f
⊢ τ =
    (evaluationEquivOfIsGalois F B ((ConcreteCategory.hom (F.map f)) a)).symm
      ((ConcreteCategory.hom (F.map (σ.hom ≫ f))) a)
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g

Tactic:
rw [Function.comp_apply, Category.assoc, comp_autMap, ← Category.assoc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ (autMap f σ).hom) ≫ g = σ.hom ≫ f ≫ g
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) τ
X : C
x : (F.obj X).obj
this : Iso.app σ X = Iso.app τ X
⊢ (ConcreteCategory.hom (σ.hom.app X)) x = (ConcreteCategory.hom (τ.hom.app X)) x

Tactic:
rw [← Iso.app_hom, ← Iso.app_hom, this]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a ↦ F.map f.hom ≫ (a f.right).hom

Tactic:
fun_prop

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a ↦ (a f.left).hom ≫ F.map f.hom

Tactic:
fun_prop

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
fun_prop

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
g : Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj :=
  fun x ↦
    match x with
    | (σ, x) => (ConcreteCategory.hom σ.hom) x
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
let h (q : Aut F × F.obj X) : Aut (F.obj X) × F.obj X :=
      ⟨((fun p ↦ p X) ∘ autEmbedding F) q.1, q.2⟩

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
g : Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj :=
  fun x ↦
    match x with
    | (σ, x) => (ConcreteCategory.hom σ.hom) x
h : Aut F × (F.obj X).obj → Aut (F.obj X) × (F.obj X).obj := fun q ↦ (((fun p ↦ p X) ∘ ⇑(autEmbedding F)) q.1, q.2)
⊢ Continuous fun p ↦ p.1 • p.2
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
g : Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj :=
  fun x ↦
    match x with
    | (σ, x) => (ConcreteCategory.hom σ.hom) x
h : Aut F × (F.obj X).obj → Aut (F.obj X) × (F.obj X).obj := fun q ↦ (((fun p ↦ p X) ∘ ⇑(autEmbedding F)) q.1, q.2)
⊢ Continuous (g ∘ h)

Tactic:
fun_prop

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : FintypeCat ⥤ FintypeCat
X : C
⊢ Continuous fun a ↦ (mapAut (F.obj X) G) ((autEmbedding F) a X)

Tactic:
fun_prop

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 := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous fun p ↦ X.obj.V.uSwitchEquiv.symm p

Tactic:
fun_prop

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 := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous fun p ↦ (p.1, X.obj.V.uSwitchEquiv p.2)

Tactic:
fun_prop

Goal state after:
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
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝ : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.obj → G × X.V.obj := fun p ↦ (p.1, (ConcreteCategory.hom r.hom) p.2)
q : G × X.V.obj → X.V.obj := fun p ↦ (ConcreteCategory.hom (X.ρ p.1).hom) p.2
q' : G × (f i).V.obj → (f i).V.obj := fun p ↦ (ConcreteCategory.hom ((f i).ρ p.1).hom) p.2
heq : q ∘ r'' = ⇑(ConcreteCategory.hom r.hom) ∘ q'
hrinj : Function.Injective ⇑(ConcreteCategory.hom r.hom)
t₁ : TopologicalSpace (G × (f i).V.obj) := inferInstance
⊢ TopologicalSpace.induced (⇑(ConcreteCategory.hom r.hom)) inferInstance = ⊥

Tactic:
rw [← le_bot_iff]

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)
this✝ : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.obj → G × X.V.obj := fun p ↦ (p.1, (ConcreteCategory.hom r.hom) p.2)
q : G × X.V.obj → X.V.obj := fun p ↦ (ConcreteCategory.hom (X.ρ p.1).hom) p.2
q' : G × (f i).V.obj → (f i).V.obj := fun p ↦ (ConcreteCategory.hom ((f i).ρ p.1).hom) p.2
heq : q ∘ r'' = ⇑(ConcreteCategory.hom r.hom) ∘ q'
hrinj : Function.Injective ⇑(ConcreteCategory.hom r.hom)
t₁ : TopologicalSpace (G × (f i).V.obj) := inferInstance
⊢ TopologicalSpace.induced (⇑(ConcreteCategory.hom r.hom)) inferInstance ≤ ⊥
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
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝¹ : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
this✝ : ∀ (i : ι), DiscreteTopology (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.obj → G × X.V.obj := fun p ↦ (p.1, (ConcreteCategory.hom r.hom) p.2)
q : G × X.V.obj → X.V.obj := fun p ↦ (ConcreteCategory.hom (X.ρ p.1).hom) p.2
q' : G × (f i).V.obj → (f i).V.obj := fun p ↦ (ConcreteCategory.hom ((f i).ρ p.1).hom) p.2
heq : q ∘ r'' = ⇑(ConcreteCategory.hom r.hom) ∘ q'
hrinj : Function.Injective ⇑(ConcreteCategory.hom r.hom)
t₁ : TopologicalSpace (G × (f i).V.obj) := inferInstance
this : TopologicalSpace.induced (⇑(ConcreteCategory.hom r.hom)) inferInstance = ⊥
⊢ Continuous r''

Tactic:
fun_prop

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

Goal state before:
pp: case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ HomRel.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath.comp q.reverse)

Tactic:
have : HomRel.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
          (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫
            Quiver.Path.reverse q) := by
        apply HomRel.CompClosure.intro
        apply redStep.step

Goal state after:
case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this : HomRel.CompClosure redStep (q ≫ 𝟙 b✝ ≫ q.reverse) (q ≫ (f.toPath ≫ (reverse f).toPath) ≫ q.reverse)
⊢ HomRel.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath.comp q.reverse)
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
S : Subgroupoid C
⊢ ∀ {c d e : D} {p : c ⟶ d},
    p ∈ {x | Map.Arrows φ hφ S c d x} →
      ∀ {q : d ⟶ e}, q ∈ {x | Map.Arrows φ hφ S d e x} → p ≫ q ∈ {x | Map.Arrows φ hφ S c e x}

Tactic:
rintro _ _ _ _ ⟨f, hf⟩ q hq

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
e✝ c d : D
c✝ d✝ : C
f : c✝ ⟶ d✝
hf : f ∈ S.arrows c✝ d✝
q : φ.obj d✝ ⟶ e✝
hq : q ∈ {x | Map.Arrows φ hφ S (φ.obj d✝) e✝ x}
⊢ φ.map f ≫ q ∈ {x | Map.Arrows φ hφ S (φ.obj c✝) e✝ x}
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

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
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d

Tactic:
· exact fun h c d f fS => h (Map.Arrows.im f fS)

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝ b✝ c✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ h✝
⊢ NatTrans.toCatHom₂ (mapWhiskerRight (f✝ ◁ η✝).toNatTrans (𝟭 D)) =
    (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor g✝.toFunctor)).hom ≫
      (mapPair f✝.toFunctor (𝟭 D)).toCatHom ◁ NatTrans.toCatHom₂ (mapWhiskerRight η✝.toNatTrans (𝟭 D)) ≫
        (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor h✝.toFunctor)).inv

Tactic:
exact congr($(mapWhiskerRight_whiskerLeft D _ _).toCatHom₂)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback b.fst b.snd 0 0

Tactic:
by
  convert! IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal
    <;> subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case mpr
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'
⊢ (∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x') → coendRel F ⟨j, x⟩ ⟨j', x'⟩

Tactic:
rintro ⟨f, y, rfl, rfl⟩

Goal state after:
case mpr
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
y : (F.obj (op j')).obj j
⊢ coendRel F ⟨j, (hom ((F.map f.op).app j)) y⟩ ⟨j', (hom ((F.obj (op j')).map f)) y⟩
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: case refine_2
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
⊢ ∃ a, (fun g ↦ f ≫ g) a = g

Tactic:
let d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData :=
        .ofExists (fun j hj ↦ (hf.map_mem j hj _ hZ).2) (fun j hj s ↦ by
          let c : Cocone ((Set.principalSegIio j).monotone.functor ⋙ hf.F) :=
            { pt := Z
              ι.app k := s.1 (op k)
              ι.naturality _ _ g := by
                dsimp
                simpa only [Category.comp_id] using! s.2 g.op }
          exact ⟨(hf.F.isColimitOfIsWellOrderContinuous j hj).desc c, fun k hk ↦
            by simpa using! (hf.F.isColimitOfIsWellOrderContinuous j hj).fac c ⟨k, hk⟩⟩)

Goal state after:
case refine_2
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 ⋯ ⋯
⊢ ∃ a, (fun g ↦ f ≫ g) a = g
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
x y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f = g

Tactic:
by
  apply Hom.ext <;> assumption

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

Goal state before:
pp: case hᵣ
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝¹ x✝ : X
f : x✝¹ ⟶ x✝
⊢ (J.map f ≫ (mkIso (e₁.app x✝) (e₂.app x✝) ⋯).hom).snd = ((mkIso (e₁.app x✝¹) (e₂.app x✝¹) ⋯).hom ≫ K.map f).snd

Tactic:
exact e₂.hom.naturality f

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

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝¹ x✝ : Type u
f : x✝¹ ⟶ x✝
x : (𝟭 (Type u)).obj x✝¹
⊢ (ConcreteCategory.hom ((𝟭 (Type u)).map f ≫ ↾pure)).toFun x =
    (ConcreteCategory.hom (↾pure ≫ __Functor✝.map f)).toFun x

Tactic:
exact (LawfulApplicative.map_pure f x).symm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : C
Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ (fromKleisli T).obj Z
⊢ ({ toFun := fun f ↦ f.of, invFun := fun f ↦ { of := f }, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g)).of =
    ((toKleisli T).map f ≫
        { toFun := fun f ↦ f.of, invFun := fun f ↦ { of := f }, left_inv := ⋯, right_inv := ⋯ }.symm g).of

Tactic:
simp [← T.η.naturality_assoc g]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
⊢ (∃ ψ, ψ ≫ φ = G ◁ φ ≫ conj G) → ∀ (X : C), (monoidHom φ X).range.Normal

Tactic:
intro ⟨ψ, hψ⟩

Goal state after:
case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
ψ : G ⊗ H ⟶ H
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
⊢ ∀ (X : C), (monoidHom φ X).range.Normal