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

Goal state before:
pp: case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.base =
    ({ base := f.base,
          fiber :=
            (α.app { as := op a.base }).toFunctor.map f.fiber ≫
              (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
        { base := g.base,
          fiber :=
            (α.app { as := op b.base }).toFunctor.map g.fiber ≫
              (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).base

pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.fiber =
    ({ base := f.base,
            fiber :=
              (α.app { as := op a.base }).toFunctor.map f.fiber ≫
                (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
          { base := g.base,
            fiber :=
              (α.app { as := op b.base }).toFunctor.map g.fiber ≫
                (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).fiber ≫
      eqToHom ⋯

Tactic:
·

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.base =
    ({ base := f.base,
          fiber :=
            (α.app { as := op a.base }).toFunctor.map f.fiber ≫
              (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
        { base := g.base,
          fiber :=
            (α.app { as := op b.base }).toFunctor.map g.fiber ≫
              (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).base
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.fiber =
    ({ base := f.base,
            fiber :=
              (α.app { as := op a.base }).toFunctor.map f.fiber ≫
                (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
          { base := g.base,
            fiber :=
              (α.app { as := op b.base }).toFunctor.map g.fiber ≫
                (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).fiber ≫
      eqToHom ⋯

Tactic:
·

Goal state after:
case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.fiber =
    ({ base := f.base,
            fiber :=
              (α.app { as := op a.base }).toFunctor.map f.fiber ≫
                (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
          { base := g.base,
            fiber :=
              (α.app { as := op b.base }).toFunctor.map g.fiber ≫
                (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).fiber ≫
      eqToHom ⋯
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 : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
⊢ ((LeftExtension.mk u adj.unit).whisker h).unit ≫
      f ◁ (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) =
    𝟙 (𝟙 a ≫ h) ⊗≫ (adj.unit ▷ (𝟙 a ≫ h) ≫ (f ≫ u) ◁ s.unit) ⊗≫ f ◁ adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension)

Tactic:
dsimp only [whisker_extension, StructuredArrow.mk_right, whisker_unit,
            StructuredArrow.mk_hom_eq_self]
          bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
tfae_1_to_2 : IsLeftAdjoint f → HasAbsLeftKanExtension f (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanExtension f (𝟙 a) → ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f
tfae_3_to_1 : (∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f) → IsLeftAdjoint f
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE

Tactic:
tfae_finish

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanLift u (𝟙 a) → ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
tfae_3_to_1 : (∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u) → IsRightAdjoint u
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
tfae_finish

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 := ⋯
i : J
hi : i ∈ l
⊢ ∀ ⦃x y : J⦄, Zag x y → Zigzag y j₂ → Zigzag x j₂

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 := ⋯
i : J
hi : i ∈ l
⊢ Zigzag j₂ j₂

Tactic:
·

Goal state after:
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 := ⋯
i : J
hi : i ∈ l
⊢ ∀ ⦃x y : J⦄, Zag x y → Zigzag y j₂ → Zigzag x j₂
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 := ⋯
i : J
hi : i ∈ l
⊢ Zigzag j₂ j₂

Tactic:
·

Goal state after:
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 := ⋯
i : J
hi : i ∈ l
⊢ Zigzag j₂ j₂
Module: Mathlib.CategoryTheory.Category.PartialFun

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

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⟩ ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑⟨some b, hb⟩ = (partialFunToPointed.map f).toFun ↑⟨some a, ⋯⟩

Tactic:
·

Goal state after:
case none
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
hb : none ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1 ∈ f a, ⟨none, hb⟩ ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑⟨none, hb⟩ = (partialFunToPointed.map f).toFun ↑⟨some a, ⋯⟩
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⟩ ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑⟨some b, hb⟩ = (partialFunToPointed.map f).toFun ↑⟨some a, ⋯⟩

Tactic:
·

Goal state after:
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⟩ ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑⟨some b, hb⟩ = (partialFunToPointed.map f).toFun ↑⟨some a, ⋯⟩
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case none
X Y : Pointed
f : X ⟶ Y
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫ (Pointed.Iso.mk (Equiv.optionSubtypeNe Y.point) ⋯).hom).toFun
      none =
    ((Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯).hom ≫ (𝟭 Pointed).map f).toFun none

pp: case some
X Y : Pointed
f : X ⟶ Y
a : X.X
ha : a ≠ X.point
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫ (Pointed.Iso.mk (Equiv.optionSubtypeNe Y.point) ⋯).hom).toFun
      (some ⟨a, ha⟩) =
    ((Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯).hom ≫ (𝟭 Pointed).map f).toFun (some ⟨a, ha⟩)

Tactic:
·

Goal state after:
case none
X Y : Pointed
f : X ⟶ Y
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫ (Pointed.Iso.mk (Equiv.optionSubtypeNe Y.point) ⋯).hom).toFun
      none =
    ((Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯).hom ≫ (𝟭 Pointed).map f).toFun none
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

pp: case some
X : PartialFun
x : X
⊢ ↑(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)))
      (some x) =
    ↑(ConcreteCategory.hom (𝟙 (partialFunToPointed.obj X))) (some x)

Tactic:
·

Goal state after:
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
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case some
X : PartialFun
x : X
⊢ ↑(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)))
      (some x) =
    ↑(ConcreteCategory.hom (𝟙 (partialFunToPointed.obj X))) (some x)

Tactic:
·

Goal state after:
case some
X : PartialFun
x : X
⊢ ↑(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)))
      (some x) =
    ↑(ConcreteCategory.hom (𝟙 (partialFunToPointed.obj X))) (some x)
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ ∃ h,
    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 h

pp: case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ f.fix a'
⊢ ∃ h,
    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 h

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ ∃ h,
    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 h
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y

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

Goal state after:
case inl.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y
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:
·

Goal state after:
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 ⋯
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ f.fix a'
⊢ ∃ h,
    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 h

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ f.fix a'
⊢ ∃ h,
    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 h
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  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' h₃
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y

pp: case inr.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  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' h₃
⊢ 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:
·

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  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' h₃
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  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' h₃
⊢ 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:
·

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  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' h₃
⊢ 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 ⋯
Module: Mathlib.Data.PFun

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a' → b ∈ f.fix a
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 : Sum.inl b' ∈ f a'
⊢ 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 : Sum.inr a'' ∈ f 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 : Sum.inl b' ∈ f a'
⊢ C a'
Module: Mathlib.Data.PFun

Goal state before:
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 : Sum.inr a'' ∈ f a'
⊢ C a'

Tactic:
·

Goal state after:
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 : Sum.inr a'' ∈ f a'
⊢ C a'
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case mp
X Y : RelCat
r : X ⟶ Y
⊢ IsIso r → ∃ f, graphFunctor.map f.hom = r

pp: case mpr
X Y : RelCat
r : X ⟶ Y
⊢ (∃ f, graphFunctor.map f.hom = r) → IsIso r

Tactic:
·

Goal state after:
case mp
X Y : RelCat
r : X ⟶ Y
⊢ IsIso r → ∃ f, graphFunctor.map f.hom = r
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case h.left
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾f ≫ ↾g = 𝟙 X

pp: case h.right
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾g ≫ ↾f = 𝟙 Y

Tactic:
·

Goal state after:
case h.left
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾f ≫ ↾g = 𝟙 X
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case h.right
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾g ≫ ↾f = 𝟙 Y

Tactic:
·

Goal state after:
case h.right
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾g ≫ ↾f = 𝟙 Y