mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X✝ : Type u
C✝ : Cat
C : Cat
X : Type u
G : C ⟶ typeToCat.obj X
⊢ (TypeCat.homEquiv.trans
          ((ConnectedComponents.typeToCatHomEquiv (↑C) X).trans (Functor.equivCatHom (↑C) (Discrete X)))).symm
      G =
    connectedComponents.map G ≫
      { app := fun X ↦ ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj X)) (𝟙 typeToCat.obj X).toFunctor,
            naturality := ⋯ }.app
        X

Tactic:
by

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)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u =
    𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)

Tactic:
by

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)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = t.unit ≫ f ◁ H.desc σs'

Tactic:
by

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)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ t.unit ≫ f ◁ H.desc σs' =
    t.unit ≫
      f ◁
        ((ρ_ t.extension).inv ≫
          (ρ_ t.extension).hom ≫
            H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))

Tactic:
by

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)) (τ : t.whisker h ⟶ s),
    τ =
      let k := s.extension;
      let θ := s.unit;
      let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
      let τ := H.desc sτ;
      let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
      let σ := H'.desc sσ;
      homMk σ ⋯

Tactic:
by

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

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ Category.{?u.8, u + 1} (KleisliCat m)

Tactic:
by

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

Goal state before:
pp: α β : PartialFun
e : α ≃ β
⊢ ↑(⇑e.symm ∘ ⇑e) = 𝟙 α

Tactic:
by

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

Goal state before:
pp: α β : PartialFun
e : α ≃ β
⊢ ↑(⇑e ∘ ⇑e.symm) = 𝟙 β

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : Type u_1
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : typeToPartialFun.map a₁✝ = typeToPartialFun.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by

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

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ ↑⟨c, hc⟩ = (f ≫ g).toFun ↑⟨a, ha⟩ →
    ∃ a_2 ∈ (PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val) ⟨a, ha⟩,
      ⟨c, hc⟩ ∈ (PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val) a_2

Tactic:
by

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

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ (∃ a_1 ∈ (PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val) ⟨a, ha⟩,
      ⟨c, hc⟩ ∈ (PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val) a_1) →
    ↑⟨c, hc⟩ = (f ≫ g).toFun ↑⟨a, ha⟩

Tactic:
by

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

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
⊢ PFun.toSubtype (fun x ↦ x ≠ Z.point) (f ≫ g).toFun ∘ Subtype.val =
    PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val ≫
      PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val

Tactic:
by

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

Goal state before:
pp: X : PartialFun
o : { X := Option X, point := none }.X
a : X
⊢ { toFun := Option.elim' none fun a ↦ (𝟙 X a).toOption, map_point := ⋯ }.toFun (some a) =
    (𝟙 { X := Option X, point := none }).toFun (some a)

Tactic:
dsimp [CategoryStruct.id]
        convert! Part.some_toOption a

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

Goal state before:
pp: X : PartialFun
o : { X := Option X, point := none }.X
a : X
⊢ { toFun := Option.elim' none fun a ↦ (𝟙 X a).toOption, map_point := ⋯ }.toFun (some a) =
    (𝟙 { X := Option X, point := none }).toFun (some a)

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ Z✝ : PartialFun
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
o : { X := Option X✝, point := none }.X
a : X✝
⊢ { toFun := Option.elim' none fun a ↦ ((f ≫ g) a).toOption, map_point := ⋯ }.toFun (some a) =
    ({ toFun := Option.elim' none fun a ↦ (f a).toOption, map_point := ⋯ } ≫
          { toFun := Option.elim' none fun a ↦ (g a).toOption, map_point := ⋯ }).toFun
      (some a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
x : α
⊢ x ∈ f.Dom ↔ ∃ y, y ∈ f x

Tactic:
by

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

Goal state before:
pp: ⊢ PartialFun ⥤ Pointed

Tactic:
by

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

Goal state before:
pp: X : PartialFun
a : (partialFunToPointed ⋙ pointedToPartialFun).obj X
⊢ (fun a ↦ ⟨some a, ⋯⟩) ((fun a ↦ Option.get ↑a ⋯) a) = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
x✝ : (p : α → Prop) × (Subtype p → β)
p : α → Prop
f : Subtype p → β
⊢ (fun f ↦ ⟨fun a ↦ (f a).Dom, f.asSubtype⟩) ((fun f x ↦ { Dom := f.fst x, get := fun h ↦ f.snd ⟨x, h⟩ }) ⟨p, f⟩) =
    ⟨p, f⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set α
h : s ⊆ f.Dom
a : α
b : β
⊢ b ∈ f.restrict h a ↔ a ∈ s ∧ b ∈ f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
b : β
⊢ b ∈ res f s a ↔ a ∈ s ∧ f a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
α✝ : Type u_7
f : α →. α✝
⊢ id <$> f = f

Tactic:
by

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
⊢ (f a).Dom

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝
⊢ b ∈
      ((𝟭 PartialFun).map f ≫
          (PartialFun.Iso.mk
              { toFun := fun a ↦ ⟨some a, ⋯⟩, invFun := fun a ↦ Option.get ↑a ⋯, left_inv := ⋯, right_inv := ⋯ }).hom)
        a ↔
    b ∈
      ((PartialFun.Iso.mk
              { toFun := fun a ↦ ⟨some a, ⋯⟩, invFun := fun a ↦ Option.get ↑a ⋯, left_inv := ⋯, right_inv := ⋯ }).hom ≫
          (partialFunToPointed ⋙ pointedToPartialFun).map f)
        a

Tactic:
by

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

Goal state before:
pp: X : Pointed
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X ≃ ((𝟭 Pointed).obj X).X

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : PartialFun
⊢ 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) =
    𝟙 (partialFunToPointed.obj X)

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : Type ?u.12
f : X✝ ⟶ Y✝
a✝ : ((typeToPartialFun ⋙ partialFunToPointed).obj X✝).X
a : typeToPartialFun.obj X✝
⊢ (typeToPartialFun.map f a).Dom

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : Type ?u.12
f : X✝ ⟶ Y✝
a✝ : ((typeToPartialFun ⋙ partialFunToPointed).obj X✝).X
a : typeToPartialFun.obj X✝
⊢ ((typeToPartialFun ⋙ partialFunToPointed).map f ≫
          { hom := { toFun := id, map_point := ⋯ }, inv := { toFun := id, map_point := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom).toFun
      (some a) =
    ({ hom := { toFun := id, map_point := ⋯ }, inv := { toFun := id, map_point := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom ≫
          typeToPointed.map f).toFun
      (some a)

Tactic:
by

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

Goal state after:
Module: Mathlib.Data.PFun

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ b ∈ f.fix a

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : 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
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ C a

Tactic:
by

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

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : 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₀
⊢ C a

Tactic:
by

Goal state after:
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
fa : Sum.inl b ∈ f 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₀
⊢ fixInduction' h hbase hind = hbase a fa

Tactic:
by

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

Goal state before:
pp: X Y : RelCat
f g : X ⟶ Y
h : f.rel = g.rel
⊢ f = g

Tactic:
by

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

Goal state before:
pp: X Y Z : RelCat
X✝ Y✝ : Type u_1
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : graphFunctor.map a₁✝ = graphFunctor.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f 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₀
⊢ fixInduction' h hbase hind = hind a a' h' fa (fixInduction' h' hbase hind)

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
⊢ f.preimage Set.univ = f.Dom

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (↑f).preimage s = f ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ s → f x ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (res f s).core t = sᶜ ∪ f ⁻¹' t

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (↑f).core s = f ⁻¹' s

Tactic:
by

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

Goal state before:
pp: 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
hif : IsIso (↾f)
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ (x, y) ∈ (graphFunctor.map (asIso (↾f)).hom).rel → (x, y) ∈ r.rel

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = f.preimage s ∪ f.Domᶜ

Tactic:
by

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

Goal state before:
pp: 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
hif : IsIso (↾f)
⊢ ∃ f, graphFunctor.map f.hom = r

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s

Tactic:
by

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

Goal state before:
pp: case mp
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, graphFunctor.map f.hom = r

Tactic:
suffices hif : IsIso (C := Type u) (↾f) by
      use asIso (↾f)
      ext ⟨x, y⟩
      exact ⟨by aesop, fun hxy ↦ (h2 (f x) y).1 ⟨x, (hf x).2, hxy⟩⟩

Goal state after:
case mp
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
⊢ IsIso (↾f)
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
⊢ b ∈ toSubtype p f a ↔ ↑b = f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ (PFun.id β).comp f x✝¹ ↔ x✝ ∈ f x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ f.comp (PFun.id α) x✝¹ ↔ x✝ ∈ f x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : γ →. δ
g : β →. γ
h : α →. β
x✝¹ : α
x✝ : δ
⊢ x✝ ∈ (f.comp g).comp h x✝¹ ↔ x✝ ∈ f.comp (g.comp h) x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝¹ : α
x✝ : γ
⊢ x✝ ∈ ↑(g ∘ f) x✝¹ ↔ x✝ ∈ (↑g).comp (↑f) x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y Z : RelCat
⊢ opFunctor.IsEquivalence

Tactic:
by

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

Goal state before:
pp: X Y Z : RelCat
⊢ unopFunctor.IsEquivalence

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : Pointed
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := { toFun := Option.map (f ≫ g).toFun, map_fst := ⋯, map_snd := ⋯ } } =
    { hom := { toFun := Option.map f.toFun, map_fst := ⋯, map_snd := ⋯ } } ≫
      { hom := { toFun := Option.map g.toFun, map_fst := ⋯, map_snd := ⋯ } }

Tactic:
by

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

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

Tactic:
by

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

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
⊢ (f.comp ↑Prod.fst).prodLift (g.comp ↑Prod.snd) = f.prodMap g

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ (PFun.id α).prodMap (PFun.id β) = PFun.id (α × β)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦
            { hom := { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToTwoPFst.map f ≫
      { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦
              {
                hom :=
                  { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ (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) =
    f

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (hom (limit.π (F ⋙ objects) X✝)) X ⟶ (hom (limit.π (F ⋙ objects) X✝)) Y
⊢ (hom (limit.π (F ⋙ objects) Y✝)) X ⟶ (hom (limit.π (F ⋙ objects) Y✝)) Y

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
⊢ (↾fun g ↦ eqToHom ⋯ ≫ (F.map (𝟙 X)).toFunctor.map g ≫ eqToHom ⋯) =
    𝟙 ((hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦
            { hom := { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToTwoPSnd.map f ≫
      { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦
              {
                hom :=
                  { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x✝¹ x✝ Z : J
f : x✝¹ ⟶ x✝
g : x✝ ⟶ Z
⊢ (↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map (f ≫ g)).toFunctor.map g_1 ≫ eqToHom ⋯) =
    (↾fun g ↦ eqToHom ⋯ ≫ (F.map f).toFunctor.map g ≫ eqToHom ⋯) ≫
      ↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map g).toFunctor.map g_1 ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j j' : J
f : j ⟶ j'
⊢ (hom ((homDiagram X X).map f)) (𝟙 ((hom (limit.π (F ⋙ objects) j)) X)) = 𝟙 ((hom (limit.π (F ⋙ objects) j')) X)

Tactic:
by

Goal state after: