mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝¹ : P.IsRegular
inst✝ : P.IsInner
j : ℕ
hj : ¬IsMax j
⊢ SSet.innerAnodyneExtensions (P.rankFunction.relativeCellComplex.F.map (CategoryTheory.homOfLE ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X✝ Y✝ Z✝ : SSet
e : X✝ ⟶ Y✝
x✝ : isomorphisms SSet e
f : Y✝ ⟶ Z✝
hf : strongInnerAnodyneExtensions f
⊢ strongInnerAnodyneExtensions (e ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X✝ Y✝ Z✝ : SSet
e : Y✝ ⟶ Z✝
x✝ : isomorphisms SSet e
f : X✝ ⟶ Y✝
hf : strongInnerAnodyneExtensions f
⊢ strongInnerAnodyneExtensions (f ≫ e)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ strongInnerAnodyneExtensions ≤ innerAnodyneExtensions

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
⊢ Disjoint ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)
    (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ isCardinalPresentable C κ = P.colimitsCardinalClosure κ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasColimitsOfSize.{w, w, v, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ IsCardinalLocallyPresentable C κ ↔
    ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : IsCardinalLocallyPresentable C κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ IsCardinalLocallyPresentable C κ'

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
s₂ : (range (f.m j)).N
g₂ : ⦋d⦌ ⟶ ⦋s₂.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₂.simplex = x₂
⊢ (fun x ↦ { dim := x.dim, simplex := (ConcreteCategory.hom ((f.b j).app (op ⦋x.dim⦌))) x.simplex }) s₁ =
    (fun x ↦ { dim := x.dim, simplex := (ConcreteCategory.hom ((f.b j).app (op ⦋x.dim⦌))) x.simplex }) s₂

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
g₂ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₁.simplex = x₂
⊢ ↑((ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) x₁) = (ConcreteCategory.hom (X.map g₁.op)) ↑⟨(f.mapN s₁).simplex, ⋯⟩

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
g₂ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₁.simplex = x₂
⊢ ↑((ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) x₁) = (ConcreteCategory.hom (X.map g₂.op)) ↑⟨(f.mapN s₁).simplex, ⋯⟩

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsColimit
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.mapCocone (PushoutCocone.mk (homOfLE ⋯) (f.b j) ⋯))

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB (Set.range (⋯.functor ⋙ ⋯.functor).obj) ((Set.principalSegIio m).cocone ⋯.functor).pt

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) ⊤

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
⊢ ⇑N.opEquiv ⁻¹' P.I ∩ ⇑N.opEquiv ⁻¹' P.II = ∅

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
⊢ ⇑N.opEquiv ⁻¹' P.I ∪ ⇑N.opEquiv ⁻¹' P.II = Set.univ

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
⊢ ∀ (a : A.op.N), a ∈ ⇑N.opEquiv ⁻¹' P.II ↔ N.opEquiv.toEquiv a ∈ P.II

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
⊢ ∀ (a : A.N), a ∈ P.I ↔ N.opEquiv.symm.toEquiv a ∈ ⇑N.opEquiv ⁻¹' P.I

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : ↑P.II
⊢ N.opEquiv.symm ↑(P.p x) ∈ P.op.I

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x y : ↑P.II
⊢ ⟨N.opEquiv.symm ↑x, ⋯⟩ = ⟨N.opEquiv.symm ↑y, ⋯⟩ ↔ x = y

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x y : ↑P.II
⊢ ↑⟨N.opEquiv.symm ↑x, ⋯⟩ < ↑(P.op.p ⟨N.opEquiv.symm ↑y, ⋯⟩) ↔ ↑x < ↑(P.p y)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
⊢ WellFounded P.op.AncestralRel

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
h₄ :
  Disjoint ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)
    (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃)
⊢ ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁).card +
      (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
          {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃).card =
    Finset.univ.card

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ Q ◁ inl ≫ Q ◁ hP.desc h k w = Q ◁ h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ Q ◁ inr ≫ Q ◁ hP.desc h k w = Q ◁ k

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ inl ▷ Q ≫ hP.desc h k w ▷ Q = h ▷ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ inr ▷ Q ≫ hP.desc h k w ▷ Q = k ▷ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
Q : C
⊢ Q ◁ f ≫ Q ◁ inl = Q ◁ g ≫ Q ◁ inr

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
Q : C
⊢ f ▷ Q ≫ inl ▷ Q = g ▷ Q ≫ inr ▷ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ pushout.inl f g ≫ Q ◁ hP.isoPushout.inv = Q ◁ inl

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ pushout.inr f g ≫ Q ◁ hP.isoPushout.inv = Q ◁ inr

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ inl ≫ Q ◁ hP.isoPushout.hom = Q ◁ pushout.inl f g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ inr ≫ Q ◁ hP.isoPushout.hom = Q ◁ pushout.inr f g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ pushout.inl f g ▷ Q ≫ hP.isoPushout.inv ▷ Q = inl ▷ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ pushout.inr f g ▷ Q ≫ hP.isoPushout.inv ▷ Q = inr ▷ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ inl ▷ Q ≫ hP.isoPushout.hom ▷ Q = pushout.inl f g ▷ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ inr ▷ Q ≫ hP.isoPushout.hom ▷ Q = pushout.inr f g ▷ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
Q : C
⊢ Q ◁ f ≫ Q ◁ pushout.inl f g = Q ◁ g ≫ Q ◁ pushout.inr f g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
Q : C
⊢ f ▷ Q ≫ pushout.inl f g ▷ Q = g ▷ Q ≫ pushout.inr f g ▷ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ X
⊢ f ▷ Z ▷ W ≫ (α_ B Z W).hom ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g) =
    (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ A
⊢ Z ◁ W ◁ g ≫ (α_ Z W Y).inv ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g) =
    (α_ Z W X).inv ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Q ◁ pushout.inl f g ≫ Q ◁ (pushoutSymmetry f g).hom = Q ◁ pushout.inr g f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Q ◁ pushout.inr f g ≫ Q ◁ (pushoutSymmetry f g).hom = Q ◁ pushout.inl g f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ pushout.inl f g ▷ Q ≫ (pushoutSymmetry f g).hom ▷ Q = pushout.inr g f ▷ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ pushout.inr f g ▷ Q ≫ (pushoutSymmetry f g).hom ▷ Q = pushout.inl g f ▷ Q

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H✝ : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H✝.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H✝.h x.2 ≫ Y.δ x.1
h₂✝ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H✝.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H✝.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
h₄ :
  Disjoint ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)
    (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃)
H :
  ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)ᶜ =
    ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃
⊢ (0, 0) ∉ {(Fin.last (n + 2), Fin.last (n + 1))}

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
i : Fin (m + 2)
hi : i ≠ k.castSucc
⊢ i ∈ Set.range ⇑(x.cast hd).simplex.1

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
i : Fin (n + 1)
⊢ i ∈ Set.range ⇑(x.cast hd).simplex.2

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
l : Fin (d + 1)
⊢ l ∈ finset x hd ↔ (x.cast hd).simplex.1 l = k.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
⊢ k.succ ≠ k.castSucc

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
i : Fin ((x.cast hd).dim + 1)
hi : (x.cast hd).simplex.1 i = k.succ
⊢ i ∈ finset x hd

Tactic:
by

Goal state after: