mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
p : Homotopic.Quotient as bs
⊢ (pi fun i ↦ proj i p) = p

Tactic:
induction p using Quotient.inductionOn

Goal state after:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a✝ : Path as bs
⊢ (pi fun i ↦ proj i ⟦a✝⟧) = ⟦a✝⟧
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i✝ : Fin (n + 1)
i : ↑{i✝}ᶜ
⊢ {↑i}ᶜ.card ≤ n

Tactic:
simp [Finset.card_compl]

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

Goal state before:
pp: X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
h : Lattice.BicartSq (A₁.obj n) (A₂.obj n) (A₃.obj n) (A₄.obj n)
⊢ IsColimit ((PushoutCocone.mk (homOfLE ⋯) (homOfLE ⋯) ⋯).map ((evaluation SimplexCategoryᵒᵖ (Type u)).obj n))

Tactic:
exact (Types.isPushout_of_bicartSq h).isColimit

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ {i}ᶜ.card ≤ n

Tactic:
simp [Finset.card_compl]

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : Sᶜ ⊆ {j}
⊢ S = Finset.univ ∨ S = {j}ᶜ

Tactic:
Finset.subset_singleton_iff,

Goal state after:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : Sᶜ = ∅ ∨ Sᶜ = {j}
⊢ S = Finset.univ ∨ S = {j}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
h : ((skeletonOfMono i) d).preimage c.map = ⊤
⊢ c.simplex ∈ Set.range ⇑(ConcreteCategory.hom (i.app (op ⦋d⦌)))

Tactic:
have := h.symm.le _ (show stdSimplex.objEquiv.symm (𝟙 ⦋d⦌) ∈ _ by simp)
    simpa [mem_skeletonOfMono_obj_iff]

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

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑(horn.primitiveTriangle i h₀ hₙ ↑k ⋯))) z =
    (stdSimplex.objEquiv.symm (intervalEdge (↑k) 2 ⋯)) z

Tactic:
fin_cases z <;> rfl

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

Goal state before:
pp: case id
V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
x✝ : V
⊢ (morphismPropertyHomMk V).multiplicativeClosure (homMk (𝟙rq x✝))

Tactic:
exact le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _)

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)
⊢ ⊤.strictMap (quotientFunctor V) ((quotientFunctor V).map f)

Tactic:
exact map_mem_strictMap _ _ _ (by 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 : Edge x y
h : HomotopicR f g
⊢ HomotopicL f g

Tactic:
by
  rcases h with ⟨h⟩
  exact Quasicategory₂.fill31 (idComp f) (compId f) h

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

Goal state before:
pp: V : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : V.HomotopyCategory ⥤ D
h₁ : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), F.obj (mk x) = G.obj (mk x)
h₂ :
  ∀ ⦃x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    F.map (homMk e) = eqToHom ⋯ ≫ G.map (homMk e) ≫ eqToHom ⋯
x✝¹ x✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x✝¹ x✝
⊢ F.map (homMk e) ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ G.map (homMk e)

Tactic:
by simp [h₂ e]

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
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
⊢ ⟨i + k, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk]

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
⊢ i + k ≤ j
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
⊢ ⟨i + k, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk]; omega

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
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
⊢ ⟨i + k, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk]

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
⊢ i + k ≤ j
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
⊢ ⟨i + k, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk]; omega

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

Goal state before:
pp: n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = σ i ≫ δ i'

Tactic:
δ_comp_σ_of_le h

Goal state after:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ σ i ≫ δ i' = σ i ≫ δ i'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
L : List ℕ
j head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : (∀ k ∈ tail✝, j ≤ k) → simplicialEvalσ tail✝ j = j
hj : ∀ k ∈ head✝ :: tail✝, j ≤ k
⊢ simplicialEvalσ (head✝ :: tail✝) j = j

Tactic:
| cons _ _ _ =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
ht : a✝ ∈ (fun K ↦ K.faces) (sSup x✝)
⊢ a✝ ∈ (fun K ↦ K.faces) L

Tactic:
cases ht with

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ x.subcomplex ≤ (y.cast ⋯).subcomplex

Tactic:
Subfunctor.ofSection_le_iff,

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ x.simplex ∈ (y.cast ⋯).subcomplex.obj (Opposite.op ⦋x.dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x : Fin (n + 3)
⊢ map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x

Tactic:
by
  obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
  · by_cases! hx : x ≤ i
    · rw [Fin.predAbove_of_le_castSucc _ _ (by simpa), Fin.castPred_castSucc]
      obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
      · simp only [map'_eq_castSucc_iff, OrderEmbedding.toOrderHom_coe,
          Fin.succAboveOrderEmb_apply, Fin.castSucc_le_castSucc_iff,
          Fin.castSucc_lt_castSucc_iff]
        constructor
        · obtain hx | rfl := hx.lt_or_eq
          · rwa [Fin.succAbove_of_castSucc_lt]
          · simpa only [Fin.succAbove_castSucc_self] using Fin.castSucc_le_succ x
        · intro j hj
          rwa [Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx),
            Fin.castSucc_lt_castSucc_iff]
      · obtain rfl : i = Fin.last _ := Fin.last_le_iff.1 hx
        simp [map'_eq_last_iff]
    · obtain ⟨x, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hx)
      rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa [Fin.le_castSucc_iff]),
        Fin.pred_castSucc_succ, map'_eq_castSucc_iff]
      simp only [Fin.succAbove_of_lt_succ _ _ hx,
        OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply,
        le_refl, Fin.castSucc_lt_castSucc_iff, true_and]
      intro j hj
      by_cases! h : j.castSucc < i
      · simpa [Fin.succAbove_of_castSucc_lt _ _ h] using hj.le
      · rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]
  · simp

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

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
⊢ ⟨↑(x.1 i) + ↑(x.2 i), ⋯⟩ ≤ ⟨↑(x.1 j) + ↑(x.2 j), ⋯⟩

Tactic:
simp only [Fin.mk_le_mk]

Goal state after:
p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(x.1 i) + ↑(x.2 i) ≤ ↑(x.1 j) + ↑(x.2 j)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
this✝ : Mono (yonedaEquiv.symm x)
this :
  (ConcreteCategory.hom (SimplicialObject.δ X i)) x =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
⊢ (ConcreteCategory.hom (SimplicialObject.δ X i)) x ∈ X.nonDegenerate n

Tactic:
this,

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
this✝ : Mono (yonedaEquiv.symm x)
this :
  (ConcreteCategory.hom (SimplicialObject.δ X i)) x =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) ∈
    X.nonDegenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ((↑s).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s).dim⦌)

Tactic:
exact s.val.notMem

Goal state after:
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : StrongEpi f
Z : C
p : X ⟶ Z
i : Z ⟶ Y
fac : p ≫ i = f
x✝ : Mono i
sq : CommSq p f i (𝟙 Y)
⊢ i ≫ sq.lift = 𝟙 Z

Tactic:
by simp [← cancel_mono i]

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

Goal state before:
pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (range (c.ιSigmaStdSimplex ≫ f.b i ≫ (f.filtration (Order.succ i)).ι)).obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x

Tactic:
obtain ⟨y, hy⟩ := hx

Goal state after:
case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hi : i ≤ i
y : Δ[c.dim + 1].obj d
hy : (ConcreteCategory.hom ((c.ιSigmaStdSimplex ≫ f.b i ≫ (f.filtration (Order.succ i)).ι).app d)) y = x
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: case refine_1.hK
X : SSet
inst✝ : X.Finite
⊢ HasCardinalLT (Arrow (Discrete X.N)) Cardinal.aleph0

pp: case inst
X : SSet
inst✝ : X.Finite
⊢ ∀ (k : Discrete X.N), IsCardinalPresentable ((Discrete.functor fun s ↦ Δ[s.dim]).obj k) Cardinal.aleph0

Tactic:
· exact hasCardinalLT_of_finite _ _ (by rfl)

Goal state after:
case inst
X : SSet
inst✝ : X.Finite
⊢ ∀ (k : Discrete X.N), IsCardinalPresentable ((Discrete.functor fun s ↦ Δ[s.dim]).obj k) Cardinal.aleph0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: case hK
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0

pp: case inst
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ ∀ (k : WalkingParallelPair),
    IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj k) Cardinal.aleph0

Tactic:
· exact hasCardinalLT_of_finite _ _ (by rfl)

Goal state after:
case inst
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ ∀ (k : WalkingParallelPair),
    IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj k) Cardinal.aleph0
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: 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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : l.l ≫ (G.obj (op Y₁)).map f₃ = adj₂.homEquiv (Arrow.Hom.right α)
⊢ adj₂.homEquiv.symm (l.l ≫ (G.obj (op Y₁)).map f₃) = Arrow.Hom.right α

Tactic:
this,

Goal state after:
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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : l.l ≫ (G.obj (op Y₁)).map f₃ = adj₂.homEquiv (Arrow.Hom.right α)
⊢ adj₂.homEquiv.symm (adj₂.homEquiv (Arrow.Hom.right α)) = Arrow.Hom.right α
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl.inr.refine_3
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
this : φ x hd (min x hd).succ = (objEquiv (x.cast hd).simplex) (min x hd)
⊢ (x.cast hd).simplex.1 i.succ = (φ x hd (min x hd).succ).1

Tactic:
this,

Goal state after:
case inl.inr.refine_3
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
this : φ x hd (min x hd).succ = (objEquiv (x.cast hd).simplex) (min x hd)
⊢ (x.cast hd).simplex.1 i.succ = ((objEquiv (x.cast hd).simplex) (min x hd)).1
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
hst :
  { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } =
    { dim := t.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.index.castSucc)) (t.x.cast ⋯).simplex }
⊢ False

Tactic:
by
    replace hst : s.x = t.isIndex.δ := by
      rwa [Subcomplex.N.ext_iff, N.ext_iff, ← s.x.cast_eq_self s.hd]
    have := t.isIndex.isType₂_δ
    rw [← hst] at this
    exact this _ _ _ s.isIndex

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

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
this : St = Finset.image it.succ.succAbove Sδ ∪ {it.succ}
⊢ St.card = Sδ.card + 1

Tactic:
this,

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
this : St = Finset.image it.succ.succAbove Sδ ∪ {it.succ}
⊢ (Finset.image it.succ.succAbove Sδ ∪ {it.succ}).card = Sδ.card + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplexHomeomorphI.symm 1 = stdSimplex.vertex 1

Tactic:
by
  simp [← TopCat.stdSimplexHomeomorphI_vertex_one]

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

Goal state before:
pp: ⊢ stdSimplex.δ 0 ≫ toSSetObjI = SSet.const (TopCat.toSSetObj₀Equiv.symm 1)

Tactic:
by
  dsimp only [toSSetObjI, toTopObjIsoI, TopCat.stdSimplexHomeomorphI]
  rw [← Adjunction.homEquiv_naturality_left, sSetTopAdj_homEquiv_stdSimplex_zero]
  congr 2
  have : stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo
      (((toTop.{u}.map (stdSimplex.δ 0)).hom) default)) = 1 := by
    rw [← stdSimplexHomeomorphUnitInterval_one]
    congr 1
    refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_
    rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]
    rfl
  exact congr_arg ULift.up.{u} this

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcⱼ : ∀ (j : ι), j ≠ i → Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)
this : w a⁻¹ < 1
⊢ Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))

Tactic:
simpa [c] using (tendsto_div_one_add_pow_nhds_one this).mul_const (w b)

Goal state after: