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

Goal state before:
pp: case comminr
⊢ (stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₁₂ ≫ (Iso.refl Λ[2, 2].toSSet).hom

Tactic:
decide

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

Goal state before:
pp: X : SSet
n : ℕ
⊢ X.skeleton (n + 1) = X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
by
  apply le_antisymm
  · conv_lhs => dsimp [skeleton]
    simp only [iSup_le_iff]
    rintro ⟨d, hd⟩ x
    rw [Nat.lt_succ_iff] at hd
    obtain hd | rfl := hd.lt_or_eq
    · exact (X.ofSimplex_le_skeleton _ hd).trans le_sup_left
    · exact le_trans (le_trans (by rfl) (le_iSup _ x)) le_sup_right
  · simp only [sup_le_iff, iSup_le_iff]
    constructor
    · exact X.skeleton.monotone (by simp)
    · intro x
      apply X.ofSimplex_le_skeleton _ (by simp)

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

Goal state before:
pp: case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 1

Tactic:
decide

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

Goal state before:
pp: case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 2).inv =
    stdSimplex.δ 0

Tactic:
decide

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

Goal state before:
pp: case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 2

Tactic:
decide

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

Goal state before:
pp: case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 0

Tactic:
decide

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

Goal state before:
pp: case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 2).inv =
    stdSimplex.δ 2

Tactic:
decide

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

Goal state before:
pp: case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 2

Tactic:
decide

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

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁))) =
    ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)))
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)

Tactic:
replace h : Y.map f₁.op c₁.simplex = Y.map f₂.op c₂.simplex := by
        rwa [← c₁.b_app_ι_app_objEquiv_symm_val f₁, ← c₂.b_app_ι_app_objEquiv_symm_val f₂]

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₂.op)) c₂.simplex
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 2 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 0

Tactic:
decide

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

Goal state before:
pp: case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 2 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv =
    stdSimplex.δ 0

Tactic:
decide

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

Goal state before:
pp: case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 2

Tactic:
decide

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

Goal state before:
pp: case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 0

Tactic:
decide

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

Goal state before:
pp: case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv =
    stdSimplex.δ 2

Tactic:
decide

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

Goal state before:
pp: case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 1

Tactic:
decide

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

Goal state before:
pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i.succ).op)) x = ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i

Tactic:
symm

Goal state after:
case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i = (ConcreteCategory.hom (X.map (mkOfSucc i.succ).op)) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case zero
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
p : X.Path 0
⊢ { s // X.spine 0 s = p }

Tactic:
exact ⟨p.vertex 0, by aesop⟩

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 b c : CatEnrichedOrdinary C
f₁ f₂ f₃ : a ⟶ b
g₁ g₂ g₃ : b ⟶ c
η : f₁ ⟶ f₂
η' : f₂ ⟶ f₃
θ : g₁ ⟶ g₂
θ' : g₂ ⟶ g₃
⊢ hComp η θ ≫ hComp η' θ' = hComp (η ≫ η') (θ ≫ θ')

Tactic:
by
  simp [hComp, ← CatEnriched.hComp_comp, Hom.comp_eq]

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

Goal state before:
pp: V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ι0₂._proof_3 })
⊢ 0 ≤ 1

Tactic:
decide

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

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
f : x.as ⟶ y.as
x✝ : ⊤ ((quotientFunctor V).map f)
⊢ (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).multiplicativeClosure.strictMap (quotientFunctor V)
    ((quotientFunctor V).map f)

Tactic:
rw [Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk]

Goal state after:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as ⟶ y.as
x✝ : ⊤ ((quotientFunctor V).map f)
⊢ ⊤.strictMap (quotientFunctor V) ((quotientFunctor V).map f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case succ
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 ⋯
⊢ (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

Tactic:
let β₂ : α ⟶ α₂ := StructuredArrow.homMk ((Hom.tr (mkOfSucc 0)).op) (Quiver.Hom.unop_inj
        (by ext x; fin_cases x <;> rfl))

Goal state after:
case succ
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 ⋯
⊢ (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
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge (x₀, y₀) (x₁, y₁)
⊢ (functor X Y ⋙ inverse X Y).map (homMk e) ≫ (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk (x₁, y₁)))).hom =
    (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk (x₀, y₀)))).hom ≫ (𝟭 (X ⊗ Y).HomotopyCategory).map (homMk e)

Tactic:
obtain ⟨ex, ey, rfl⟩ := e.tensor_surjective

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
ex : Edge x₀ x₁
ey : Edge y₀ y₁
⊢ (functor X Y ⋙ inverse X Y).map (homMk (ex.tensor ey)) ≫
      (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk (x₁, y₁)))).hom =
    (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk (x₀, y₀)))).hom ≫
      (𝟭 (X ⊗ Y).HomotopyCategory).map (homMk (ex.tensor ey))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case comp_of.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
m₁ b₁ : ℕ
h₁' : mk m₁ = mk (m + 1)
g : mk (m₁ + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
h' : L₁.length = b₁
hL₁ : IsAdmissible m₁ L₁
e₁ : g = standardσ L₁ ⋯
⊢ ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk m) (h₂ : mk (m₁ + b₁) = mk (m_1 + b)) (h : L.length = b),
      IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L ⋯

Tactic:
obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'

Goal state after:
case comp_of.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
b₁ : ℕ
h' : L₁.length = b₁
h₁' : mk (m + 1) = mk (m + 1)
g : mk (m + 1 + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
hL₁ : IsAdmissible (m + 1) L₁
e₁ : g = standardσ L₁ ⋯
⊢ ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk m) (h₂ : mk (m + 1 + b₁) = mk (m_1 + b)) (h : L.length = b),
      IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L ⋯
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
φ : ⦋1⦌ ⟶ ⦋n⦌
⊢ 0 ≤ 1

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
i : SimplexCategoryᵒᵖ
x✝ : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C
⊢ (ConcreteCategory.hom
          (↾EnrichedFunctor.comp SSet
              (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (𝟙 i).unop).uliftMap))).toFun
      x✝ =
    (ConcreteCategory.hom
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x✝

Tactic:
change EnrichedFunctor.comp SSet (SimplicialThickening.functor OrderHom.id) _ = _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
i : SimplexCategoryᵒᵖ
x✝ : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C
⊢ EnrichedFunctor.comp SSet (SimplicialThickening.functor OrderHom.id) x✝ =
    (ConcreteCategory.hom
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : map' g x.castSucc = y.castSucc
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
rw [hy]
      rw [map'_eq_castSucc_iff] at hy
      obtain ⟨z, hz⟩ | hz := Fin.eq_castSucc_or_eq_last (map' f y.castSucc)
      · rw [hz, Eq.comm]
        rw [map'_eq_castSucc_iff] at hz ⊢
        constructor
        · refine hy.1.trans ?_
          simp only [OrderHom.comp_coe, Function.comp_apply, Fin.castSucc_le_castSucc_iff]
          exact g.monotone (by simpa using hz.1)
        · intro i hi
          exact hy.2 (f i) (by simpa using hz.2 i hi)
      · rw [hz, Eq.comm]
        rw [map'_eq_last_iff] at hz ⊢
        intro i
        exact hy.2 (f i) (by simpa using hz i)

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
dx : ℕ
x : X _⦋dx⦌
y : X _⦋dx + 1⦌
hxy : { dim := dx, simplex := x }.IsUniquelyCodimOneFace { dim := dx + 1, simplex := y }
⊢ ⋯.index ⋯ = hxy.index ⋯

Tactic:
symm

Goal state after:
X Y : SSet
e : X ≅ Y
dx : ℕ
x : X _⦋dx⦌
y : X _⦋dx + 1⦌
hxy : { dim := dx, simplex := x }.IsUniquelyCodimOneFace { dim := dx + 1, simplex := y }
⊢ hxy.index ⋯ = ⋯.index ⋯
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
⊢ map' f x ≤ map' f y

Tactic:
exact Finset.min'_subset _ (fun z hz ↦ by
    obtain ⟨z, rfl⟩ | rfl := z.eq_castSucc_or_eq_last
    · simp only [castSucc_mem_finset_iff] at hz ⊢
      exact hxy.trans hz
    · simp)

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:
symm

Goal state after:
X : SSet
inst✝ : X.Nonsingular
x y z : X.N
h : x ≤ y
h' : y ≤ z
⊢ monoOfLE ⋯ = monoOfLE h ≫ monoOfLE h'
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

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

Tactic:
simp [(P.isUniquelyCodimOneFace s).δ_index]

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:
symm

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
⊢ h.index s = ⋯.index ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : l.succ ≤ i
⊢ k.succ ≤ (x.cast hd).simplex.1 i

Tactic:
rw [← hl.simplex_fst_succ]

Goal state after:
case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : l.succ ≤ i
⊢ (x.cast hd).simplex.1 l.succ ≤ (x.cast hd).simplex.1 i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : InnerFibration p
sq₁₃ : internalHom.PullbackObjObj i p
⊢ InnerFibration sq₁₃.π

Tactic:
rw [innerFibration_iff]
  intro _ _ _ ⟨k, h0, hn⟩
  let sq₁₂ := Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[_, k].ι
  rw [← internalHomAdjunction₂.hasLiftingProperty_iff sq₁₂]
  suffices innerAnodyneExtensions sq₁₂.ι from
    this _ (by rwa [← innerFibration_iff])
  intro E B p hp
  rw [HasLiftingProperty.iff_of_arrow_iso_left
    (show Arrow.mk sq₁₂.ι ≅ Arrow.mk sq₁₂.flipTensor.ι from
      Arrow.isoMk (Iso.refl _) (β_ _ _))]
  let sq₁₃' := Functor.PullbackObjObj.ofHasPullback MonoidalClosed.internalHom Λ[_, k].ι p
  rw [internalHomAdjunction₂.hasLiftingProperty_iff _ sq₁₃']
  suffices (MorphismProperty.monomorphisms _).rlp sq₁₃'.π from this _ inferInstance
  rw [rlp_monomorphisms]
  rintro _ _ _ ⟨n⟩
  rw [← internalHomAdjunction₂.hasLiftingProperty_iff
    (Subcomplex.unionProd.pushoutObjObj.{u} _ _),
    Subcomplex.unionProd.pushoutObjObj_ι]
  exact prodStdSimplex.innerAnodyneExtensions_unionProd_ι k h0 hn n _ hp

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

Goal state before:
pp: p : ℕ
i : Fin (p + 1)
⊢ (stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)

Tactic:
nonDegenerate_max_dim_iff _ rfl

Goal state after:
p : ℕ
i : Fin (p + 1)
⊢ orderHomOfSimplex (stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc) ⋯ = OrderHom.id
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

Goal state before:
pp: case refine_2
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
s₂ : Δ[1] _⦋p + 1⦌
hs : (s₁, s₂) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
⊢ ∃ a, (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a = ⟨(s₁, s₂), hs⟩

Tactic:
nonDegenerate_max_dim_iff _ rfl

Goal state after:
case refine_2
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
s₂ : Δ[1] _⦋p + 1⦌
hs✝ : (s₁, s₂) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, s₂) ⋯ = OrderHom.id
⊢ ∃ a, (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a = ⟨(s₁, s₂), hs✝⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
⊢ A.image f.map ≤ B

Tactic:
rintro n _ ⟨a, ha, rfl⟩
  have := f.map_coe ⟨a, ha⟩
  aesop

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

Goal state before:
pp: X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
h : f.Homotopy g
f' : RelativeMorphism B C ψ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ A.ι ▷ Δ[1] ≫ h.h ≫ f'.map = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι

Tactic:
simp [h.rel_assoc, ← fac]

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := ⋯
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := ⋯
hg : HasFPowerSeriesOnBall g p x p.radius
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
⊢ Set.EqOn g f (Metric.eball x r)

Tactic:
symm

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := ⋯
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := ⋯
hg : HasFPowerSeriesOnBall g p x p.radius
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
⊢ Set.EqOn f g (Metric.eball x r)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : v (b ^ q.den / a ^ q.num) < 1
hq₂ : 1 < w (b ^ q.den / a ^ q.num)
⊢ False

Tactic:
exact not_lt_of_gt (h.lt_one_iff.1 hq₁) hq₂

Goal state after: