mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ k.castSucc < i.succ

Tactic:
by simpa

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc ≤ j.castSucc

Tactic:
by simpa

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

Goal state before:
pp: n : ℕ
⊢ Function.Injective toMk₁

Tactic:
intro i j h
  wlog hij : i < j generalizing i j
  · grind
  have := ConcreteCategory.congr_hom h ⟨i.1, lt_of_lt_of_le hij (by dsimp; lia)⟩
  simp [toMk₁_apply, if_pos hij] at this

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]

Goal state after:
α : Type u_1
a : α
inst✝ : Preorder α
c x✝ : α
b : a ≤ x✝ ∧ x✝ ≤ c
⊢ ∀ ⦃b : α⦄, x✝ ≤ b → b ≤ c → a ≤ b
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
i : Fin (n + 1)
this : x ≤ (f i).castSucc
⊢ i.castSucc ∈ finset f x

Tactic:
by simpa

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ b ∈ finset f x, y.castSucc ≤ b
i : Fin (n + 1)
hi : i < y
this : x ≤ (f i).castSucc
⊢ i.castSucc ∈ finset f x

Tactic:
by simpa

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

Goal state before:
pp: n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 2)
⊢ map' f (map' g x) = map' (g.comp f) x

Tactic:
by
  obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x
  · obtain ⟨y, hy⟩ | hx := Fin.eq_castSucc_or_eq_last (map' g x.castSucc)
    · rw [hy]
      rw [map'_eq_castSucc_iff] at hy
      obtain ⟨z, hz⟩ | hz := Fin.eq_castSucc_or_eq_last (map' f y.castSucc)
      · rw [hz, Eq.comm]
        rw [map'_eq_castSucc_iff] at hz ⊢
        constructor
        · refine hy.1.trans ?_
          simp only [OrderHom.comp_coe, Function.comp_apply, Fin.castSucc_le_castSucc_iff]
          exact g.monotone (by simpa using hz.1)
        · intro i hi
          exact hy.2 (f i) (by simpa using hz.2 i hi)
      · rw [hz, Eq.comm]
        rw [map'_eq_last_iff] at hz ⊢
        intro i
        exact hy.2 (f i) (by simpa using hz i)
    · rw [Eq.comm, hx, map'_last]
      rw [map'_eq_last_iff] at hx ⊢
      intro i
      apply hx
  · simp

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

Goal state before:
pp: n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ x.castSucc ≤ i.castSucc

Tactic:
by simpa

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
⊢ j.castSucc < x.castSucc

Tactic:
by simpa

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

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ i.succ.castSucc ≤ x.castSucc.castSucc

Tactic:
by simpa

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

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc.castSucc < i.succ.castSucc

Tactic:
by simpa

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

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc ≤ i.castSucc

Tactic:
by simpa

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

Goal state before:
pp: X₁ X₂ X₃ X₄ : SSet
inst✝¹ : X₁.Finite
inst✝ : X₂.Finite
⊢ (X₁ ⊗ X₂).Finite

Tactic:
by
  obtain ⟨d₁, _⟩ := X₁.hasDimensionLT_of_finite
  obtain ⟨d₂, _⟩ := X₂.hasDimensionLT_of_finite
  exact finite_of_hasDimensionLT _ (d₁ + d₂) (fun _ _ ↦ inferInstance)

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim + 1⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim + 1⦌)
hy :
  (ConcreteCategory.hom ((f.m j).app (op ⦋c.dim + 1⦌)))
      ((ConcreteCategory.hom (x'.ιSigmaHorn.app (op ⦋c.dim + 1⦌))) ⟨y, hy'⟩) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌))))
⊢ False

Tactic:
← NatTrans.comp_app_apply,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim + 1⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim + 1⦌)
hy :
  (ConcreteCategory.hom ((x'.ιSigmaHorn ≫ f.m j).app (op ⦋c.dim + 1⦌))) ⟨y, hy'⟩ =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌))))
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim⦌)
hy :
  (ConcreteCategory.hom ((f.m j).app (op ⦋c.dim⦌))) ((ConcreteCategory.hom (x'.ιSigmaHorn.app (op ⦋c.dim⦌))) ⟨y, hy'⟩) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
⊢ False

Tactic:
← NatTrans.comp_app_apply,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim⦌)
hy :
  (ConcreteCategory.hom ((x'.ιSigmaHorn ≫ f.m j).app (op ⦋c.dim⦌))) ⟨y, hy'⟩ =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
⊢ False
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) κ
this : ∀ (k : Kᵒᵖ), ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ
⊢ HasCardinalLT (Arrow Kᵒᵖ) κ

Tactic:
by simpa

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

Goal state before:
pp: case inl.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₁ f c')
⊢ Cell.type₁ f c = Cell.type₁ f c'

Tactic:
simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h

Goal state after:
case inl.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : P.p c.s = P.p c'.s
⊢ Cell.type₁ f c = Cell.type₁ f c'
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₂ f c')
⊢ Cell.type₁ f c = Cell.type₂ f c'

Tactic:
simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h

Goal state after:
case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : ↑(P.p c.s) = ↑c'.s
⊢ Cell.type₁ f c = Cell.type₂ f c'
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₁ f c')
⊢ Cell.type₂ f c = Cell.type₁ f c'

Tactic:
simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h

Goal state after:
case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : ↑c.s = ↑(P.p c'.s)
⊢ Cell.type₂ f c = Cell.type₁ f c'
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 ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₂ f c')
⊢ Cell.type₂ f c = Cell.type₂ f c'

Tactic:
simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h

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 ι
j : ι
c c' : f.Cell j
h : c.s = c'.s
⊢ Cell.type₂ f c = Cell.type₂ f c'
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
this : IsCardinalPresentable G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ (f₁ ≫ Φ.map (IsFiltered.leftToMax j₁ j₂)) ≫ colimit.ι Φ (IsFiltered.max j₁ j₂) = g₁

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
this : IsCardinalPresentable G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ (f₂ ≫ Φ.map (IsFiltered.rightToMax j₁ j₂)) ≫ colimit.ι Φ (IsFiltered.max j₁ j₂) = g₂

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
Q : C
⊢ f ▷ Q ≫ pushout.inl f g ▷ Q = g ▷ Q ≫ pushout.inr f g ▷ Q

Tactic:
by
  simp [← comp_whiskerRight, pushout.condition]

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

Goal state before:
pp: case refine_1
X : SSet
x✝ : IsEmpty (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
this : IsEmpty ((fun X ↦ X) (X _⦋n⦌))
⊢ X.degenerate n = ⊤

Tactic:
subsingleton

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
inst✝ : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
y : X.π₀
⊢ x = y

Tactic:
subsingleton

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

Goal state before:
pp: p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ j.castSucc < i.castSucc.succ

Tactic:
by simpa

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

Goal state before:
pp: p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ ≤ j.castSucc

Tactic:
by simpa

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.degenerate (n + 1)
⊢ X.ιChainComplex x ≫ PInfty.f (n + 1) = 0

Tactic:
simp only [degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
hx : ∃ i y, (ConcreteCategory.hom (SimplicialObject.σ X i)) y = x
⊢ X.ιChainComplex x ≫ PInfty.f (n + 1) = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

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₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝ : Arrow C₂
⊢ Arrow.Hom.left
      ((F.leibnizPushout.obj X₁).map
          ({
                app := fun X₂ ↦
                  Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                    (pullback.lift
                      (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                      (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯)
                    ⋯,
                naturality := ⋯ }.app
            x✝) ≫
        {
              app := fun X₃ ↦
                Arrow.homMk
                  (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj X₃).left))
                    (adj₂.homEquiv.symm
                      (pullback.fst ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                        ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                    ⋯)
                  (adj₂.homEquiv.symm
                    (pullback.snd ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                      ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                  ⋯,
              naturality := ⋯ }.app
          ((F.leibnizPushout.obj X₁).obj x✝)) =
    Arrow.Hom.left (𝟙 ((F.leibnizPushout.obj X₁).obj x✝))

Tactic:
apply pushout.hom_ext <;> simp [← homEquiv_symm_naturality_two, ofHasPushout_pt]

Goal state after:
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 : i ≤ j
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ i.castSucc.castSucc < j.castSucc.succ

Tactic:
by simpa

Goal state after:
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
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ j.castSucc.succ ≤ i.succ.castSucc

Tactic:
by simpa

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 : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ stdSimplex.δ k ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = const x

Tactic:
rw [stdSimplex.δ_comp_yonedaEquiv_symm, δ_opObjEquiv,
      ← stdSimplex.yonedaEquiv_δ_comp, h.δ_map_of_gt _ (by grind)]

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (const (opObjEquiv.symm x)))) = const x
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
x✝ : C(↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))), ↑X)
⊢ (fun x ↦ { toFun := fun x_1 ↦ x, continuous_toFun := ⋯ }) ((fun f ↦ f.toFun default) x✝) = x✝

Tactic:
ext x
        obtain rfl := Subsingleton.elim x default
        rfl

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

Goal state before:
pp: X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
⊢ TopCat.toSSetObj₀Equiv (SSet.yonedaEquiv (sSetTopAdj.unit.app Δ[0])) =
    TopCat.toSSetObj₀Equiv (SSet.yonedaEquiv (SSet.const (TopCat.toSSetObj₀Equiv.symm default)))

Tactic:
subsingleton

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun x ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
this : #↑(ULift.down ⁻¹' t) ≤ lift.{v, u} a
⊢ #↑t ≤ a

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
n : ℕ
hc : 1 < 0
⊢ False

Tactic:
exact lt_irrefl _ (hc.trans zero_lt_one)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 (0 • x))

Tactic:
have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) := by
        simp_rw [← inv_pow]
        apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one
        rw [norm_inv]
        exact inv_lt_one_of_one_lt₀ hc

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 (0 • x))
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ 1 < v x ↔ 1 < w x

Tactic:
simpa only [map_one] using h.lt_iff_lt (x := 1)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Field R
inst✝⁴ : Semifield S
inst✝³ : LinearOrder S
v w : AbsoluteValue R S
inst✝² : IsStrictOrderedRing S
inst✝¹ : Archimedean S
inst✝ : ExistsAddOfLE S
hv✝ : v.IsNontrivial
h : ∀ (x : R), v x < 1 → w x < 1
a : R
ha₀ : a ≠ 0
hw : w a < 1
x₀ : R
hx₀ : x₀ ≠ 0 ∧ v x₀ < 1
n : ℕ
hv : 1 ≤ v a
⊢ w x₀ < w a ^ n

Tactic:
rw [← one_mul (_ ^ _), ← mul_inv_lt_iff₀ (pow_pos (by simp_all) _),
      ← map_pow, ← map_inv₀, ← map_mul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Field R
inst✝⁴ : Semifield S
inst✝³ : LinearOrder S
v w : AbsoluteValue R S
inst✝² : IsStrictOrderedRing S
inst✝¹ : Archimedean S
inst✝ : ExistsAddOfLE S
hv✝ : v.IsNontrivial
h : ∀ (x : R), v x < 1 → w x < 1
a : R
ha₀ : a ≠ 0
hw : w a < 1
x₀ : R
hx₀ : x₀ ≠ 0 ∧ v x₀ < 1
n : ℕ
hv : 1 ≤ v a
⊢ w (x₀ * (a ^ n)⁻¹) < 1
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : 0 < r
⊢ (ball x r).Nonempty

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ≥0∞
hr : 0 < r
⊢ x ∈ eball x r

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ (closedBall x r).Nonempty

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ x ∈ closedBall x r

Tactic:
by simpa

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
this :
  ∀ {a : F},
    a ≠ 0 → v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → False
ha : v a ≤ 1
⊢ v a⁻¹ ≠ 1

Tactic:
by simpa

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
this :
  ∀ {a : F},
    a ≠ 0 → v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → False
ha : v a ≤ 1
⊢ log (v b) / log (w b) ≠ log (v a⁻¹) / log (w a⁻¹)

Tactic:
by simpa

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
this :
  ∀ {a : F},
    a ≠ 0 →
      v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → 1 < v b → False
hb : v b ≤ 1
⊢ v b⁻¹ ≠ 1

Tactic:
by simpa

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
this :
  ∀ {a : F},
    a ≠ 0 →
      v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → 1 < v b → False
hb : v b ≤ 1
⊢ log (v b⁻¹) / log (w b⁻¹) ≠ log (v a) / log (w a)

Tactic:
by simpa

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

Goal state before:
pp: 𝕜 : 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
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • 0 z

Tactic:
by simpa

Goal state after: