mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left) (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) ≫
      pushout.desc
          (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
            pushout.desc
              (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                  X₃.right ≫
                pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              ⋯)
          ((α_ X₁.left X₂.right X₃.right).inv ≫
            pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                X₃.right ≫
              pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
          ⋯ ≫
        pushout.desc
          ((α_ X₁.right X₂.right X₃.left).hom ≫
            X₁.right ◁
                pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
              pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
          (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
            pushout.desc
              (X₁.right ◁
                  pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                    (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              ⋯)
          ⋯ =
    pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
        (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) ≫
      𝟙 (X₁ □ X₂ □ X₃).left

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CodiscreteCategory

Goal state before:
pp: α : Type u
⊢ Function.LeftInverse Codiscrete.mk Codiscrete.as

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CodiscreteCategory

Goal state before:
pp: α : Type u
⊢ Function.RightInverse Codiscrete.mk Codiscrete.as

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CodiscreteCategory

Goal state before:
pp: A : Type u_1
x✝ : (Codiscrete A)ᵒᵖ
⊢ (𝟭 (Codiscrete A)ᵒᵖ).obj x✝ ≅ ((functor fun x ↦ (unop x).as) ⋙ (functor fun x ↦ (unop x).as).rightOp).obj x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x : WalkingIso
⊢ C

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x y : WalkingIso
x✝ : x ⟶ y
⊢ WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x : WalkingIso
⊢ WalkingIso.rec (motive := fun {x_1} ↦ (x_1 ⟶ x) → (WalkingIso.rec X Y x_1 ⟶ WalkingIso.rec X Y x))
      (fun x_1 ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) x x_1)
      (fun x_1 ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) x x_1)
      x (𝟙 x) =
    𝟙 (WalkingIso.rec X Y x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
⊢ min hl.δ ⋯ = l

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
t : Fin (d + 1)
ht : IsIndex hl.δ ⋯ t
h : t = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
t : Fin d
ht : IsIndex hl.δ ⋯ t.succ
⊢ l = t.succ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
⊢ IsType₂ hl.δ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : i < l.castSucc
⊢ l ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.succ.succ
hi : i < l.succ.castSucc
⊢ i < l.succ.succ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left) (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
      {
            hom :=
              pushout.desc
                ((α_ X₁.right X₂.right X₃.left).hom ≫
                  X₁.right ◁
                      pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left)
                        (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                    pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                      (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
                  pushout.desc
                    (X₁.right ◁
                        pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                          (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                      pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                        (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                    (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                      (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                    ⋯)
                ⋯,
            inv :=
              pushout.desc
                (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
                  pushout.desc
                    (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                      (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                    (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left)
                          (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                        X₃.right ≫
                      pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                        (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                    ⋯)
                ((α_ X₁.left X₂.right X₃.right).inv ≫
                  pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left)
                        (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                      X₃.right ≫
                    pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                      (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                ⋯,
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        (X₁ □ X₂ □ X₃).hom =
    pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
        (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
      ((X₁ □ X₂) □ X₃).hom ≫ (α_ X₁.right X₂.right X₃.right).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x y z : WalkingIso
x✝¹ : x ⟶ y
x✝ : y ⟶ z
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) z x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) z x)
      x (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ y) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y y))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) y x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) y x)
        x x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) z x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) z x)
        y x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
⊢ ∀ (X : WalkingIso), ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).obj X = F.obj X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
⊢ ∀ (X Y : WalkingIso) (f : X ⟶ Y),
    ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f =
      eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi✝ : l.castSucc < i
hi : l.succ < i
⊢ l ≠ Fin.last u.dim

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.castSucc.succ
hi✝ : l.castSucc.castSucc < i
hi : l.castSucc.succ < i
⊢ l.castSucc.castSucc < i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.castSucc.succ
hi✝ : l.castSucc.castSucc < i
hi : l.castSucc.succ < i
⊢ l.succ.castSucc < i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
i : Fin (d + 2)
hu' :
  { dim := u.dim, simplex := u.simplex } =
    { dim := d, simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex }
⊢ i = l.castSucc ∨ i = l.succ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
ht : IsType₂ t
s : Type₁ k n
hst : s.δ = t
d : ℕ
hd : t.dim = d
⊢ ht.type₁ hd = s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hd' : y.dim = d' + 1
l' : Fin (d' + 1)
hl' : IsIndex y hd' l'.succ
h : hl.δ = hl'.δ
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h : { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } = { dim := t.d + 1, simplex := (t.x.cast ⋯).simplex }
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h :
  { dim := s.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex } =
    { dim := t.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.index.castSucc)) (t.x.cast ⋯).simplex }
⊢ s.δ = t.δ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h : s.δ = t.δ
u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hs : s.δ = u
⊢ IsType₂ u

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ ((X₁ □ X₂) □ X₃) ≅ X₁ □ X₂ □ X₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
pt : C₃
inl : (F.obj Y₁).obj X₂ ⟶ pt
inr : (F.obj X₁).obj Y₂ ⟶ pt
isPushout : IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl inr
⊢ (F.map f₁).app X₂ ≫ (F.obj Y₁).map f₂ = (F.obj X₁).map f₂ ≫ (F.map f₁).app Y₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h :
  { dim := s.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex } =
    { dim := t.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.index.castSucc)) (t.x.cast ⋯).simplex }
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : MonoidalCategory C
X₁✝ X₂✝ X₃ : Arrow C
W : C
inst✝ : BraidedCategory C
X₁ X₂ : Arrow C
⊢ (pushoutSymmetry (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≪≫
          HasColimit.isoOfNatIso (spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).hom ≫
      (X₂ □ X₁).hom =
    (X₁ □ X₂).hom ≫ (β_ X₁.right X₂.right).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
inst✝ : HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
⊢ (F.map f₁).app X₂ ≫ (F.obj Y₁).map f₂ = (F.obj X₁).map f₂ ≫ (F.map f₁).app Y₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ (F.map f₁).app X₂ ≫ ((e.app Y₁).app X₂).hom = ((e.app X₁).app X₂).hom ≫ (F'.map f₁).app X₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
hst :
  { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } =
    { dim := t.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.index.castSucc)) (t.x.cast ⋯).simplex }
⊢ s.x = ⋯.δ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : MonoidalClosed C
X : Arrow C
I : C
i : IsInitial I
W : C
this✝ : IsIso (X.hom ▷ I)
this : IsPushout (X.hom ▷ I) (X.left ◁ i.to W) ((i.ofIso (zeroMul i).symm).to (X.left ⊗ W)) (𝟙 (X.left ⊗ W))
⊢ pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (i.to W)).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (i.to W)).hom) ≫
      this.isoPushout.symm.hom ≫ X.hom ▷ W =
    pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (i.to W)).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (i.to W)).hom) ≫
      (ofHasPushout (curriedTensor C) X.hom (Arrow.mk (i.to W)).hom).ι ≫
        (Iso.refl (((curriedTensor C).obj X.right).obj (Arrow.mk (i.to W)).right)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ (F.obj X₁).map f₂ ≫ ((e.app X₁).app Y₂).hom = ((e.app X₁).app X₂).hom ≫ (F'.obj X₁).map f₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
hst :
  { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } =
    { dim := t.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.index.castSucc)) (t.x.cast ⋯).simplex }
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ sq.inl ≫ (Iso.refl sq.pt).hom = ((e.app Y₁).app X₂).hom ≫ (e.inv.app Y₁).app X₂ ≫ sq.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ sq.inr ≫ (Iso.refl sq.pt).hom = ((e.app X₁).app Y₂).hom ≫ (e.inv.app X₁).app Y₂ ≫ sq.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X : Arrow C
I : C
i : IsInitial I
W : C
this✝ : IsIso (I ◁ X.hom)
this : IsPushout (i.to W ▷ X.left) (I ◁ X.hom) (𝟙 (W ⊗ X.left)) ((i.ofIso (mulZero i).symm).to (W ⊗ X.left))
⊢ pushout.inl (((curriedTensor C).map (Arrow.mk (i.to W)).hom).app X.left)
        (((curriedTensor C).obj (Arrow.mk (i.to W)).left).map X.hom) ≫
      this.isoPushout.symm.hom ≫ W ◁ X.hom =
    pushout.inl (((curriedTensor C).map (Arrow.mk (i.to W)).hom).app X.left)
        (((curriedTensor C).obj (Arrow.mk (i.to W)).left).map X.hom) ≫
      (ofHasPushout (curriedTensor C) (Arrow.mk (i.to W)).hom X.hom).ι ≫
        (Iso.refl (((curriedTensor C).obj (Arrow.mk (i.to W)).right).obj X.right)).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
⊢ (chainComplexFunctor C).Additive

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : MonoidalClosed C
X : Arrow C
I : C
i : IsInitial I
T : C
t : IsTerminal T
⊢ (X.left ◁ᵢ t.uniqueUpToIso SemiCartesianMonoidalCategory.isTerminalTensorUnit ≪≫ ρ_ X.left).hom ≫ X.hom =
    X.hom ▷ T ≫ (X.right ◁ᵢ t.uniqueUpToIso SemiCartesianMonoidalCategory.isTerminalTensorUnit ≪≫ ρ_ X.right).hom

Tactic:
by

Goal state after: