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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ n₀ ≤ n₀ + n

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h :
  { dim := (↑s).dim,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p t)).cast ⋯).simplex }
⊢ s = t

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝¹ : X.Nonsingular
x y : X.N
h : x ≤ y
g : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Mono g
⊢ monoOfLE h = g → (ConcreteCategory.hom (X.map g.op)) y.simplex = x.simplex

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝¹ : X.Nonsingular
x y : X.N
h : x ≤ y
g : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Mono g
h' : (ConcreteCategory.hom (X.map g.op)) y.simplex = x.simplex
⊢ (ConcreteCategory.hom (X.map (monoOfLE h).op)) y.simplex = x.simplex

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ (↑(g (n₀ + n + 1))).dim = (↑(g (n₀ + n))).dim

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x : X.N
⊢ monoOfLE ⋯ = 𝟙 ⦋x.dim⦌

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y z : X.N
h : x ≤ y
h' : y ≤ z
⊢ monoOfLE h ≫ monoOfLE h' = monoOfLE ⋯

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
⊢ WellFounded P.AncestralRel

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p t)).cast ⋯).simplex }
⊢ ↑(P.p s) = ↑t

Tactic:
by

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : ↑h.pairing.II
hxy : h.pairing.AncestralRel x y
⊢ f.rank (h.equivII.symm x) < f.rank (h.equivII.symm y)

Tactic:
by

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
g : h.pairing.RankFunction α
x✝ y✝ : h.ι
hxy : h.AncestralRel x✝ y✝
⊢ g.rank (h.equivII x✝) < g.rank (h.equivII y✝)

Tactic:
by

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
x✝ : h.RankFunction α
⊢ (fun g ↦ { rank := fun x ↦ g.rank (h.equivII x), lt := ⋯ })
      ((fun f ↦ { rank := fun s ↦ f.rank (h.equivII.symm s), lt := ⋯ }) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
x : A.N
⊢ ∃ s,
    x.toS = { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } ∨
      x.toS =
        { dim := (↑s).dim,
          simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex }

Tactic:
by

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
x✝ : h.pairing.RankFunction α
⊢ (fun f ↦ { rank := fun s ↦ f.rank (h.equivII.symm s), lt := ⋯ })
      ((fun g ↦ { rank := fun x ↦ g.rank (h.equivII x), lt := ⋯ }) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ x✝ : h.ι
hst : h.type₁ x✝¹ = h.type₁ x✝
⊢ { dim := h.dim x✝¹ + 1, simplex := h.simplex x✝¹ } = { dim := h.dim x✝ + 1, simplex := h.simplex x✝ }

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
hst : h.type₂ s = h.type₂ t
⊢ { dim := h.dim s, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index s))) (h.simplex s) } =
    { dim := h.dim t, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index t))) (h.simplex t) }

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
⊢ h.type₁ s ≠ h.type₂ t

Tactic:
by

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : ↑h.pairing.II
hxy : h.pairing.AncestralRel x y
⊢ (↑x).dim = (↑y).dim → f.rank (h.equivII.symm x) < f.rank (h.equivII.symm y)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s + 1, simplex := h.simplex s }
⊢ x = h.type₁ s

Tactic:
by

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
g : h.pairing.WeakRankFunction α
x✝ y✝ : h.ι
hxy : h.AncestralRel x✝ y✝
⊢ h.dim x✝ = h.dim y✝ → g.rank (h.equivII x✝) < g.rank (h.equivII y✝)

Tactic:
by

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
x✝ : h.WeakRankFunction α
⊢ (fun g ↦ { rank := fun x ↦ g.rank (h.equivII x), lt := ⋯ })
      ((fun f ↦ { rank := fun s ↦ f.rank (h.equivII.symm s), lt := ⋯ }) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index s))) (h.simplex s) }
⊢ x = h.type₂ s

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
⊢ ∃ s, x = h.type₁ s ∨ x = h.type₂ s

Tactic:
by

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
x✝ : h.pairing.WeakRankFunction α
⊢ (fun f ↦ { rank := fun s ↦ f.rank (h.equivII.symm s), lt := ⋯ })
      ((fun g ↦ { rank := fun x ↦ g.rank (h.equivII x), lt := ⋯ }) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.I ∩ h.II = ∅

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.I ∪ h.II = Set.univ

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : h.IsProper
f : h.RankFunction α
⊢ h.IsRegular

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : h.ι
⊢ h.pairing.p (h.equivII x) = h.equivI x

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : h.ι
⊢ h.pairing.p.symm (h.equivI x) = h.equivII x

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : h.ι
⊢ h.type₁ x = ↑(h.pairing.p (h.equivII x))

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
x : ↑h.pairing.II
⊢ (↑x).IsUniquelyCodimOneFace (↑(h.pairing.p x)).toS

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.pairing.IsProper ↔ h.IsProper

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : h.IsProper
f : h.WeakRankFunction α
⊢ h.IsRegular

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
⊢ ⋯.index ⋯ = h.index s

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
d : ℕ
hd : h.dim s = d
⊢ ↑(⋯.index hd) = ↑(h.index s)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
x : ↑h.pairing.II
⊢ ∀ {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ 0

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
x : ↑h.pairing.II
⊢ ∀ {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ Fin.last (d + 1)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
⊢ h.AncestralRel s t ↔ h.pairing.AncestralRel (h.equivII s) (h.equivII t)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
this : IsEmpty { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑h.pairing.II
hf : ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.AncestralRel ((fun n ↦ h.equivII.symm (f n)) (n + 1)) ((fun n ↦ h.equivII.symm (f n)) n)

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
p q : ℕ
h : p + 1 = q
k : Fin (p + 1)
⊢ Y _⦋p + 1⦌ = Y _⦋q⦌

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
t : T
⊢ ∃ u, ψ u = (↑↑t).toS

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
p : ℕ
⊢ hom H p (p + 1) = -∑ k, (-1) ^ ↑k • H.h k

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
⊢ WellFounded h.pairing.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
⊢ f.app (op ⦋0⦌) = hom H 0 1 ≫ ((alternatingFaceMapComplex C).obj Y).d 1 0 + g.app (op ⦋0⦌)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsRegular
⊢ h.IsProper

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ : h.pairing.IsRegular
this✝ : h.IsProper
this : IsEmpty { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
f : ℕ → h.ι
hf : ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.pairing.AncestralRel ((fun n ↦ h.equivII (f n)) (n + 1)) ((fun n ↦ h.equivII (f n)) n)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.pairing.IsRegular ↔ h.IsRegular

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
⊢ Finite { x // P.AncestralRel x y }

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
⊢ P.rank' hy = ⨆ x, P.rank' ⋯ + 1

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
x : ↑P.II
r : P.AncestralRel x y
⊢ P.rank' ⋯ < P.rank' hy

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ P.IsRegular ↔ Nonempty (P.RankFunction ℕ)

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
⊢ ⨆ j, Subcomplex.range (c.ι.app j) = ⊤

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
⊢ Subcomplex.range φ = ⨆ j, Subcomplex.range (c.ι.app j ≫ φ)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ P.IsRegular ↔ Nonempty (P.WeakRankFunction ℕ)

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
n : ℕ
h : ∀ (j : J), (F.obj j).HasDimensionLT n
⊢ c.pt.HasDimensionLT n

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
inst✝¹ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
inst✝ : Finite J
h : ∀ (j : J), (F.obj j).Finite
⊢ c.pt.Finite

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{?u.4, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
⊢ (⊥_ SSet).Finite

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ (X ⨿ Y).Finite

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{?u.4, u_1} J
inst✝³ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst✝² : Finite ι
X : ι → SSet
inst✝¹ : HasCoproduct X
inst✝ : ∀ (j : ι), (X j).Finite
⊢ HasColimitsOfShape (Discrete ι) (Type u)

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{?u.4, u_1} J
inst✝³ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst✝² : Finite ι
X : ι → SSet
inst✝¹ : HasCoproduct X
inst✝ : ∀ (j : ι), (X j).Finite
this : HasColimitsOfShape (Discrete ι) (Type u)
x✝ : Discrete ι
j : ι
⊢ ((Discrete.functor X).obj { as := j }).Finite

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{?u.4, u_1} J
inst✝³ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst✝² : Finite ι
X : ι → SSet
inst✝¹ : HasCoproduct X
inst✝ : ∀ (j : ι), (X j).Finite
⊢ (∐ X).Finite

Tactic:
by

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

Goal state before:
pp: ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
i : ι
⊢ Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := i } ≫ f) ≤ Subcomplex.range (Sigma.ι X i ≫ f)

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
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
⊢ α x = -β (x.2.succ, x.1.castSucc)

Tactic:
by

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

Goal state before:
pp: ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
i : ι
⊢ Subcomplex.range (Sigma.ι X i ≫ f) ≤ Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := i } ≫ f)

Tactic:
by

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

Goal state before:
pp: ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ Subcomplex.range f = ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)

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)
x✝¹ x✝ : Fin (n + 1) × Fin (n + 2)
⊢ γ₁ x✝¹ = γ₁ x✝ → x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ x₁ ∈ ⊤.obj m

Tactic:
by

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

Goal state before:
pp: X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : x₁ ∈ ⊤.obj m
⊢ x₂ ∈ ⊤.obj m

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 γ₁
x✝¹ x✝ : Fin (n + 1) × Fin (n + 2)
⊢ γ₂ x✝¹ = γ₂ x✝ → x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: X₁ X₂ : SSet
⊢ ⨆ x₁, ⨆ x₂, (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex) = ⊤

Tactic:
by

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

Goal state before:
pp: X₁ X₂ : SSet
p q : ℕ
x₁ : X₁ _⦋p⦌
x₂ : X₂ _⦋q⦌
⊢ (ofSimplex x₁).prod (ofSimplex x₂) = range (yonedaEquiv.symm x₁ ⊗ₘ yonedaEquiv.symm x₂)

Tactic:
by

Goal state after: