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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
t : Fin (1 + 1)
⊢ (α.hom ≫ (mkOfSucc 1).op).unop = α₀.hom.unop

Tactic:
ext x

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x✝) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
β₀ : α ⟶ α₀ := ⋯
β₁ : α ⟶ α₁ := ⋯
β₂ : α ⟶ α₂ := ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x✝) = (ConcreteCategory.hom (s.π.app α₀)) x✝
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x✝) = (ConcreteCategory.hom (s.π.app α₂)) x✝
t : Fin (1 + 1)
x : Fin ((unop (op ⦋1⦌)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (mkOfSucc 1).op).unop) x) = ↑((Hom.toOrderHom α₀.hom.unop) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
⊢ W = ⊤

Tactic:
ext ⟨a, ha⟩ ⟨b, hb⟩ f

Goal state after:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : SimplexCategory
ha : a.len ≤ d
b : SimplexCategory
hb : b.len ≤ d
f : { obj := a, property := ha } ⟶ { obj := b, property := hb }
⊢ W f ↔ ⊤ f
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
by_cases hk' : k ≤ j.castSucc

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
hk' : k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
hk' : ¬k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
j : StructuredArrow (op ⦋n⦌) (inclusion 2).op
⊢ (↾fun x ↦ lift sx s x) ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j

Tactic:
ext x

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
j : StructuredArrow (op ⦋n⦌) (inclusion 2).op
x : s.pt
⊢ (ConcreteCategory.hom ((↾fun x ↦ lift sx s x) ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j)).toFun x =
    (ConcreteCategory.hom (s.π.app j)).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
⊢ m = ↾fun x ↦ lift sx s x

Tactic:
ext x

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
⊢ (ConcreteCategory.hom m).toFun x = (ConcreteCategory.hom (↾fun x ↦ lift sx s x)).toFun x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (x.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j)))

Tactic:
rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₁
      simpa [← inl'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₁ j

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : ¬s.subcomplex ≤ A
⊢ s.simplex ∉ A.obj (Opposite.op ⦋s.dim⦌)

Tactic:
simpa using hs

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
x✝¹ x✝ : A.N
⊢ x✝¹.toN = x✝.toN → x✝¹ = x✝

Tactic:
by simp [ext_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inr (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ inr (WithInitial.of y₁) (WithInitial.of y₂)

Tactic:
by
    change inr' _ _ ≫ tensorHomOf _ _ = WithInitial.down f₂ ≫ inr' _ _
    ext i : 3
    dsimp [tensorHomOf]
    have e₁ := inr'_eval x₁ x₂ i
    have e₂ := inr'_eval y₁ y₂ <| (WithInitial.down f₂).toOrderHom i
    simp only [SimplexCategory.len_mk] at e₁ e₂
    rw [e₁, e₂]
    simp only [SimplexCategory.eqToHom_toOrderHom, SimplexCategory.len_mk,
      Nat.succ_eq_add_one, OrderEmbedding.toOrderHom_coe,
      OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply,
      Fin.cast_cast, Fin.cast_eq_self, Fin.cast_inj]
    conv_lhs =>
      change Fin.addCases
        (fun i ↦ Fin.castAdd (y₂.len + 1) (f₁.toOrderHom i))
        (fun i ↦ Fin.natAdd (y₁.len + 1) (f₂.toOrderHom i))
        (Fin.natAdd (x₁.len + 1) i)
      rw [Fin.addCases_right]
    rfl

Goal state after:
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.IsProper
inst✝ : P.IsInner
⊢ ∀ (x : ↑(P.ofIso e hA).II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ Fin.last (d + 1)

Tactic:
rintro ⟨b, hb⟩ d hd
    obtain ⟨a, rfl⟩ := (N.orderIsoOfIso e hA).symm.surjective b
    simp only [ofIso_II, Set.mem_preimage, OrderIso.apply_symm_apply] at hb
    simpa only [P.ofIso_index e hA ⟨a, hb⟩ hd] using IsInner.ne_last ⟨a, hb⟩ hd

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

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
⊢ a < b ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2

Tactic:
Prod.lt_iff

Goal state after:
p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
⊢ a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2 ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
hn : p + q + 1 ≤ n
⊢ (Δ[p] ⊗ Δ[q]).degenerate n = ⊤

Tactic:
ext x

Goal state after:
p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ x ∈ (Δ[p] ⊗ Δ[q]).degenerate n ↔ x ∈ ⊤
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
    rw [(P.isUniquelyCodimOneFace t).δ_index rfl] at h
    rwa [← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq,
      N.ext_iff, SSet.N.ext_iff]

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

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

Tactic:
· refine ⟨s, Or.inl ?_⟩
      nth_rw 1 [← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq]
      rfl

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:
Subcomplex.N.ext_iff,

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ x✝ : h.ι
hst : (h.type₁ x✝¹).toN = (h.type₁ x✝).toN
⊢ { dim := h.dim x✝¹ + 1, simplex := h.simplex x✝¹ } = { dim := h.dim x✝ + 1, simplex := h.simplex x✝ }
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:
Subcomplex.N.ext_iff,

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
hst : (h.type₂ s).toN = (h.type₂ t).toN
⊢ { 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) }
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:
let T := { x : P.II // P.AncestralRel x y }

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
⊢ Finite { x // P.AncestralRel x y }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: case refine_2
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
f : ⦋(↑↑t).dim⦌ ⟶ ⦋(↑(P.p y)).dim⦌
w✝ : CategoryTheory.Mono f
hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex = (↑↑t).simplex
⊢ ψ ⟨⟨(↑↑t).dim, ⋯⟩, f⟩ = (↑↑t).toS

Tactic:
SSet.S.ext_iff

Goal state after:
case refine_2
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
f : ⦋(↑↑t).dim⦌ ⟶ ⦋(↑(P.p y)).dim⦌
w✝ : CategoryTheory.Mono f
hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex = (↑↑t).simplex
⊢ (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex = (↑↑t).toN.1.simplex
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
  ext m ⟨x₁, x₂⟩
  simp only [Subfunctor.iSup_obj, Subcomplex.prod_obj, Set.mem_iUnion, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]
  have hx₁ : x₁ ∈ (⊤ : X₁.Subcomplex).obj _ := by simp
  have hx₂ : x₂ ∈ (⊤ : X₂.Subcomplex).obj _ := by simp
  simp only [← N.iSup_subcomplex_eq_top, Subfunctor.iSup_obj, Set.mem_iUnion] at hx₁ hx₂
  obtain ⟨s₁, hs₁⟩ := hx₁
  obtain ⟨s₂, hs₂⟩ := hx₂
  exact ⟨s₁, s₂, hs₁, hs₂⟩

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

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ⨆ i, f.filtration ↑i ≤ f.filtration m

pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ f.filtration m ≤ ⨆ i, f.filtration ↑i

Tactic:
· simp only [iSup_le_iff, Subtype.forall, Set.mem_Iio]
    intro j hj
    exact f.filtration_monotone hj.le

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ f.filtration m ≤ ⨆ i, f.filtration ↑i
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
j : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
y : f.Cell j
t : Δ[y.dim + 1] _⦋d⦌
h : x = y
⊢ Δ[x.dim + 1] _⦋d⦌ = Δ[y.dim + 1] _⦋d⦌

Tactic:
by rw [h]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ P.retractClosure ≤ isCardinalPresentable C κ

Tactic:
simpa only [ObjectProperty.retractClosure_le_iff] using h.le_isCardinalPresentable

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.smallCategoryOfSet.obj
f g : (𝟭 ↑h.smallCategoryOfSet.obj).obj x ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y
hfg :
  h.functor.mapArrow.obj { left := x, right := y, hom := f } =
    h.functor.mapArrow.obj { left := x, right := y, hom := g }
⊢ { left := x, right := y, hom := f } = { left := x, right := y, hom := g }

Tactic:
obtain rfl : f = g := by simpa [Arrow.mk_eq_mk_iff] using! hfg

Goal state after:
case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.smallCategoryOfSet.obj
f : (𝟭 ↑h.smallCategoryOfSet.obj).obj x ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y
hfg :
  h.functor.mapArrow.obj { left := x, right := y, hom := f } =
    h.functor.mapArrow.obj { left := x, right := y, hom := f }
⊢ { left := x, right := y, hom := f } = { left := x, right := y, hom := f }
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 simp [mapN, ← hg₁, dsimp% NatTrans.naturality_apply (f.b j)]

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h : s = t
⊢ s.x = t.x

Tactic:
by rw [h]

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 (d + 2)
hi : i < (min x hd).castSucc
⊢ (objEquiv (x.cast hd).simplex) ((min x hd).predAbove i) = (objEquiv (x.cast hd).simplex) (i.castPred ⋯)

Tactic:
Fin.predAbove_of_le_castSucc _ _ hi.le

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
hi : i < (min x hd).castSucc
⊢ (objEquiv (x.cast hd).simplex) (i.castPred ⋯) = (objEquiv (x.cast hd).simplex) (i.castPred ⋯)
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

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

pp: case one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ C

Tactic:
exacts [X, Y]

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (ht.type₁ ⋯).x = s.x

Tactic:
Subcomplex.N.ext_iff,

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (ht.type₁ ⋯).x.toN = s.x.toN
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.x = t.x

Tactic:
Subcomplex.N.ext_iff,

Goal state after:
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.x.toN = t.x.toN
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:
Subcomplex.N.ext_iff,

Goal state after:
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.δ.toN = t.δ.toN
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:
Subcomplex.N.ext_iff,

Goal state after:
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.toN = ⋯.δ.toN
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝³ : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (X.map x✝ ≫ ↾fun x ↦ isEmptyElim x) = (↾fun x ↦ isEmptyElim x) ≫ x✝³.map x✝

Tactic:
ext x

Goal state after:
X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝³ : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
x : X.obj x✝²
⊢ (ConcreteCategory.hom (X.map x✝ ≫ ↾fun x ↦ isEmptyElim x)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ isEmptyElim x) ≫ x✝³.map x✝)).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (X.chainComplex R).d 1 0 ≫ fromChainComplexXZero X R = 0

Tactic:
ext x

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
x : X _⦋1⦌
⊢ X.ιChainComplex x ≫ (X.chainComplex R).d 1 0 ≫ fromChainComplexXZero X R = X.ιChainComplex x ≫ 0