mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
i j : (glueData hf).J
⊢ yoneda.map (⋯.fst' (f j)) ≫ f i = yoneda.map (⋯.symmetry ⋯ ≫ ⋯.fst' (f i)) ≫ f j

Tactic:
Functor.relativelyRepresentable.symmetry_fst,

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
i j : (glueData hf).J
⊢ yoneda.map (⋯.fst' (f j)) ≫ f i = yoneda.map (⋯.snd (f j)) ≫ f j
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x ∈ closure (Set.range Rat.cast)

Tactic:
Metric.mem_closure_range_iff

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ∀ ε > 0, ∃ k, dist x ↑k < ε
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : n + 1 < q
⊢ φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0

Tactic:
hσ'_eq_zero hqn' (c_mk (n + 2) (n + 1) rfl),

Goal state after:
case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : n + 1 < q
⊢ φ ≫ 0 ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Homotopy (P (q + 1)) (𝟙 K[X])

Tactic:
refine
      Homotopy.trans (Homotopy.ofEq ?_)
        (Homotopy.trans
          (Homotopy.add (homotopyPToId q) (Homotopy.compLeft (homotopyHσToZero q) (P q)))
          (Homotopy.ofEq ?_))

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P (q + 1) = P q + P q ≫ Hσ q

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] + P q ≫ 0 = 𝟙 K[X]
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive

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.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ α.inv = β.hom ≫ 𝟙 ((𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P))

Tactic:
← Iso.inv_comp_eq

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.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ β.inv ≫ α.inv = 𝟙 ((𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P))
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: case h_p
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).X n).p ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫
      (((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).X
          n).p

Tactic:
· dsimp
        simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
h : X ≃ₕ Unit
h' : Y ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)

Tactic:
exact ⟨h.trans h'.symm⟩

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
⊢ (toHoCatLocalizerMorphism C).IsLocalizedEquivalence

Tactic:
by
  apply (factorsThroughLocalization C).isLocalizedEquivalence
  apply MorphismProperty.eq_inverseImage_quotientFunctor

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

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

Tactic:
by
  obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X
  rw [HoCat.adjUnit_app, weakEquivalence_toHoCat_map_iff,
    weakEquivalence_iff_of_objectProperty]
  infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
⊢ trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor

Tactic:
simp [trivialCofibrations, h₁, h₃]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
⊢ x ∈
      {x |
        ∃ (hx : x ∈ A.obj U✝), (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩} →
    x ∈
      ⇑(ConcreteCategory.hom (F₁.map φ)) ⁻¹'
        {x |
          ∃ (hx : x ∈ A.obj V✝), (ConcreteCategory.hom (f.app V✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app V✝)) ⟨x, hx⟩}

Tactic:
rintro ⟨hx, h⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
hx : x ∈ A.obj U✝
h : (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩
⊢ x ∈
    ⇑(ConcreteCategory.hom (F₁.map φ)) ⁻¹'
      {x | ∃ (hx : x ∈ A.obj V✝), (ConcreteCategory.hom (f.app V✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app V✝)) ⟨x, hx⟩}
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u''
inst✝¹ : Category.{v'', u''} J
inst✝ : HasPushouts C
⊢ (epimorphisms C).functorCategory J = epimorphisms (J ⥤ C)

Tactic:
ext _ _ f
  simp only [functorCategory, epimorphisms.iff, NatTrans.epi_iff_epi_app]

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

Goal state before:
pp: case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl y₁) →
    x₁ = y₁ ∨
      ∃ x₀ y₀,
        ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
          x₁ = (ConcreteCategory.hom f) x₀ ∧ y₁ = (ConcreteCategory.hom f) y₀

pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ (x₁ = y₁ ∨
      ∃ x₀ y₀,
        ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
          x₁ = (ConcreteCategory.hom f) x₀ ∧ y₁ = (ConcreteCategory.hom f) y₀) →
    Rel' f g (Sum.inl x₁) (Sum.inl y₁)

Tactic:
· rintro (_ | ⟨_, _, h⟩)
    · exact Or.inl rfl
    · exact Or.inr ⟨_, _, h, rfl, rfl⟩

Goal state after:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ (x₁ = y₁ ∨
      ∃ x₀ y₀,
        ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
          x₁ = (ConcreteCategory.hom f) x₀ ∧ y₁ = (ConcreteCategory.hom f) y₀) →
    Rel' f g (Sum.inl x₁) (Sum.inl y₁)
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
hf : Fibration f
n : ℕ
i : Fin (n + 2)
⊢ HasLiftingProperty Λ[n + 1, i].ι f

Tactic:
fibration_iff

Goal state after:
X Y : SSet
f : X ⟶ Y
hf : J.rlp f
n : ℕ
i : Fin (n + 2)
⊢ HasLiftingProperty Λ[n + 1, i].ι f
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
⊢ Fibration f

Tactic:
fibration_iff

Goal state after:
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
⊢ J.rlp f
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a.left
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 1]

pp: case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 1]

Tactic:
· exact face_le_horn (2 : Fin 3) 1 (by simp)

Goal state after:
case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 1]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ≤
      Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ∧
    Y.skeleton n ≤
        Subcomplex.range i ⊔ Y.skeleton n ⊔
          ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ∧
      ∀ (i_1 : ↑(Y.nonDegenerate n)),
        Subcomplex.ofSimplex ↑i_1 ≤
          Subcomplex.range i ⊔ Y.skeleton n ⊔
            ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
refine ⟨le_sup_left.trans le_sup_left,
      le_sup_right.trans le_sup_left, fun x ↦ ?_⟩

Goal state after:
case a
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case pos
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∈ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

pp: case neg
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
· exact le_trans (le_trans (by simpa) le_sup_left) le_sup_left

Goal state after:
case neg
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ ∀ {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), tensorHom f g = whiskerRight f X₂ ≫ Y₁.whiskerLeft g

Tactic:
intros; ext; simp [tensorHom_def]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U : C
⊢ (X.snd.β Y.fst).hom ▷ U ≫ ((Y ⊗ X).snd.β U).hom = ((X ⊗ Y).snd.β U).hom ≫ U ◁ (X.snd.β Y.fst).hom

Tactic:
dsimp
      simp only [Category.assoc]
      rw [← IsIso.inv_comp_eq, IsIso.Iso.inv_hom, ← HalfBraiding.monoidal_assoc,
        ← HalfBraiding.naturality_assoc, HalfBraiding.monoidal]
      simp

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

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hfg : HomotopicR f g
hgh : HomotopicR g h
⊢ HomotopicR f h

Tactic:
rcases hfg with ⟨hfg⟩
  rcases hgh with ⟨hgh⟩
  exact Quasicategory₂.fill31 (idComp (id x)) hfg hgh

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

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

Tactic:
by simp [h'']

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case mk.mk
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 : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
c : ℕ
h : a + b = c
⊢ W f

Tactic:
induction c generalizing a b with

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.left.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx✝ : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc ≤ i.succAbove x

Tactic:
Fin.succAbove_of_castSucc_lt

Goal state after:
case pos.inl.left.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx✝ : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc ≤ x.castSucc

case pos.inl.left.inl.h
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx✝ : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc < i
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inr
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 1)).castSucc = Fin.last (n + 1)

Tactic:
· obtain rfl : i = Fin.last _ := Fin.last_le_iff.1 hx
        simp [map'_eq_last_iff]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
this : IsEmpty { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑h.pairing.II
hf : ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.AncestralRel ((fun n ↦ h.equivII.symm (f n)) (n + 1)) ((fun n ↦ h.equivII.symm (f n)) n)

Tactic:
simpa [ancestralRel_iff] using hf n

Goal state after:
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:
rwa [SSet.S.ext_iff]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ : h.pairing.IsRegular
this✝ : h.IsProper
this : IsEmpty { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
f : ℕ → h.ι
hf : ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.pairing.AncestralRel ((fun n ↦ h.equivII (f n)) (n + 1)) ((fun n ↦ h.equivII (f n)) n)

Tactic:
simpa [ancestralRel_iff] using hf n

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ ∀ (j : WalkingCospan),
    (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
        (c x✝).π.app j =
      𝟙 (c x✝).pt ≫ (c x✝).π.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app none =
    𝟙 (c x✝).pt ≫ (c x✝).π.app none

case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.left) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.left)

case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.right) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ∀ (j : WalkingCospan),
    (hc Z✝).lift
          { pt := (c X✝).pt,
            π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
        (c Z✝).π.app j =
      ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
          (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
        (c Z✝).π.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app none =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app none

case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.left) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.left)

case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.right) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
⊢ IsCardinalPresentable c.pt κ

Tactic:
by
  have (k : Kᵒᵖ) : ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ := by
    dsimp; infer_instance
  exact Functor.isCardinalAccessible_of_isLimit
    (coyoneda.mapCone c.op) (isLimitOfPreserves _ hc.op) κ (by simpa)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerAnodyneExtensions Λ[n, i].ι

Tactic:
innerAnodyneExtensions_eq_llp_rlp

Goal state after:
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions.rlp.llp Λ[n, i].ι
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: case h₁
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct α
this : l.l ≫ f₃ = Arrow.Hom.right α
⊢ (adj₂.homEquiv l.l ≫ sq₁₃.π) ≫ sq₁₃.snd = Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α) ≫ sq₁₃.snd

Tactic:
simp only [Category.assoc, sq₁₃.π_snd, ← this, adj₂.homEquiv_naturality_three,
            arrowHomEquiv_apply_right_snd, Arrow.mk_right]

Goal state after:
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]

Goal state after:
X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : InnerFibration p
sq₁₃ : internalHom.PullbackObjObj i p
⊢ innerFibrations sq₁₃.π
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

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

Tactic:
fibration_iff

Goal state after:
X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
⊢ J.rlp sq₁₃.π
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 + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
t : Fin (d + 1)
ht : IsIndex hl.δ ⋯ t
h : t = 0
⊢ False

Tactic:
by simp [h] at ht

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom (SimplicialObject.σ Δ[1] j)) (objMk₁ i)) k = (objMk₁ i.castSucc) k

Tactic:
exact ConcreteCategory.congr_hom (SimplexCategory.σ_comp_toMk₁_of_le _ _ h) k

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

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ ↑(((ConcreteCategory.hom
                (X.map
                  (stdSimplex.objEquiv
                      ((ConcreteCategory.hom (δ Δ[n] (Fin.last (n + 1))))
                        (stdSimplex.objEquiv.symm (SimplexCategory.σ (Fin.last n))))).op))
              x,
            (ConcreteCategory.hom (δ Δ[1] (Fin.last (n + 1)))) (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)).2
        k) =
    ↑(((ConcreteCategory.hom (ι₀.app (op ⦋n⦌))) x).2 k)

Tactic:
simp [stdSimplex.δ_objMk₁_of_le, stdSimplex.objMk₁_apply_eq_zero_iff, ← Fin.castSucc_succ]

Goal state after: