mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) x₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))

pp: case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝))

pp: case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝))

Tactic:
· have h₀ : Rel f g _ _ := Rel.inl_inr x₀
      rw [Quot.sound h₀, h]
      symm
      apply Quot.sound
      apply Rel.inl_inr

Goal state after:
case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝))

case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex

Goal state before:
pp: S : SSet
inst✝ : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[n + 1, i].ι ≫ σ

Tactic:
have sq' : CommSq σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from _) := ⟨by simp⟩
  exact ⟨sq'.lift, by simp⟩

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₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂ →
    (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂

Tactic:
apply pushoutCocone_inl_eq_inr_imp_of_iso e

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

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x₁ x₂ : sigmaStdSimplex i d _⦋n⦌
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨c₁, f₁, _, rfl⟩ := isPushout_aux x₁ hx₁

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

Goal state before:
pp: case h.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
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc = stdSimplex.objEquiv.symm (mkOfSucc k ≫ SimplexCategory.δ j)

Tactic:
mkOfSucc_δ_lt hlt

Goal state after:
case h.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
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc = stdSimplex.objEquiv.symm (mkOfSucc k.castSucc)
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝⁵ : Category.{v', u'} V
inst✝⁴ : MonoidalCategory V
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : EnrichedOrdinaryCategory V C
D : Type u''
inst✝¹ : Category.{v'', u''} D
inst✝ : EnrichedOrdinaryCategory V D
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ homOf V ((eHomEquiv V) (f ≫ g)) = homOf V ((eHomEquiv V) f) ≫ homOf V ((eHomEquiv V) g)

Tactic:
by simp [eHomEquiv_comp]

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

Goal state before:
pp: V : Type u'
inst✝⁵ : Category.{v', u'} V
inst✝⁴ : MonoidalCategory V
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : EnrichedOrdinaryCategory V C
D : Type u''
inst✝¹ : Category.{v'', u''} D
inst✝ : EnrichedOrdinaryCategory V D
X Y Z : ForgetEnrichment V D
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) ((eHomEquiv V).symm (homTo V (f ≫ g))) =
    (eHomEquiv V) ((eHomEquiv V).symm (homTo V f) ≫ (eHomEquiv V).symm (homTo V g))

Tactic:
by simp [eHomEquiv_comp]

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
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
α β : F ⟶ G
h : ∀ (X : C), α.out.app X = β.out.app X
⊢ α = β

Tactic:
rcases α with ⟨α⟩
  rcases β with ⟨β⟩
  congr
  ext
  apply h

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₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ (X.fst ◁ f.f) ▷ U ≫ ((X.tensorObj Y₂).snd.β U).hom = ((X.tensorObj Y₁).snd.β U).hom ≫ U ◁ X.fst ◁ f.f

Tactic:
dsimp only [tensorObj_fst, tensorObj_snd_β, Iso.trans_hom, whiskerLeftIso_hom,
    Iso.symm_hom, whiskerRightIso_hom]
  calc
    _ = 𝟙 _ ⊗≫
      X.fst ◁ (f.f ▷ U ≫ (HalfBraiding.β Y₂.snd U).hom) ⊗≫
        (HalfBraiding.β X.snd U).hom ▷ Y₂.fst ⊗≫ 𝟙 _ := by monoidal
    _ = 𝟙 _ ⊗≫
      X.fst ◁ (HalfBraiding.β Y₁.snd U).hom ⊗≫
        ((X.fst ⊗ U) ◁ f.f ≫ (HalfBraiding.β X.snd U).hom ▷ Y₂.fst) ⊗≫ 𝟙 _ := by
      rw [f.comm]; monoidal
    _ = _ := by rw [whisker_exchange]; monoidal

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
inst✝ : X.IsCoskeletal n
⊢ CostructuredArrow.IsUniversal (rightExtensionInclusion X n)

Tactic:
by
  apply Functor.isUniversalOfIsRightKanExtension

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

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝ : Category.{u, u} C
F G : X ⟶ (truncation 2).obj (nerve C)
h : map F = map G
f : X.obj (op { obj := ⦋1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom (F.app (op { obj := ⦋1⦌, property := ⋯ }))) f =
    (ConcreteCategory.hom (G.app (op { obj := ⦋1⦌, property := ⋯ }))) f

Tactic:
obtain ⟨x₀, x₁, f, rfl⟩ := Truncated.Edge.exists_of_simplex f

Goal state after:
X : Truncated 2
C : Type u
inst✝ : Category.{u, u} C
F G : X ⟶ (truncation 2).obj (nerve C)
h : map F = map G
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })
f : Truncated.Edge x₀ x₁
⊢ (ConcreteCategory.hom (F.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom (G.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case cast
n : ℕ
i✝ : Fin (n + 1)
⊢ δ i✝.castSucc ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) i✝.castSucc = 𝟙 (mk n)

Tactic:
· simp only [Fin.lastCases_castSucc]
      exact δ_comp_σ_self

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

Goal state before:
pp: case succ.comp_of.inr.inr
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
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain ⟨z, e, m, he, hm, fac⟩ := hn j f hf
          exact ⟨z, e, m ≫ δ j', he, P_δ.comp_mem _ _ hm (P_δ.δ j'),
            by simp [h'', reassoc_of% fac]⟩

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.succ)) k

Tactic:
dsimp
    rw [toMk₁_of_castSucc_lt i.succ k (by simpa), toMk₁_of_castSucc_lt]
    by_cases hk' : j.castSucc < k
    · rwa [Fin.predAbove_of_castSucc_lt _ _ hk', Fin.castSucc_pred_lt_iff]
    · simp only [not_lt] at hk'
      rw [Fin.predAbove_of_le_castSucc _ _ hk']
      exact lt_of_le_of_lt (by simpa) h

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
c x✝ : α
b : x✝ ∈ Icc a c
⊢ (fun x ↦ x ≤ c) x✝ ∧ ∀ ⦃b : α⦄, x✝ ≤ b → (fun x ↦ x ≤ c) b → b ∈ Icc a c

Tactic:
simp_all only [mem_Icc, and_true, true_and]
  exact fun _ x _ ↦ b.1.trans x

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:
by exact k

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

Goal state before:
pp: case neg
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ i.predAbove j < x

Tactic:
Fin.predAbove_of_le_castSucc _ _ h,

Goal state after:
case neg
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ j.castPred ⋯ < x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : j ≤ i.castSucc
⊢ i.predAbove j < x

Tactic:
Fin.predAbove_of_le_castSucc _ _ h,

Goal state after:
case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : j ≤ i.castSucc
⊢ j.castPred ⋯ < x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁ y₁ z₁ x₂ y₂ z₂ : AugmentedSimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
g₁ : y₁ ⟶ z₁
g₂ : y₂ ⟶ z₂
⊢ (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
by
  cat_disch

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
⊢ ∃ s, x = h.type₁ s ∨ x = h.type₂ s

Tactic:
obtain ⟨s, _ | _⟩ := h.surjective' x
  · exact ⟨s, Or.inl (by rwa [N.ext_iff, SSet.N.ext_iff])⟩
  · exact ⟨s, Or.inr (by rwa [N.ext_iff, SSet.N.ext_iff])⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
⊢ ∃ s, x = h.type₁ s ∨ x = h.type₂ s

Tactic:
by
  obtain ⟨s, _ | _⟩ := h.surjective' x
  · exact ⟨s, Or.inl (by rwa [N.ext_iff, SSet.N.ext_iff])⟩
  · exact ⟨s, Or.inr (by rwa [N.ext_iff, SSet.N.ext_iff])⟩

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Surjective h.functor.mapArrow.obj

Tactic:
rintro ⟨X, Y, f⟩

Goal state after:
case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X Y : C
f : (𝟭 C).obj X ⟶ (𝟭 C).obj Y
⊢ ∃ a, h.functor.mapArrow.obj a = { left := X, right := Y, hom := f }
Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
hY : F.DenseAt Y
⊢ F.isDenseAt.IsClosedUnderIsomorphisms

Tactic:
rw [isDenseAt_eq_isPointwiseLeftKanExtensionAt]
  infer_instance

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 : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

Tactic:
by_cases hx : IsType₂ x

Goal state after:
case pos
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : ¬IsType₂ x
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }
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 : ℕ
⊢ ∀ {x y : (pairingCore k n).ι},
    (pairingCore k n).AncestralRel x y →
      (pairingCore k n).dim x = (pairingCore k n).dim y → (finset x.x ⋯).card < (finset y.x ⋯).card

Tactic:
intro ⟨s, d, hds, is, hs⟩ ⟨t, d', hdt, it, ht⟩ ⟨h₁, h₂⟩ h₃

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
s : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hds : s.dim = d + 1
is : Fin (d + 1)
hs : IsIndex s hds is.succ
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hdt : t.dim = d' + 1
it : Fin (d' + 1)
ht : IsIndex t hdt it.succ
h₁ :
  { x := s, d := d, hd := hds, index := is, isIndex := hs } ≠ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₂ :
  (pairingCore k n).type₂ { x := s, d := d, hd := hds, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₃ :
  (pairingCore k n).dim { x := s, d := d, hd := hds, index := is, isIndex := hs } =
    (pairingCore k n).dim { x := t, d := d', hd := hdt, index := it, isIndex := ht }
⊢ (finset { x := s, d := d, hd := hds, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := t, d := d', hd := hdt, index := it, isIndex := ht }.x ⋯).card
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
⊢ (ConcreteCategory.hom (SimplicialObject.δ Δ[1] j)) (objMk₁ i) = objMk₁ (i.pred ⋯)

Tactic:
by
  ext k : 1
  exact ConcreteCategory.congr_hom (SimplexCategory.δ_comp_toMk₁_of_lt _ _ h) k

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

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

pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ j.succ)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc)) (stdSimplex.objMk₁ j.castSucc.succ.succ)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
          stdSimplex.objMk₁ j.castSucc.succ).2
      k

Tactic:
· simpa [stdSimplex.δ_objEquiv_symm_apply,
        SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}] using!
          ConcreteCategory.congr_hom (X.δ_comp_σ_of_le hij) x

Goal state after:
case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ j.succ)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc)) (stdSimplex.objMk₁ j.castSucc.succ.succ)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
          stdSimplex.objMk₁ j.castSucc.succ).2
      k
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case snd.h
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc ≤ j.castSucc.succ

Tactic:
← Fin.castSucc_succ

Goal state after:
case snd.h
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc ≤ j.succ.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j)) ≫
      σ Y i.succ =
    σ X i ≫
      ↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j.castSucc)

Tactic:
by
    ext x
    simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.σ_naturality_apply]
    dsimp
    apply congr_arg
    ext k : 2
    · simp [← SimplexCategory.σ_comp_σ hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]
      rfl
    · rw [stdSimplex.σ_objMk₁_of_le _ _ (by simpa)]
      rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ stdSimplex.δ k ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = const (opObjEquiv.symm x)

Tactic:
simp [stdSimplex.δ_comp_yonedaEquiv_symm, ← stdSimplex.yonedaEquiv_δ_comp,
      opObjEquiv_symm_yonedaEquiv_const, h.δ_map_of_lt k.rev (by grind)]

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularSet

Goal state before:
pp: S : SSet
m : SimplexCategoryᵒᵖ
a : S.obj m
⊢ ((ConcreteCategory.hom ((sSetTopAdj.unit.app S).app m)) a).down =
    SSet.toTopSimplex.inv.app (Opposite.unop m) ≫ SSet.toTop.map (SSet.yonedaEquiv.symm a)

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
R : Type u_3
T : Type u_4
inst✝² : Semiring R
v : AbsoluteValue R S
inst✝¹ : SMul T R
inst✝ : FaithfulSMul T R
m₁✝ m₂✝ : T
h : ∀ (a : WithAbs v), m₁✝ • a.ofAbs = m₂✝ • a.ofAbs
⊢ m₁✝ = m₂✝

Tactic:
exact FaithfulSMul.eq_of_smul_eq_smul fun _ ↦ h (toAbs v _)

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

Goal state before:
pp: X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x) =
    (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x)

Tactic:
apply (hY.spineEquiv 2).injective
  ext i
  fin_cases i
  · dsimp
    rw [spineEquiv_f₂_arrow_zero]
    dsimp [StrictSegal.spineEquiv]
    rw [← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_zero, op_comp,
      Functor.map_comp_apply, hσ, SimplexCategory.mkOfSucc_zero_eq_δ,
      ← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_zero,
      op_comp, Functor.map_comp_apply, hδ₁]
  · dsimp
    rw [spineEquiv_f₂_arrow_one]
    simp [StrictSegal.spineEquiv, SimplexCategory.mkOfSucc_one_eq_δ,
      ← Functor.map_comp_apply, ← op_comp]

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case hbc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
n : ℕ
w : E
hw : dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ 0 ≤ (↑c * ↑f'symm.nnnorm) ^ n

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
⊢ ↑n ≤ ↑⋯.choose ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
obtain ⟨g, hg, hg_ne, hm⟩ := (hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h).choose_spec

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
⊢ ↑n ≤ ↑⋯.choose ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z