mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          {
            app := fun j ↦
              Discrete.casesOn j fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
            naturality := ⋯ } }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ m = ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : ↑s.1
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) (x + y)) =
    (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x) + fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
r : R
x : ↑s.1
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) (r • x)) =
    (RingHom.id R) r • fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x

Tactic:
by

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

Goal state before:
pp: case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝)) ≫
      match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝))

Tactic:
simp only [WalkingMulticospan.Hom.id_eq_id,
            Functor.map_id, Functor.const_obj_map, Category.comp_id]

Goal state after:
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ 𝟙 P ≫ ι a✝ = ι a✝
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.pt
w :
  ∀ (j : Discrete J),
    m ≫ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.π.app j = s.π.app j
⊢ m = lift f s

Tactic:
by

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

Goal state before:
pp: case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.fst a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.left (J.fst a✝) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.fst a✝)

Tactic:
simp only [WalkingMulticospan.Hom.id_eq_id,
            Functor.map_id, Functor.const_obj_map, Category.comp_id]

Goal state after:
case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst a✝)
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A M B : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : AddCommGroup B
inst✝² : Module R B
inst✝¹ : AddCommGroup M
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective ⇑j
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ Mono (ShortComplex.moduleCatMkOfKerLERange (↟j) (↟g) ⋯).f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A M B : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : AddCommGroup B
inst✝² : Module R B
inst✝¹ : AddCommGroup M
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective ⇑g
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
⊢ Epi (ShortComplex.moduleCatMkOfKerLERange (↟j) (↟g) ⋯).g

Tactic:
by

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✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.snd a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.left (J.snd a✝) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.snd a✝)

Tactic:
simp only [WalkingMulticospan.Hom.id_eq_id,
            Functor.map_id, Functor.const_obj_map, Category.comp_id]

Goal state after:
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.snd a✝) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj P).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
    (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))

Tactic:
simp only [WalkingMulticospan.Hom.id_eq_id,
            Functor.map_id, Functor.const_obj_map, Category.comp_id]

Goal state after:
case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective ⇑j
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ Function.Injective ⇑(↑ULift.moduleEquiv.symm ∘ₗ j ∘ₗ ↑ULift.moduleEquiv)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective ⇑j
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ (↑ULift.moduleEquiv.symm ∘ₗ j ∘ₗ ↑ULift.moduleEquiv).range = (↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑ULift.moduleEquiv).ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective ⇑j
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ (↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑ULift.moduleEquiv) ∘ₗ ↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑ULift.moduleEquiv =
    LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective ⇑g
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
⊢ Function.Surjective ⇑(↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑ULift.moduleEquiv)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective ⇑g
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
⊢ (↑ULift.moduleEquiv.symm ∘ₗ j ∘ₗ ↑ULift.moduleEquiv).range = (↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑ULift.moduleEquiv).ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective ⇑g
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
⊢ (↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑ULift.moduleEquiv) ∘ₗ ↑ULift.moduleEquiv.symm ∘ₗ j ∘ₗ ↑ULift.moduleEquiv =
    LinearMap.id

Tactic:
by

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
⊢ IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)

Tactic:
by

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✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
⊢ ∀ ⦃X Y : WalkingMulticospan J⦄ (f : X ⟶ Y),
    (((Functor.const (WalkingMulticospan J)).obj P).map f ≫
        match Y with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
      (match X with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
        I.multicospan.map f

Tactic:
by

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.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b

Tactic:
by

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 t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
⊢ ∀ (j : WalkingMulticospan J), t.π.app j = e.hom ≫ s.π.app j

Tactic:
by

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
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
⊢ ∀ (s : Cone I.multicospan) (j : WalkingMulticospan J), lift s ≫ K.π.app j = s.π.app j

Tactic:
by

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
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
⊢ ∀ (s : Cone I.multicospan) (m : s.pt ⟶ K.pt), (∀ (j : WalkingMulticospan J), m ≫ K.π.app j = s.π.app j) → m = lift s

Tactic:
by

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
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
⊢ f = g

Tactic:
by

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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
⊢ Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd = Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd

Tactic:
by

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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K : Multifork I
⊢ Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd = Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd

Tactic:
by

Goal state after:
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
i : ℕ
hi : i ≤ n
⊢ i < n + 1

Tactic:
by

Goal state after:
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
i j : ℕ
hij : autoParam (i ≤ j) map'._auto_1
hjn : autoParam (j ≤ n) map'._auto_3
⊢ i < n + 1

Tactic:
by

Goal state after:
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
i j : ℕ
hij : autoParam (i ≤ j) map'._auto_1
hjn : autoParam (j ≤ n) map'._auto_3
⊢ j < n + 1

Tactic:
by

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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
⊢ ∀ ⦃X Y : WalkingMulticospan J⦄ (f : X ⟶ Y),
    (((Functor.const (WalkingMulticospan J)).obj a.pt).map f ≫
        match Y with
        | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
        | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
      (match X with
        | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
        | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
        I.multicospan.map f

Tactic:
by

Goal state after:
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
i j : ℕ
hij : i ≤ j
hjn : j ≤ n
⊢ ⟨i, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
by

Goal state after:
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
X₀ X₁ : C
f : X₀ ⟶ X₁
i : Fin 2
⊢ i ≤ i

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingMulticospan J), f.hom ≫ (Multifork.ofPiFork K₂).π.app j = (Multifork.ofPiFork K₁).π.app j

Tactic:
by

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
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
⊢ { l //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }

Tactic:
by

Goal state after:
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, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : ⟨i, hi⟩ ⟶ ⟨j, hj⟩
hij' : i ≤ j
k : ℕ
hk : i + k = j
⊢ j ≤ n

Tactic:
by

Goal state after:
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, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
⊢ ∀ ⦃X Y : Fin (n + 1)⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f

Tactic:
by

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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K : Multifork I
⊢ ∀ (j : WalkingMulticospan J),
    ((𝟭 (Multifork I)).obj K).π.app j =
      (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫ ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app j

Tactic:
by

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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
⊢ ∀ (i : J.L),
    ((Iso.refl ((I.ofPiForkFunctor hd ⋙ I.toPiForkFunctor hc hd).obj K).pt).hom ≫
          ((𝟭 (Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd))).obj K).ι) ≫
        c.proj i =
      ((I.ofPiForkFunctor hd ⋙ I.toPiForkFunctor hc hd).obj K).ι ≫ c.proj i

Tactic:
by

Goal state after:
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, ⋯⟩ = 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
⊢ i + k < n

Tactic:
by

Goal state after:
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, ⋯⟩ = 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
⊢ i + k ≤ n

Tactic:
by

Goal state after:
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, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
⊢ ∀ ⦃X Y : Fin (n + 1)⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f

Tactic:
by

Goal state after:
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
⊢ G.map' i (i + 1) ⋯ hi ≫ (app ⟨i + 1, ⋯⟩).inv = (app ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 0
f : F.obj' 0 homMk₀._proof_1 ⟶ G.obj' 0 homMk₀._proof_1
i : ℕ
hi : i < 0
⊢ (F.map' i (i + 1) ⋯ hi ≫
      match ⟨i + 1, ⋯⟩ with
      | ⟨0, isLt⟩ => f) =
    (match ⟨i, ⋯⟩ with
      | ⟨0, isLt⟩ => f) ≫
      G.map' i (i + 1) ⋯ hi

Tactic:
by

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 ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
⊢ φ = φ'

Tactic:
by

Goal state after: