mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: case snd
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.snd = (G.symm.trans F.symm).snd

Tactic:
exact ContinuousMap.Homotopy.symm_trans _ _

Goal state after:
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ proj i (pi fun i ↦ Quotient.mk (a✝ i)) = Quotient.mk (a✝ i)

Tactic:
proj,

Goal state after:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i ↦ Quotient.mk (a✝ i)).map { toFun := fun p ↦ p i, continuous_toFun := ⋯ } = Quotient.mk (a✝ i)
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I × ↑I
⊢ 0 ≤ ↑(σ x.1)

Tactic:
unit_interval

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I × ↑I
⊢ 0 ≤ ↑x.1

Tactic:
unit_interval

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast ⋯

Tactic:
by
  rw [conj_eqToHom_iff_heq
    ((πₘ (TopCat.ofHom f)).map ⟦p⟧) ((πₘ (TopCat.ofHom g)).map ⟦q⟧)
    (FundamentalGroupoid.ext <| start_path hfg)
    (FundamentalGroupoid.ext <| end_path hfg)]
  exact heq_path_of_eq_image hfg

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
⊢ weakEquivalences C (HoCat.pResolutionObj X)

Tactic:
simpa using mem_weakEquivalences (HoCat.pResolutionObj X)

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : Y.Quasicategory
⊢ X.Quasicategory

Tactic:
rw [quasicategory_iff_innerFibration] at hY ⊢
  rw [Subsingleton.elim (terminal.from X) (p ≫ terminal.from Y), innerFibration_iff]
  refine innerFibrations.comp_mem _ _ InnerFibration.mem hY.mem

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ homEquiv (𝟙 a) = 𝟙 a.toBase

Tactic:
unfold homEquiv

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ ((eHomEquiv Cat).trans
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat) (a ⟶[Cat] a)).trans Cat.fromChosenTerminalEquiv))
      (𝟙 a) =
    𝟙 a.toBase
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ homEquiv (f ≫ g) = homEquiv f ≫ homEquiv g

Tactic:
unfold homEquiv

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ ((eHomEquiv Cat).trans
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat) (a ⟶[Cat] c)).trans Cat.fromChosenTerminalEquiv))
      (f ≫ g) =
    ((eHomEquiv Cat).trans
          ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat) (a ⟶[Cat] b)).trans
            Cat.fromChosenTerminalEquiv))
        f ≫
      ((eHomEquiv Cat).trans
          ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat) (b ⟶[Cat] c)).trans
            Cat.fromChosenTerminalEquiv))
        g
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ r.degHom (f ≫ g) ≤ r.degHom g

Tactic:
by
  have ⟨_, g₁, g₂, _, _, h_fac, h_deg⟩ := r.exists_fac g
  rw [h_deg, ← h_fac, ← Category.assoc]
  exact r.degHom_le (f ≫ g₁) g₂

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : r.degHom f = r.deg Y✝
X Y : C
p : X✝ ⟶ Y✝
hp : W₁ p
h : r.degHom f = r.deg Y✝
hi : W₂ (𝟙 Y✝)
fac : p ≫ 𝟙 Y✝ = f
⊢ W₁ f

Tactic:
obtain rfl : p = f := by simpa using fac

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ X Y : C
p : X✝ ⟶ Y✝
hp : W₁ p
hi : W₂ (𝟙 Y✝)
hf h : r.degHom p = r.deg Y✝
fac : p ≫ 𝟙 Y✝ = p
⊢ W₁ p
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.deg X = r.deg Y

Tactic:
have {X Y : C} (e : X ≅ Y) : r.deg X ≤ r.deg Y := by
    rw [← r.degHom_id X, ← e.hom_inv_id]
    apply r.degHom_le
  exact le_antisymm (this e) (this e.symm)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
hf : generators.multiplicativeClosure f
⊢ P f

Tactic:
induction hf with

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
hf : generators.multiplicativeClosure' f
⊢ P f

Tactic:
induction hf with

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case succ.comp_of
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain ⟨rfl, rfl⟩ | h' := eq_or_len_le_of_P_δ hf

Goal state after:
case succ.comp_of.inl
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

case succ.comp_of.inr
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
⊢ ∃ L m b, ∃ (h₁ : mk m = y) (h₂ : x = mk (m + b)) (h : L.length = b), IsAdmissible m L ∧ f = standardσ L ⋯

Tactic:
induction hf with

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
⊢ ∃ L m b, ∃ (h₁ : mk m = y) (h₂ : x = mk (m + b)) (h : L.length = b), IsAdmissible m L ∧ f = standardσ L ⋯

Tactic:
by
  induction hf with
  | id n =>
    use [], n.len, 0, rfl, rfl, rfl, IsAdmissible.nil _
    rfl
  | of f hf =>
    cases hf with | @σ m k =>
    use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
    simp [standardσ]
  | @comp_of _ j x' g g' hg hg' h_rec =>
    cases hg' with | @σ m k =>
    obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec
    obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'
    use simplicialInsert k.val L₁, m, b₁ + 1, rfl, by grind, by grind, by grind
    subst_vars
    have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm
    simp_all [Fin.ofNat_eq_cast, Fin.cast_val_eq_self, standardσ_comp_standardσ_assoc,
      standardσ_comp_standardσ]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m : ℕ
hL : IsAdmissible m []
k : ℕ
hk : k < [].length
⊢ simplicialEvalσ [] [][k] = simplicialEvalσ [] ([][k] + 1)

Tactic:
grind [→ IsAdmissible.singleton]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ :
  ∀ {m : ℕ},
    IsAdmissible m tail✝ →
      ∀ {k : ℕ} {hk : k < tail✝.length}, simplicialEvalσ tail✝ tail✝[k] = simplicialEvalσ tail✝ (tail✝[k] + 1)
m : ℕ
hL : IsAdmissible m (head✝ :: tail✝)
k : ℕ
hk : k < (head✝ :: tail✝).length
⊢ simplicialEvalσ (head✝ :: tail✝) (head✝ :: tail✝)[k] = simplicialEvalσ (head✝ :: tail✝) ((head✝ :: tail✝)[k] + 1)

Tactic:
grind [→ IsAdmissible.singleton]

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

Goal state before:
pp: case mp
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } →
    ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x

Tactic:
rintro ⟨_, ⟨f, ⟨_, h₁⟩, h₂⟩⟩

Goal state after:
case mp
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
left✝¹ : { dim := d + 1, simplex := y }.dim = { dim := d, simplex := x }.dim + 1
f : ⦋{ dim := d, simplex := x }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y }.dim⦌
h₂ :
  ∀ (y_1 : ⦋{ dim := d, simplex := x }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y }.dim⦌),
    (fun f ↦
          Mono f ∧
            (ConcreteCategory.hom (X.map f.op)) { dim := d + 1, simplex := y }.simplex =
              { dim := d, simplex := x }.simplex)
        y_1 →
      y_1 = f
left✝ : Mono f
h₁ : (ConcreteCategory.hom (X.map f.op)) { dim := d + 1, simplex := y }.simplex = { dim := d, simplex := x }.simplex
⊢ ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsRegular
hP : WellFounded P.AncestralRel
⊢ WellFounded (P.ofIso e hA).AncestralRel

Tactic:
wellFounded_iff_isEmpty_descending_chain

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n) }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

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

Tactic:
wellFounded_iff_isEmpty_descending_chain

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝¹ : PartialOrder α
inst✝ : WellFoundedLT α
f : P.RankFunction α
⊢ IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
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:
wellFounded_iff_isEmpty_descending_chain

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
⊢ IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
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
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ P.p s = P.p t

Tactic:
Subtype.ext_iff,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ ↑(P.p s) = ↑(P.p t)
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 := ((↑s).cast ⋯).simplex } = { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ s = t

Tactic:
Subtype.ext_iff,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h : { dim := (↑s).dim, simplex := ((↑s).cast ⋯).simplex } = { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ ↑s = ↑t
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
this : WellFounded h.AncestralRel
⊢ WellFounded h.pairing.AncestralRel

Tactic:
wellFounded_iff_isEmpty_descending_chain

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
this : IsEmpty { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
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 : WellFounded h.pairing.AncestralRel
⊢ WellFounded h.AncestralRel

Tactic:
wellFounded_iff_isEmpty_descending_chain

Goal state after:
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) }
⊢ IsEmpty { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
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 → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ t₁ = t₂

Tactic:
Subtype.ext_iff,

Goal state after:
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 → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ ↑t₁ = ↑t₂
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 → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ ↑t₁ = ↑t₂

Tactic:
Subtype.ext_iff,

Goal state after:
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 → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ ↑↑t₁ = ↑↑t₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

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

Tactic:
ext m ⟨x₁, x₂⟩

Goal state after:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ (x₁, x₂) ∈ (⨆ x₁, ⨆ x₂, (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)).obj m ↔
    (x₁, x₂) ∈ ⊤.obj m
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a.notMem.refine_2.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ (↑t).toN < (↑(P.p c.s)).toN

Tactic:
SSet.N.lt_iff

Goal state after:
case a.notMem.refine_2.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ (↑t).subcomplex < (↑(P.p c.s)).subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsFinitelyPresentable X

Tactic:
apply +allowSynthFailures isCardinalPresentable_of_isColimit' _
      (isCoequalizerEpiComp ((EffectiveEpi.getStruct p).isColimitCoforkOfIsPullback
        (IsPullback.of_hasPullback p p)) q) _

Goal state after:
case hK
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0

case inst
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ ∀ (k : WalkingParallelPair),
    IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj k) Cardinal.aleph0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
h✝ : P.IsRegular
⊢ anodyneExtensions f

Tactic:
rw [← Subfunctor.toRange_ι f]

Goal state after:
X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
h✝ : P.IsRegular
⊢ anodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
w✝ : P.IsRegular
h✝ : P.IsInner
⊢ innerAnodyneExtensions f

Tactic:
rw [← Subfunctor.toRange_ι f]

Goal state after:
X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
w✝ : P.IsRegular
h✝ : P.IsInner
⊢ innerAnodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op

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

Tactic:
wellFounded_iff_isEmpty_descending_chain

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (m + 2)
hi : i ≠ k.castSucc
this : x.simplex ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋x.dim⦌)
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.1

Tactic:
simp [Subcomplex.mem_unionProd_iff, mem_horn_iff_notMem_range] at this

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (m + 2)
hi : i ≠ k.castSucc
this :
  x.simplex.2 ∉ ∂Δ[n].obj (Opposite.op ⦋x.dim⦌) ∧
    ∀ (x_1 : Fin (m + 1 + 1)), ¬x_1 = k.castSucc → ∃ x_2, x.simplex.1 x_2 = x_1
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.1
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)
⊢ (tensorRight X₃.left).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      ((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left ≫
        (α_ 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) =
    (tensorRight X₃.left).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      ((curriedTensor C).obj (X₁ □ X₂).left).map 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))
            ⋯

Tactic:
simp [← whisker_exchange_assoc, Limits.pushout.associator_naturality_left_condition,
            ← comp_whiskerRight_assoc]

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularHomology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
X : TopCat
R : C
⊢ ((X.singularHomology₀Iso R).hom ≫ Sigma.desc fun x ↦ 𝟙 R) = X.singularHomology₀ε R

Tactic:
by
  dsimp only [singularHomology₀Iso, singularHomology₀ε, SSet.homology₀ε]
  cat_disch

Goal state after: