mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} A'
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₁ hF).counitIso = equivalence₁CounitIso hF

Tactic:
ext Y

Goal state after:
A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} A'
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
Y : B'
⊢ (equivalence₁ hF).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso.hom.app = (equivalenceCounitIso η).hom.app

Tactic:
ext Y

Goal state after:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ (equivalence hF hG).counitIso.hom.app Y = (equivalenceCounitIso η).hom.app Y
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ {x y : ℚ_[p]}, ↑(padicNormE (x - y)) = 0 → x = y

Tactic:
intro _

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ : ℚ_[p]
⊢ ∀ {y : ℚ_[p]}, ↑(padicNormE (x✝ - y)) = 0 → x✝ = y
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| ∑ x, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q x))) • φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ ⟨a, ⋯⟩

pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| ∑ x,
    ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q x)) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x))

Tactic:
· rw [Fin.sum_univ_castSucc]

Goal state after:
case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| ∑ x,
    ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q x)) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x))
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| ∑ x,
    ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q x)) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x))

Tactic:
· rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).Factors ((P (n + 1)).f (n + 1))

Tactic:
NormalizedMooreComplex.objX,

Goal state after:
case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).Factors ((P (n + 1)).f (n + 1))
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ : ∀ (i : ℕ), (inv (N₁.map f)).f.f i ≫ PInfty.f i ≫ f.app (op ⦋i⦌) = PInfty.f i
h₃ :
  ∀ (n : ℕ), PInfty.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) = (inv (N₁.map f)).f.f n ≫ PInfty.f n ≫ f.app (op ⦋n⦌)
h₁ : ∀ (i : ℕ), PInfty.f i ≫ f.app (op ⦋i⦌) ≫ (inv (N₁.map f)).f.f i = PInfty.f i
n : ℕ
⊢ IsIso (f.app (op ⦋n⦌))

Tactic:
induction n with
    -- degree 0
    | zero =>
      use (inv (N₁.map f)).f.f 0
      have h₁₀ := h₁ 0
      have h₂₀ := h₂ 0
      dsimp at h₁₀ h₂₀
      simp only [id_comp] at h₁₀ h₂₀
      tauto
    | succ n hn =>
      use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }
      simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
        PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
        SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case neg.h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n⦌.len ≠ n'

pp: case neg.h₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ¬Isδ₀ i

Tactic:
· exact h

Goal state after:
case neg.h₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ¬Isδ₀ i
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      ((Γ₀.splitting (N₂.obj P).X).desc (op ⦋n⦌) fun A ↦
          (PInfty.f (unop A.fst).len ≫ P.p.app A.fst) ≫
            ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).cofan (op ⦋n⦌)).inj A) ≫
        ((Γ₂N₂ToKaroubiIso.hom.app P.X).f.app (op ⦋n⦌) ≫
            (Γ₀.splitting K[P.X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ P.X.map A.e.op) ≫
          P.p.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)

Tactic:
Γ₂N₂ToKaroubiIso_hom_app,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      ((Γ₀.splitting (N₂.obj P).X).desc (op ⦋n⦌) fun A ↦
          (PInfty.f (unop A.fst).len ≫ P.p.app A.fst) ≫
            ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).cofan (op ⦋n⦌)).inj A) ≫
        ((Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app P.X)).f.app (op ⦋n⦌) ≫
            (Γ₀.splitting K[P.X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ P.X.map A.e.op) ≫
          P.p.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e' = cast hu hv e ↔ e' ≍ e

Tactic:
by
  rw [eq_comm, Hom.cast_eq_iff_heq]
  exact ⟨HEq.symm, HEq.symm⟩

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ Path u v = Path u' v'

Tactic:
by rw [hu, hv]

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

Goal state before:
pp: case h_map
I : Type u
X : I → TopCat
⊢ autoParam
    (∀ (X_1 Y : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))) (f : X_1 ⟶ Y),
      (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
        CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯)
    CategoryTheory.Functor.ext._auto_1

Tactic:
intro _

Goal state after:
case h_map
I : Type u
X : I → TopCat
X✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
⊢ ∀ (Y : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))) (f : X✝ ⟶ Y),
    (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
      CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_map
A : TopCat
B : TopCat
⊢ ∀ (X Y : ↑(π.obj (TopCat.of (↑A × ↑B)))) (f : X ⟶ Y),
    ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f ≍ (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f

Tactic:
rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ f

Goal state after:
case h_map
A : TopCat
B : TopCat
x₀ : ↑A
x₁ : ↑B
y₀ : ↑A
y₁ : ↑B
f : { as := (x₀, x₁) } ⟶ { as := (y₀, y₁) }
⊢ ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f ≍ (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ ⟦p₁⟧ ≍ ⟦p₂⟧

Tactic:
obtain rfl : x₀ = x₂ := by convert! hp 0 <;> simp
  obtain rfl : x₁ = x₃ := by convert! hp 1 <;> simp
  rw [heq_iff_eq]; congr; ext t; exact hp t

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
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
⊢ (const Y x₀).Homotopic (const Y x₁) ↔ Joined x₀ x₁

Tactic:
refine ⟨fun ⟨H⟩ ↦ ⟨⟨(H.toContinuousMap.comp .prodSwap).curry default, ?_, ?_⟩⟩,
    fun ⟨p⟩ ↦ ⟨p.toHomotopyConst⟩⟩

Goal state after:
case refine_1
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
x✝ : (const Y x₀).Homotopic (const Y x₁)
H : (const Y x₀).Homotopy (const Y x₁)
⊢ ((H.comp prodSwap).curry default).toFun 0 = x₀

case refine_2
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
x✝ : (const Y x₀).Homotopic (const Y x₁)
H : (const Y x₀).Homotopy (const Y x₁)
⊢ ((H.comp prodSwap).curry default).toFun 1 = x₁
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (fibrations Cᵒᵖ).IsStableUnderRetracts

Tactic:
rw [fibrations_op]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject.HoCat C
⊢ IsIso (HoCat.adjCounit'.app X)

Tactic:
by
  obtain ⟨X, rfl⟩ := BifibrantObject.toHoCat_obj_surjective X
  rw [HoCat.adjCounit'_app]
  have : WeakEquivalence (C := BifibrantObject C)
      (BifibrantObject.homMk ((mk X.obj).iBifibrantResolutionObj).hom) := by
    simp only [BifibrantObject.weakEquivalence_homMk_iff]
    infer_instance
  infer_instance

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

Goal state before:
pp: case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
⊢ A ≤ Λ[n + 1, i]

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

Goal state after:
case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
⊢ ∀ (n_1 : ℕ) (x : ↑(Δ[n + 1].nonDegenerate n_1)), ↑x ∈ A.obj (op ⦋n_1⦌) → ↑x ∈ Λ[n + 1, i].obj (op ⦋n_1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ objMk OrderHom.id ∉ ∂Δ[n].obj (op ⦋n⦌)

Tactic:
rw [boundary_eq_iSup, Subfunctor.iSup_obj, Set.mem_iUnion, not_exists]
  intro i hi
  simpa using @hi i (by aesop)

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n].op.preimage (stdSimplex.opIso ⦋n⦌).inv = ∂Δ[n]

Tactic:
ext ⟨⟨d⟩⟩ j
  simp only [Subcomplex.preimage_obj, Set.mem_preimage, stdSimplex.opIso_inv_app_hom_apply,
    Subcomplex.mem_op_obj_iff, mem_boundary_iff_notMem_range, Set.mem_range,
    stdSimplex.opObjEquiv_opObjEquiv_symm_apply, not_exists]
  constructor
  all_goals
  · rintro ⟨k, hk⟩
    exact ⟨k.rev, fun l _ ↦ hk l.rev (by aesop)⟩

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

Goal state before:
pp: case refine_2
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
⊢ A ≤ ∂Δ[n]

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

Goal state after:
case refine_2
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
⊢ ∀ (n_1 : ℕ) (x : ↑(Δ[n].nonDegenerate n_1)), ↑x ∈ A.obj (op ⦋n_1⦌) → ↑x ∈ ∂Δ[n].obj (op ⦋n_1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (fibrations SSet).IsMultiplicative

Tactic:
fibrations_eq

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ J.rlp.IsMultiplicative
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (fibrations SSet).IsStableUnderRetracts

Tactic:
fibrations_eq

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ J.rlp.IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex

Goal state before:
pp: Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
⊢ fibrations SSet (terminal.from Z)

Tactic:
fibrations_eq

Goal state after:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
⊢ J.rlp (terminal.from Z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex

Goal state before:
pp: Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
⊢ J.rlp (terminal.from Z)

Tactic:
intro _

Goal state after:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X✝ : SSet
⊢ ∀ ⦃Y : SSet⦄ (g : X✝ ⟶ Y), J g → HasLiftingProperty g (terminal.from Z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
⊢ ⊤ ≤ ⨆ n, X.skeleton n

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

Goal state after:
X : SSet
⊢ ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ ⊤.obj (op ⦋n⦌) → ↑x ∈ (⨆ n, X.skeleton n).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∂Δ[d] ≤ ((skeletonOfMono i) d).preimage c.map

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

Goal state after:
case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∀ (n : ℕ) (x : ↑(Δ[d].nonDegenerate n)),
    ↑x ∈ ∂Δ[d].obj (op ⦋n⦌) → ↑x ∈ (((skeletonOfMono i) d).preimage c.map).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case mk.zero
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
hm : ⦋0⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋0⦌, property := hm })
fac : SimplexCategory.δ (Fin.castSucc 0) ≫ SimplexCategory.σ 0 = 𝟙 ⦋0⦌
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋0⦌, property := hm }))).toFun x

Tactic:
dsimp at fac

Goal state after:
case mk.zero
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
hm : ⦋0⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋0⦌, property := hm })
fac : SimplexCategory.δ 0 ≫ SimplexCategory.σ 0 = 𝟙 ⦋0⦌
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋0⦌, property := hm }))).toFun x
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
rw [← spine_arrow, spine_δ_arrow_gt sx _ hgt]
    dsimp
    apply congr_arg
    apply Subtype.ext
    dsimp [horn.face, CosimplicialObject.δ]
    rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
      Quiver.Hom.unop_op, SSet.yonedaEquiv_map, Equiv.apply_symm_apply,
      mkOfSucc_δ_gt hgt]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
X✝ Y✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
⊢ (id W C).forget.map f ≫ (Iso.refl ((id W C).forget.obj Y✝)).hom =
    (Iso.refl ((id W C).forget.obj X✝)).hom ≫ (𝟭 (ForgetEnrichment W C)).map f

Tactic:
simp [forget]

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ range ((A.prod B).ι ≫ fst X Y) ≤ A

Tactic:
intro _

Goal state after:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
⊢ (range ((A.prod B).ι ≫ fst X Y)).obj i✝ ⊆ A.obj i✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ range ((A.prod B).ι ≫ fst X Y) ≤ A

Tactic:
intro _ _ ⟨⟨_, ⟨_, _⟩⟩, _⟩

Goal state after:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
a✝ : X.obj i✝
val✝ : (X ⊗ Y).obj i✝
left✝ : val✝.1 ∈ A.obj i✝
right✝ : val✝.2 ∈ B.obj i✝
h✝ : (ConcreteCategory.hom (((A.prod B).ι ≫ fst X Y).app i✝)) ⟨val✝, ⋯⟩ = a✝
⊢ a✝ ∈ A.obj i✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ range ((A.prod B).ι ≫ snd X Y) ≤ B

Tactic:
intro _

Goal state after:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
⊢ (range ((A.prod B).ι ≫ snd X Y)).obj i✝ ⊆ B.obj i✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ range ((A.prod B).ι ≫ snd X Y) ≤ B

Tactic:
intro _ _ ⟨⟨_, ⟨_, _⟩⟩, _⟩

Goal state after:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
a✝ : Y.obj i✝
val✝ : (X ⊗ Y).obj i✝
left✝ : val✝.1 ∈ A.obj i✝
right✝ : val✝.2 ∈ B.obj i✝
h✝ : (ConcreteCategory.hom (((A.prod B).ι ≫ snd X Y).app i✝)) ⟨val✝, ⋯⟩ = a✝
⊢ a✝ ∈ B.obj i✝
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
⊢ ⊤ ≤ (morphismPropertyHomMk V).multiplicativeClosure

Tactic:
intro _

Goal state after:
V : Type u_1
inst✝ : ReflQuiver V
X✝ : FreeRefl V
⊢ ∀ ⦃Y : FreeRefl V⦄ (f : X✝ ⟶ Y), ⊤ f → (morphismPropertyHomMk V).multiplicativeClosure f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: ⊢ generators.multiplicativeClosure = ⊤

Tactic:
apply le_antisymm (by simp)
  rintro x y f -
  induction f using CategoryTheory.Quotient.induction with | _ f
  induction f using Paths.induction with
  | id => exact generators.multiplicativeClosure.id_mem _
  | comp _ k h =>
    cases k
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _

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
⊢ generators.multiplicativeClosure ≤ P

Tactic:
intro _

Goal state after:
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✝ : SimplexCategoryGenRel
⊢ ∀ ⦃Y : SimplexCategoryGenRel⦄ (f : X✝ ⟶ Y), generators.multiplicativeClosure f → P f
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
⊢ generators.multiplicativeClosure' ≤ P

Tactic:
intro _

Goal state after:
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✝ : SimplexCategoryGenRel
⊢ ∀ ⦃Y : SimplexCategoryGenRel⦄ (f : X✝ ⟶ Y), generators.multiplicativeClosure' f → P f
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s✝ t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
s t : RelUpperSet P
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by cases s; cases t; congr

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s✝ t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
s t : RelLowerSet P
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by cases s; cases t; congr

Goal state after:
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
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ Fin (⦋i⦌.len + 1)

Tactic:
exact k

Goal state after: