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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ Hσ q = Hσ q ≫ (alternatingFaceMapComplex C).map f

Tactic:
unfold Hσ

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ nullHomotopicMap' (hσ' q) =
    nullHomotopicMap' (hσ' q) ≫ (alternatingFaceMapComplex C).map f
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
n m : ℕ
hnm : (ComplexShape.down ℕ).Rel m n
⊢ ((alternatingFaceMapComplex C).map f).f n ≫ hσ' q n m hnm = hσ' q n m hnm ≫ ((alternatingFaceMapComplex C).map f).f m

Tactic:
simp only [alternatingFaceMapComplex_map_f, hσ'_naturality]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ (Hσ q).f n = G.map ((Hσ q).f n)

Tactic:
unfold Hσ

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: 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
⊢ φ ≫ (Hσ q).f (n + 1) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩

Tactic:
rw [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl),
    hσ'_eq hnaq (c_mk (n + 1) n rfl), hσ'_eq (hnaq_shift 1) (c_mk (n + 2) (n + 1) rfl)]

Goal state after:
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
⊢ φ ≫
      ((AlternatingFaceMapComplex.obj X).d (n + 1) n ≫ ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯ +
        (((-1) ^ (a + 1) • X.σ ⟨a + 1, ⋯⟩) ≫ eqToHom ⋯) ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1)) =
    -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ ↑p ^ (-padicValRat p { num := n, den := d, den_nz := hn, reduced := hd }) ≤ 1

Tactic:
padicValRat,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ ↑p ^
      (-(↑(padicValInt p { num := n, den := d, den_nz := hn, reduced := hd }.num) -
          ↑(padicValNat p { num := n, den := d, den_nz := hn, reduced := hd }.den))) ≤
    1
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev = (Q (n + 1)).f (n + 1)

Tactic:
· exact Eq.trans (by simp) (decomposition_Q n (n + 1)).symm

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ ((splitting K).cofan Δ).inj A ≫ (obj K).map θ =
    Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ ((splitting K).cofan Δ').inj (A.pull θ)

Tactic:
apply Obj.map_on_summand

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ factorThruImage (θ.unop ≫ A.e) ≫ image.ι (θ.unop ≫ A.e) = θ.unop ≫ A.e
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    0
⊢ ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫ (Γ₀.obj K).δ j.succ = 0

Tactic:
exact eq

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ f ≫ 𝟙 (X _⦋n⦌) ≫ PInfty.f n = 0

Tactic:
s.decomposition_id,

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ f ≫ (∑ A, s.πSummand A ≫ (s.cofan (op ⦋n⦌)).inj A) ≫ PInfty.f n = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ s.πSummand (IndexSet.id (op ⦋n⦌)) ≫ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    𝟙 (X _⦋n⦌) ≫ PInfty.f n

Tactic:
s.decomposition_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ s.πSummand (IndexSet.id (op ⦋n⦌)) ≫ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    (∑ A, s.πSummand A ≫ (s.cofan (op ⦋n⦌)).inj A) ≫ PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ s.πSummand (IndexSet.id (op ⦋i⦌)) ≫
      (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) =
    (𝟙 (X _⦋i⦌) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op ⦋j⦌))

Tactic:
s.decomposition_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ s.πSummand (IndexSet.id (op ⦋i⦌)) ≫
      (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) =
    ((∑ A, s.πSummand A ≫ (s.cofan (op ⦋i⦌)).inj A) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op ⦋j⦌))
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
y : Y
⊢ (const X y).Homotopic (const X y)

Tactic:
by rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ weakEquivalences (CofibrantObject C) ≤ (weakEquivalences C).inverseImage ι

Tactic:
by rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hcof : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (HoCat C)).Q
Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hcof ⥤ H := (localizerMorphism C).localizedFunctor Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lcofπ F)
G : H ⥤ Hcof := (HoCat.localizerMorphismResolution C).localizedFunctor L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G := CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lcofπ G
this : Localization.Lifting L (weakEquivalences C) (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F)
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
have : Localization.Lifting Lcof (weakEquivalences (CofibrantObject C))
        (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eF.symm G ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eG.symm⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hcof : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (HoCat C)).Q
Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hcof ⥤ H := (localizerMorphism C).localizedFunctor Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lcofπ F)
G : H ⥤ Hcof := (HoCat.localizerMorphismResolution C).localizedFunctor L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G := CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lcofπ G
this✝ : Localization.Lifting L (weakEquivalences C) (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F)
this : Localization.Lifting Lcof (weakEquivalences (CofibrantObject C)) (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G)
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
inst✝ : CategoryWithCofibrations C
X Y : Over S
f : X ⟶ Y
⊢ Cofibration f ↔ Cofibration (Over.Hom.left f)

Tactic:
simp only [cofibration_iff, cofibrations_over_def, MorphismProperty.over_iff]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ weakEquivalences (BifibrantObject C) ≤ (weakEquivalences C).inverseImage ι

Tactic:
by rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
⊢ c.π (J.fst default) ≫ hc.desc (isPushout.multicofork h h' s) = s.inl

Tactic:
by simpa using! hc.fac (isPushout.multicofork h h' s) (.right (J.fst default))

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ stdSimplex.face S ≤ Λ[n + 1, j] ↔ S ≠ Finset.univ ∧ S ≠ {j}ᶜ

Tactic:
rw [subcomplex_le_horn_iff, stdSimplex.face_le_face_iff, ← not_iff_not]
  simp only [Decidable.not_not, ne_eq, not_and_or]
  refine ⟨fun h ↦ ?_, by aesop⟩
  rw [← Finset.compl_subset_compl, compl_compl,
    Finset.subset_singleton_iff, Finset.compl_eq_empty_iff] at h
  grind [eq_compl_comm]

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n] ≤ ∂Δ[n]

Tactic:
by rfl

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₃ ⟶ X₄
b : X₂ ⟶ X₄
sq : IsPushout l t r b
ht : monomorphisms (Type u) t
⊢ monomorphisms (Type u) r

Tactic:
simp only [monomorphisms.iff] at ht ⊢
    exact Limits.Types.pushoutCocone_inr_mono_of_isColimit sq.flip.isColimit

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2} = Λ[2, 0]

Tactic:
by
    apply le_antisymm
    · rw [sup_le_iff]
      constructor
      · exact face_le_horn (2 : Fin 3) 0 (by simp)
      · exact face_le_horn (1 : Fin 3) 0 (by simp)
    · rw [horn_eq_iSup, iSup_le_iff]
      rintro i
      fin_cases i
      · exact le_sup_right
      · exact le_sup_left

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

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : ↑(X.nonDegenerate ↑k)
⊢ Subcomplex.ofSimplex ↑x ≤ Subcomplex.ofSimplex ↑x

Tactic:
by rfl

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

Goal state before:
pp: X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w✝ : Epi f
y : ↑(X.nonDegenerate j)
⊢ Subcomplex.ofSimplex ↑y ≤ Subcomplex.ofSimplex ↑y

Tactic:
by rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ y₃ : X₄
eq : (ConcreteCategory.hom k) x₃ = (ConcreteCategory.hom k) y₃
⊢ x₃ = y₃

Tactic:
obtain (⟨x₂, rfl⟩ | ⟨x₃, rfl, hx₃⟩) := eq_or_eq_of_isPushout' h₁ x₃

Goal state after:
case inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
y₃ : X₄
x₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) y₃
⊢ (ConcreteCategory.hom r) x₂ = y₃

case inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
y₃ : X₄
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) y₃
⊢ (ConcreteCategory.hom b) x₃ = y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
d n : ℕ
h : d < n
⊢ (X.skeleton n).obj (op ⦋d⦌) = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
X : SSet
d n : ℕ
h : d < n
⊢ ⊤ ⊆ (X.skeleton n).obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
d : ℕ
hd✝ : d < d + 1
hd : d ≤ d
x : ↑(X.nonDegenerate ↑⟨d, hd✝⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ Subcomplex.ofSimplex ↑x

Tactic:
by rfl

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤ Subcomplex.ofSimplex ↑x

Tactic:
by rfl

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d) = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ ⊤ ≤ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d)
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h
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)
⊢ (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:
let ksucc := k.succ.castSucc

Goal state after:
case h
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
⊢ (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)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: C : Type u₁
W : Type v
inst✝² : Category.{w, v} W
inst✝¹ : MonoidalCategory W
inst✝ : EnrichedCategory W C
X Y Z : C
f : 𝟙_ W ⟶ X ⟶[W] Y
g : 𝟙_ W ⟶ Y ⟶[W] Z
⊢ homOf W ((λ_ (𝟙_ W)).inv ≫ (f ⊗ₘ g) ≫ eComp W X Y Z) = homOf W f ≫ homOf W g

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u₁
W : Type v
inst✝² : Category.{w, v} W
inst✝¹ : MonoidalCategory W
inst✝ : EnrichedCategory W C
X Y Z : C
f : 𝟙_ W ⟶ X ⟶[W] Y
g : 𝟙_ W ⟶ Y ⟶[W] Z
⊢ homOf W (((λ_ (𝟙_ W)).inv ≫ (f ⊗ₘ g)) ≫ eComp W X Y Z) = homOf W f ≫ homOf W g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ B ≤ B

Tactic:
by rfl

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ A ≤ A

Tactic:
by rfl

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).image (β_ Y X).inv = T.unionProd S

Tactic:
by
  apply image_β_hom

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Terminal

Goal state before:
pp: this : IsDiscrete (ShrinkHoms.{u} PUnit.{u + 1})
⊢ HasTerminal Cat

Tactic:
exact IsTerminal.hasTerminal (X := Cat.of (ShrinkHoms PUnit)) isTerminalOfUniqueOfIsDiscrete

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk
C D : Cat
obj✝¹ : ↑C → ↑D
map✝¹ : {X Y : ↑C} → (X ⟶ Y) → (obj✝¹ X ⟶ obj✝¹ Y)
map_id✝¹ : ∀ (X : ↑C), map✝¹ (𝟙 X) = 𝟙 (obj✝¹ X)
map_comp✝¹ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
obj✝ : ↑C → ↑D
map✝ : {X Y : ↑C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
hyp :
  forget.map { obj := obj✝¹, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toCatHom =
    forget.map { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.toCatHom
⊢ { obj := obj✝¹, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
cases hyp

Goal state after:
case mk.mk.refl
C D : Cat
obj✝ : ↑C → ↑D
map✝ : {X Y : ↑C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝¹ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝¹ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
map_id✝ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
⊢ { obj := obj✝, map := map✝, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk
V W : ReflQuiv
toPrefunctor✝¹ : ↑V ⥤q ↑W
map_id✝¹ : ∀ (X : ↑V), toPrefunctor✝¹.map (𝟙rq X) = 𝟙rq (toPrefunctor✝¹.obj X)
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp :
  forgetToQuiv.map { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } =
    forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }
⊢ { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }

Tactic:
cases hyp

Goal state after:
case mk.mk.refl
V W : ReflQuiv
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝¹ map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ forgetToQuiv.map ({ toPrefunctor := e.inv, map_id := ⋯ } ≫ { toPrefunctor := e.hom, map_id := h_id }) =
    forgetToQuiv.map (𝟙 (of W))

Tactic:
exact e.inv_hom_id

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 : ℕ
hij : i ≤ i
hj : i ≤ n
⊢ ⟨i, ⋯⟩ ≤ ⟨i, ⋯⟩

Tactic:
by rfl

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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
Zf : C
f₁ : X ⟶ Zf
f₂ : Zf ⟶ Z
hf₁ : W₁ f₁
hf₂ : W₂ f₂
fac_f : f₁ ≫ f₂ = f
eq_f : r.degHom f = r.deg Zf
Zg : C
g₁ : Z ⟶ Zg
g₂ : Zg ⟶ Y
hg₁ : W₁ g₁
hg₂ : W₂ g₂
fac_g : g₁ ≫ g₂ = g
eq_g : r.degHom g = r.deg Zg
Zh : C
h₁ : Zf ⟶ Zh
h₂ : Zh ⟶ Zg
hh₁ : W₁ h₁
hh₂ : W₂ h₂
fac_h : h₁ ≫ h₂ = f₂ ≫ g₁
eq_h : r.degHom (f₂ ≫ g₁) = r.deg Zh
factfg : W₁.MapFactorizationData W₂ (f ≫ g) := { Z := Zh, i := f₁ ≫ h₁, p := h₂ ≫ g₂, fac := ⋯, hi := ⋯, hp := ⋯ }
⊢ r.degHom (f ≫ g) ≤ r.deg Z

Tactic:
r.degHom_eq factfg

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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
Zf : C
f₁ : X ⟶ Zf
f₂ : Zf ⟶ Z
hf₁ : W₁ f₁
hf₂ : W₂ f₂
fac_f : f₁ ≫ f₂ = f
eq_f : r.degHom f = r.deg Zf
Zg : C
g₁ : Z ⟶ Zg
g₂ : Zg ⟶ Y
hg₁ : W₁ g₁
hg₂ : W₂ g₂
fac_g : g₁ ≫ g₂ = g
eq_g : r.degHom g = r.deg Zg
Zh : C
h₁ : Zf ⟶ Zh
h₂ : Zh ⟶ Zg
hh₁ : W₁ h₁
hh₂ : W₂ h₂
fac_h : h₁ ≫ h₂ = f₂ ≫ g₁
eq_h : r.degHom (f₂ ≫ g₁) = r.deg Zh
factfg : W₁.MapFactorizationData W₂ (f ≫ g) := { Z := Zh, i := f₁ ≫ h₁, p := h₂ ≫ g₂, fac := ⋯, hi := ⋯, hp := ⋯ }
⊢ r.deg factfg.Z ≤ r.deg Z
Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory

Goal state before:
pp: X✝ Y✝ : SemiSimplexCategory
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toSimplexCategory.map a₁✝ = toSimplexCategory.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by
    ext : 2
    apply ConcreteCategory.congr_hom h

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
⊢ x = y

Tactic:
by
  apply Path.ext
  ext
  apply h

Goal state after: