mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.ι (J.fst b) ≫ I.fst b

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.ι (J.fst b) ≫ I.fst b
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.snd b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) =
    K.ι (J.snd b) ≫ I.snd b

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.snd b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) =
    K.ι (J.snd b) ≫ I.snd b
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ 𝟙 (T.obj X.A) = 𝟙 (T.obj X.A)

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

Tactic:
ext
    dsimp
    rw [← Functor.map_comp, X.counit, Functor.map_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.π.app (WalkingMulticospan.right b)

Tactic:
]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a

Tactic:
]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ (lift E ≫ K.π.app (WalkingMulticospan.left (J.fst b))) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b)

Tactic:
]

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ (lift E ≫ K.π.app (WalkingMulticospan.left (J.fst b))) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b)
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f = s.ι.f ≫ 𝟙 (T.obj X.A)

Tactic:
]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f = s.ι.f ≫ 𝟙 (T.obj X.A)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ g ≫ K.ι (J.fst b) ≫ I.fst b = g ≫ K.ι (J.fst b) ≫ I.fst b

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ 𝟙 a.pt ≫ a.ι ≫ I.sndPiMapOfIsLimit c hd ≫ d.proj a✝ = (a.ι ≫ c.proj (J.snd a✝)) ≫ I.snd a✝

Tactic:
]

Goal state after:
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ 𝟙 a.pt ≫ a.ι ≫ I.sndPiMapOfIsLimit c hd ≫ d.proj a✝ = (a.ι ≫ c.proj (J.snd a✝)) ≫ I.snd a✝
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case inl
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i k : Fin 2
hij : i ≤ i
hjk : i ≤ k
⊢ map f i k ⋯ = map f i k hjk

Tactic:
]

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

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
⊢ m.f = (m ≫ (beckCoalgebraFork X).ι).f ≫ T.ε.app X.A

Tactic:
]

Goal state after:
case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
⊢ m.f = (m ≫ (beckCoalgebraFork X).ι).f ≫ T.ε.app X.A
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingParallelPair), f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app j = (Multifork.toPiFork hc hd K₁).π.app j

Tactic:
rintro (_ | _)
        · apply Fan.IsLimit.hom_ext hc
          simp
        · apply Fan.IsLimit.hom_ext hd
          simp

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case inr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j : Fin 2
hij : i ≤ j
hjk : j ≤ j
⊢ map f i j ⋯ = map f i j hij

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
⊢ app ⟨i, ⋯⟩ = app ⟨i, ⋯⟩

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i j : ℕ
hj✝ : i + (k + 1) = j
hj : i + k + 1 = j
hj' : j ≤ n
⊢ F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'

Tactic:
]

Goal state after:
case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i j : ℕ
hj✝ : i + (k + 1) = j
hj : i + k + 1 = j
hj' : j ≤ n
⊢ F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    (Fan.mk X fun x ↦ (Iso.refl X).hom).proj (J.fst x✝) ≫ (ofParallelHoms J f g).fst x✝

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    (Fan.mk X fun x ↦ (Iso.refl X).hom).proj (J.fst x✝) ≫ (ofParallelHoms J f g).fst x✝
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
⊢ app ⟨i, ⋯⟩ ≫ G.map' i (i + k) ⋯ ⋯ ≫ G.map' (i + k) (i + k + 1) ⋯ hj' =
    app ⟨i, ⋯⟩ ≫ G.map' i (i + k) ⋯ ⋯ ≫ G.map' (i + k) (i + k + 1) ⋯ hj'

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    (Fan.mk X fun x ↦ (Iso.refl X).hom).proj (J.snd x✝) ≫ (ofParallelHoms J f g).snd x✝

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    (Fan.mk X fun x ↦ (Iso.refl X).hom).proj (J.snd x✝) ≫ (ofParallelHoms J f g).snd x✝
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ (app ⟨i + 1, ⋯⟩).hom = (app ⟨i, ⋯⟩).hom ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
⊢ F.map' i (i + 1) ⋯ hi = F.map' i (i + 1) ⋯ hi

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
f : F ⟶ G
⊢ (∀ (X : Fin (0 + 1)), IsIso (f.app X)) ↔ IsIso (f.app 0)

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
f : F ⟶ G
⊢ (∀ (X : Fin (0 + 1)), IsIso (f.app X)) ↔ IsIso (f.app 0)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) = I.fst a ≫ K.π (J.fst a)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) = I.fst a ≫ K.π (J.fst a)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.inv ≫ right.hom =
    left.inv ≫ left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5

Tactic:
right.inv_hom_id,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ 𝟙 (G.obj' 1 homMk₁._proof_5) =
    left.inv ≫ left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ 𝟙 (G.obj' 1 homMk₁._proof_5) = G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ 𝟙 (G.obj' 1 homMk₁._proof_5) = G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
f : F ⟶ G
⊢ (∀ (X : Fin (1 + 1)), IsIso (f.app X)) ↔ IsIso (f.app 0) ∧ IsIso (f.app 1)

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
f : F ⟶ G
⊢ (∀ (X : Fin (1 + 1)), IsIso (f.app X)) ↔ IsIso (f.app 0) ∧ IsIso (f.app 1)
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (R.map (h.counit.app (L.obj X))) ≫ h.counit.app (L.obj X)) =
    R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X))

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (R.map (h.counit.app (L.obj X))) ≫ h.counit.app (L.obj X)) =
    R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X))
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (h.unit.app X) ≫ h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (h.unit.app X) ≫ h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) = K.ι.app (WalkingMultispan.left a)

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (h.unit.app (R.obj X) ≫ R.map (L.map (h.unit.app (R.obj X)))) =
    L.map (h.unit.app (R.obj X)) ≫ L.map (h.unit.app (R.obj (L.obj (R.obj X))))

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (h.unit.app (R.obj X) ≫ R.map (L.map (h.unit.app (R.obj X)))) =
    L.map (h.unit.app (R.obj X)) ≫ L.map (h.unit.app (R.obj (L.obj (R.obj X))))
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) ≫ desc S =
    I.multispan.map (WalkingMultispan.Hom.fst a) ≫ S.ι.app (WalkingMultispan.right (J.fst a))

Tactic:
]

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) ≫ desc S =
    I.multispan.map (WalkingMultispan.Hom.fst a) ≫ S.ι.app (WalkingMultispan.right (J.fst a))
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (h.unit.app (R.obj X) ≫ R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (h.unit.app (R.obj X) ≫ R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport i).μ = 𝟙 (𝟭 C)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport i).μ = 𝟙 (𝟭 C)
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
⊢ (adj.toComonad.transport j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
⊢ (adj.toComonad.transport j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f 0 ⟨k, hk⟩ ⋯ = map F f 0 ⟨k, hk⟩ hjk

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ R.map (h.counit.app X✝) ≫ R.map f = R.map (h.counit.app X✝) ≫ R.map f

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X))) =
    L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ L.map (h.unit.app X✝ ≫ R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y✝)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ L.map (h.unit.app X✝ ≫ R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (𝟙 (G.obj B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (𝟙 (G.obj B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app ((reflector R ⋙ R).obj X.A) ≫ R.map ((reflector R).map X.a) =
    𝟙 ((reflector R ⋙ R).obj X.A)

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app ((reflector R ⋙ R).obj X.A) ≫ R.map ((reflector R).map X.a) =
    𝟙 ((reflector R ⋙ R).obj X.A)