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

Goal state before:
pp: case mk.vcomp.h₁
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
θ_ih✝ : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
⊢ (fun p ↦ normalizeAux p f✝) = ?mk.vcomp.b

pp: case mk.vcomp.h₂
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
θ_ih✝ : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
⊢ ?mk.vcomp.b = fun p ↦ normalizeAux p h✝

pp: case mk.vcomp.b
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
θ_ih✝ : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
⊢ Path a a✝ → Path a b✝

Tactic:
<;>

Goal state after:
case mk.vcomp.h₁
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
θ_ih✝ : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
⊢ (fun p ↦ normalizeAux p f✝) = ?mk.vcomp.b

case mk.vcomp.h₂
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
θ_ih✝ : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
⊢ ?mk.vcomp.b = fun p ↦ normalizeAux p h✝

case mk.vcomp.b
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
θ_ih✝ : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
⊢ Path a a✝ → Path a b✝
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✝)

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:
<;>

Goal state after:
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✝)

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✝
⊢ ⋯ = ⋯
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case f
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✝
h : b✝ ⟶ c✝
a✝ : Hom₂ f✝ g✝
⊢ Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝ ▷ h) =
    𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
      Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝) ▷ liftHom F h ≫ 𝟙 (liftHom F g✝ ≫ liftHom F h)

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✝ g✝ : a✝¹ ⟶ b✝¹
η : f✝ ⟶ g✝
h : b✝¹ ⟶ c✝
a✝ b✝ : Hom₂ f✝ g✝
p✝ : Rel a✝ b✝
⊢ ⋯ = ⋯

Tactic:
<;>

Goal state after:
case f
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✝
h : b✝ ⟶ c✝
a✝ : Hom₂ f✝ g✝
⊢ Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝ ▷ h) =
    𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
      Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝) ▷ liftHom F h ≫ 𝟙 (liftHom F g✝ ≫ liftHom F h)

case h
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✝
a✝ b✝ : Hom₂ f✝ g✝
p✝ : Rel a✝ b✝
⊢ ⋯ = ⋯
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).base = f.base

pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
⊢ eqToHom ⋯ ≫ ((map (𝟙 F)).map f).fiber = f.fiber

Tactic:
<;>

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).base = f.base

case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
⊢ eqToHom ⋯ ≫ ((map (𝟙 F)).map f).fiber = f.fiber
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ F
f : X✝ ⟶ Y✝
⊢ ((map (α ≫ β)).map f).base = ((map β).map ((map α).map f)).base

pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ F
f : X✝ ⟶ Y✝
⊢ eqToHom ⋯ ≫ ((map (α ≫ β)).map f).fiber = ((map β).map ((map α).map f)).fiber

Tactic:
<;>

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ F
f : X✝ ⟶ Y✝
⊢ ((map (α ≫ β)).map f).base = ((map β).map ((map α).map f)).base

case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ F
f : X✝ ⟶ Y✝
⊢ eqToHom ⋯ ≫ ((map (α ≫ β)).map f).fiber = ((map β).map ((map α).map f)).fiber
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x y : ∫ᶜ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).base = f.base

pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x y : ∫ᶜ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).fiber = f.fiber ≫ eqToHom ⋯

Tactic:
<;>

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x y : ∫ᶜ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).base = f.base

case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x y : ∫ᶜ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).fiber = f.fiber ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ᶜ F
f : X✝ ⟶ Y✝
⊢ ((map (α ≫ β)).map f).base = ((map β).map ((map α).map f)).base

pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ᶜ F
f : X✝ ⟶ Y✝
⊢ ((map (α ≫ β)).map f).fiber = ((map β).map ((map α).map f)).fiber ≫ eqToHom ⋯

Tactic:
<;>

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ᶜ F
f : X✝ ⟶ Y✝
⊢ ((map (α ≫ β)).map f).base = ((map β).map ((map α).map f)).base

case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ᶜ F
f : X✝ ⟶ Y✝
⊢ ((map (α ≫ β)).map f).fiber = ((map β).map ((map α).map f)).fiber ≫ eqToHom ⋯
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 ⋯).hom =
    (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

Tactic:
by
  rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f).inv, Iso.inv_hom_id]
  simp [mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃ hf]

Goal state after:
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 ⋯ ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ =
    F.mapComp' f₀₁ f₁₃ f ⋯ ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv

Tactic:
by
  rw [F.mapComp'_comp_whiskerLeft_mapComp'_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]
  simp

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
⊢ liftFunctor J (functorToDiscrete X f) x = f x

Tactic:
by
    obtain ⟨x, h⟩ := Quotient.exists_rep x
    rw [← h]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j' : ConnectedComponents J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ ∃ a, (decomposedTo J).map a = f

Tactic:
have : j' = k' := by
      rw [← hX, ← hY, Quotient.eq'']
      exact Relation.ReflTransGen.single (Or.inl ⟨f⟩)

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j' : ConnectedComponents J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
this : j' = k'
⊢ ∃ a, (decomposedTo J).map a = f
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f

pp: case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), f ≫ 𝟙 Y = f

pp: case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {W X Y Z : KleisliCat m} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
<;>

Goal state after:
case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f

case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), f ≫ 𝟙 Y = f

case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {W X Y Z : KleisliCat m} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f✝ = f✝

pp: case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ f✝ ≫ 𝟙 Y✝ = f✝

pp: case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝

Tactic:
<;>

Goal state after:
case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f✝ = f✝

case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ f✝ ≫ 𝟙 Y✝ = f✝

case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (𝟙 X✝ ≫ f✝) x✝ = f✝ x✝

pp: case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (f✝ ≫ 𝟙 Y✝) x✝ = f✝ x✝

pp: case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
x✝ : W✝
⊢ ((f✝ ≫ g✝) ≫ h✝) x✝ = (f✝ ≫ g✝ ≫ h✝) x✝

Tactic:
<;>

Goal state after:
case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (𝟙 X✝ ≫ f✝) x✝ = f✝ x✝

case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (f✝ ≫ 𝟙 Y✝) x✝ = f✝ x✝

case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
x✝ : W✝
⊢ ((f✝ ≫ g✝) ≫ h✝) x✝ = (f✝ ≫ g✝ ≫ h✝) x✝
Module: Mathlib.Data.PFun

Goal state before:
pp: case mp.inl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inl b ∈ f a
⊢ b ∈ f.fix a'

pp: case mp.inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a✝ a' : α
ha' : Sum.inr a' ∈ f a✝
b : β
h : b ∈ f.fix a✝
a : α
h' : Sum.inr a ∈ f a✝
e' : b ∈ f.fix a
⊢ b ∈ f.fix a'

Tactic:
<;>

Goal state after:
case mp.inl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inl b ∈ f a
⊢ b ∈ f.fix a'

case mp.inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a✝ a' : α
ha' : Sum.inr a' ∈ f a✝
b : β
h : b ∈ f.fix a✝
a : α
h' : Sum.inr a ∈ f a✝
e' : b ∈ f.fix a
⊢ b ∈ f.fix a'
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ fixInduction h H = H a h fun x h' ↦ fixInduction ⋯ H

Tactic:
unfold fixInduction
  generalize_proofs
  induction ‹Acc _ _›
  rfl

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : (f a').get ⋯ = Sum.inl b'
⊢ C a'

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : (f a').get ⋯ = Sum.inr a''
⊢ C a'

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : (f a').get ⋯ = Sum.inl b'
⊢ C a'

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : (f a').get ⋯ = Sum.inr a''
⊢ C a'
Module: Mathlib.Data.PFun

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
h : x ∈ s
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t

pp: case neg
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
h : ¬x ∈ s
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
h : x ∈ s
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t

case neg
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
h : ¬x ∈ s
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Tactic:
trans ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2

α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2
Module: Mathlib.CategoryTheory.Category.TwoP

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

Tactic:
exact f.hom.map_fst.symm

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

Goal state before:
pp: case x.refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ (hom (limit.π (F ⋙ objects) j))
      ((hom
          (limit.lift (F ⋙ objects)
            { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
        X✝) =
    (s.π.app j).toFunctor.obj X✝

pp: case x.refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ (s.π.app j).toFunctor.obj Y✝ =
    (hom (limit.π (F ⋙ objects) j))
      ((hom
          (limit.lift (F ⋙ objects)
            { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
        Y✝)

Tactic:
<;>

Goal state after:
case x.refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ (hom (limit.π (F ⋙ objects) j))
      ((hom
          (limit.lift (F ⋙ objects)
            { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
        X✝) =
    (s.π.app j).toFunctor.obj X✝

case x.refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ (s.π.app j).toFunctor.obj Y✝ =
    (hom (limit.π (F ⋙ objects) j))
      ((hom
          (limit.lift (F ⋙ objects)
            { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
        Y✝)
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)).obj X.rel ≤
    (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F)).obj ((Subobject.pullback π(π₁, F.F)).obj X.rel)

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F)).obj
      ((Subobject.pullback (prod.map F.f (𝟙 Y.tgt))).obj Y.rel) ≤
    (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).obj ((Subobject.pullback π(π₁, G.F)).obj Y.rel)

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).obj ((Subobject.pullback (prod.map G.f (𝟙 Z.tgt))).obj Z.rel) ≤
    (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel

Tactic:
<;>

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)).obj X.rel ≤
    (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F)).obj ((Subobject.pullback π(π₁, F.F)).obj X.rel)

case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F)).obj
      ((Subobject.pullback (prod.map F.f (𝟙 Y.tgt))).obj Y.rel) ≤
    (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).obj ((Subobject.pullback π(π₁, G.F)).obj Y.rel)

case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).obj ((Subobject.pullback (prod.map G.f (𝟙 Z.tgt))).obj Z.rel) ≤
    (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: case e_a.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
<;>

Goal state after:
case e_a.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: case e_self.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
<;>

Goal state after:
case e_self.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)