mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
S : C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (cofibrations (Over S)).HasFactorization (trivialFibrations (Over S))

Tactic:
cofibrations_over_def,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
S : C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (cofibrations C).over.HasFactorization (trivialFibrations (Over S))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

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
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
j : J.R
⊢ F.map (c.ι (J.fst j)) ≫ (d.map F).fst j = F.map (c.ι (J.snd j)) ≫ (d.map F).snd j

Tactic:
dsimp
    rw [← F.map_comp, ← F.map_comp, condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

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
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
j : J.L
⊢ (d.map F).fst j ≫ F.map (c.π (J.fst j)) = (d.map F).snd j ≫ F.map (c.π (J.snd j))

Tactic:
dsimp
    rw [← F.map_comp, ← F.map_comp, condition]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
h : i ≠ j
⊢ stdSimplex.face {i}ᶜ ≤ ⨆ j_1, stdSimplex.face {↑j_1}ᶜ

Tactic:
exact le_iSup (fun (k : ({j}ᶜ : Set (Fin (n + 1)))) ↦ stdSimplex.face.{u} {k.1}ᶜ) ⟨i, h⟩

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

Goal state before:
pp: case «0»
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ¬(stdSimplex.edge n a b hab) ((fun i ↦ i) ⟨0, ⋯⟩) = k

Tactic:
exact Ne.symm hk.2.1

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ (stdSimplex.faceSingletonComplIso i).inv ≫ ι i = faceι i

Tactic:
by
  rw [← cancel_epi (stdSimplex.faceSingletonComplIso i).hom, Iso.hom_inv_id_assoc]
  rfl

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ 2 = n ∨ 2 < n

Tactic:
or_comm,

Goal state after:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ 2 < n ∨ 2 = n
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
⊢ Function.Injective ⇑(hom φ)

Tactic:
intro x₁ y₁ h

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
x₁ y₁ : c₁.pt
h : (hom φ) x₁ = (hom φ) y₁
⊢ x₁ = y₁
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht : Function.Injective ⇑(ConcreteCategory.hom t)
⊢ t ≫ r = l ≫ b ∧
    (∀ (x₁ y₁ : (fun X ↦ X) X₁),
        (ConcreteCategory.hom t) x₁ = (ConcreteCategory.hom t) y₁ ∧
            (ConcreteCategory.hom l) x₁ = (ConcreteCategory.hom l) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃),
        (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) x₃ →
          ∃ x₁, (ConcreteCategory.hom t) x₁ = x₂ ∧ (ConcreteCategory.hom l) x₁ = x₃

Tactic:
refine ⟨h.w, fun x₁ y₁ ⟨h₂, _⟩ ↦ ht h₂, fun x₂ x₃ hx ↦ ?_⟩

Goal state after:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht : Function.Injective ⇑(ConcreteCategory.hom t)
x₂ : (fun X ↦ X) X₂
x₃ : (fun X ↦ X) X₃
hx : (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) x₃
⊢ ∃ x₁, (ConcreteCategory.hom t) x₁ = x₂ ∧ (ConcreteCategory.hom l) x₁ = x₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
x : (MultispanShape.ofLinearOrder ↑{2}ᶜ).L
⊢ (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst x ≫
      match (MultispanShape.ofLinearOrder ↑{2}ᶜ).fst x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
        | 2, hi => ⋯.elim
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd x ≫
      match (MultispanShape.ofLinearOrder ↑{2}ᶜ).snd x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
        | 2, hi => ⋯.elim
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
by
      dsimp at x ⊢
      fin_cases x
      · dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 2 3 (by simp)).hom,
          ← Category.assoc]
        convert! h₂₃ <;> decide
      · dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 1 2 (by simp)).hom,
          ← Category.assoc]
        convert! h₁₂ <;> decide
      · dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 0 2 (by simp)).hom,
          ← Category.assoc]
        convert! h₀₂ <;> decide

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n✝ n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (spineToSimplex h (X.spine (n + 1) s)) =
    (ConcreteCategory.hom (SimplicialObject.δ X 0)) s

Tactic:
δ₀_spineToSimplex,

Goal state after:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n✝ n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
⊢ spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯) = (ConcreteCategory.hom (SimplicialObject.δ X 0)) s
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ ((α_ X Y Z).hom ≫ (α_ X Y Z).inv).f = 𝟙 ((X ⊗ Y) ⊗ Z).fst

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (𝟙 ((X ⊗ Y) ⊗ Z)).f = 𝟙 ((X ⊗ Y) ⊗ Z).fst
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (α_ X Y Z).inv.f = (α_ X.fst Y.fst Z.fst).inv

Tactic:
apply Iso.inv_ext' -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
  rw [← associator_hom_f, ← comp_f, Iso.hom_inv_id]; rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ ((λ_ X).hom ≫ (λ_ X).inv).f = 𝟙 (𝟙_ (Center C) ⊗ X).fst

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (𝟙 (𝟙_ (Center C) ⊗ X)).f = 𝟙 (𝟙_ (Center C) ⊗ X).fst
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ ((ρ_ X).hom ≫ (ρ_ X).inv).f = 𝟙 (X ⊗ 𝟙_ (Center C)).fst

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (𝟙 (X ⊗ 𝟙_ (Center C))).f = 𝟙 (X ⊗ 𝟙_ (Center C)).fst
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F G : FreeRefl V ⥤ D
h₁ : ∀ (v : V), F.obj (mk v) = G.obj (mk v)
h₂ : ∀ {v w : V} (f : v ⟶ w), F.map (homMk f) = eqToHom ⋯ ≫ G.map (homMk f) ≫ eqToHom ⋯
⊢ (quotientFunctor V ⋙ F).obj = (quotientFunctor V ⋙ G).obj

Tactic:
by ext; apply h₁

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

Goal state before:
pp: X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
z : SimplexCategoryGenRel
e : X✝ ⟶ z
m : z ⟶ Y✝
he : P_σ e
hm : P_δ m
fac : f = e ≫ m
⊢ Nonempty (P_σ.MapFactorizationData P_δ f)

Tactic:
exact ⟨⟨z, e, m, fac.symm, he, hm⟩⟩

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

Goal state before:
pp: case hᵥ
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)
⊢ (X.spine i
          ((ConcreteCategory.hom (X.map f.op))
            (sx.spineToSimplex
              { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
                arrow := fun i ↦
                  (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
                arrow_src := ⋯, arrow_tgt := ⋯ }))).vertex
      k =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)).vertex k

Tactic:
spine_map_vertex,

Goal state after:
case hᵥ
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)
⊢ (X.spine n
          (sx.spineToSimplex
            { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
              arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
              arrow_src := ⋯, arrow_tgt := ⋯ })).vertex
      ((Hom.toOrderHom f) k) =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)).vertex k
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
g : h.pairing.RankFunction α
x✝ y✝ : h.ι
hxy : h.AncestralRel x✝ y✝
⊢ g.rank (h.equivII x✝) < g.rank (h.equivII y✝)

Tactic:
rw [ancestralRel_iff] at hxy
        exact g.lt hxy

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
g : h.pairing.WeakRankFunction α
x✝ y✝ : h.ι
hxy : h.AncestralRel x✝ y✝
⊢ h.dim x✝ = h.dim y✝ → g.rank (h.equivII x✝) < g.rank (h.equivII y✝)

Tactic:
rw [ancestralRel_iff] at hxy
        exact g.lt hxy

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
x : Fin (n + 1)
hx : x ∈ Finset.univ
⊢ β (γ₄ x) = -β (γ₃ x)

Tactic:
by simp [h_succ_comp_δ_castSucc_succ, β, γ₃, γ₄]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable X κ
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
this : EssentiallySmall.{w, w, w} J
j : J
f : X ⟶ p.diag.obj j
hf : f ≫ { pt := X, ι := p.ι }.ι.app j = 𝟙 X
⊢ P.retractClosure X

Tactic:
exact ⟨_, p.prop_diag_obj j, ⟨{ i := _, r := _, retract := hf}⟩⟩

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

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
P₁ P₂ : Cᵒᵖ ⥤ A
i : P₁ ⟶ P₂
x✝ : Mono i
hi : ∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i
⊢ ∀ (X : Cᵒᵖ), IsIso (i.app X)

Tactic:
rintro ⟨X⟩

Goal state after:
A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
P₁ P₂ : Cᵒᵖ ⥤ A
i : P₁ ⟶ P₂
x✝ : Mono i
hi : ∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i
X : C
⊢ IsIso (i.app (op X))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ hx.simplex hd ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)

Tactic:
refine fun h ↦ (x.cast hd).notMem ?_
  rw [← hx.δ_simplex hd]
  exact (Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] ∂Δ[n]).map
    (SimplexCategory.δ (min x hd).castSucc).op h

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

Goal state before:
pp: X Y Z : SSet
s : Cofork (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ (ConcreteCategory.hom s.π) x₀ = (ConcreteCategory.hom s.π) x₁

Tactic:
simpa only [← e.src_eq, ← e.tgt_eq] using!
        ConcreteCategory.congr_hom s.condition e.edge

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

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₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (𝟭 C₃).map
        (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
          ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.map (Arrow.Hom.right sq)).app f₂.right)

Tactic:
apply PushoutObjObj.hom_ext
    all_goals simp [← NatTrans.comp_app, ← Functor.map_comp]

Goal state after:
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₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ sq₁₂.inl ≫
      (𝟭 C₃).map
          (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
            ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.obj f₁.right).map (Arrow.Hom.right sq))

Tactic:
simp [← map_comp]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
inst✝² : CommRing R
T : Type u_3
inst✝¹ : Field T
inst✝ : Algebra R T
w : AbsoluteValue T ℝ
r : R
⊢ UniformContinuous fun x ↦ r • x

Tactic:
simp_rw [Algebra.smul_def]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
inst✝² : CommRing R
T : Type u_3
inst✝¹ : Field T
inst✝ : Algebra R T
w : AbsoluteValue T ℝ
r : R
⊢ UniformContinuous fun x ↦ (algebraMap R (WithAbs w)) r * x
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
⊢ 𝔠 ≤ #𝕜

Tactic:
suffices ∃ f : (ℕ → Bool) → 𝕜, range f ⊆ univ ∧ Continuous f ∧ Injective f by
    rcases this with ⟨f, -, -, f_inj⟩
    simpa using lift_mk_le_lift_mk_of_injective f_inj

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
⊢ ∃ f, range f ⊆ Set.univ ∧ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Injective f
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
⊢ 0 < v a

Tactic:
by simp [ha₀]

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t : ℝ
⊢ ∀ ⦃j : ℝ⦄, t ≠ j → Function.onFun Disjoint (fun t ↦ [c + x -[ℝ] c + t • y] ∩ s) t j

Tactic:
t'

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
⊢ t ≠ t' → Function.onFun Disjoint (fun t ↦ [c + x -[ℝ] c + t • y] ∩ s) t t'
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t : ℝ
⊢ ∀ ⦃j : ℝ⦄, t ≠ j → Function.onFun Disjoint (fun t ↦ [c - x -[ℝ] c + t • y] ∩ s) t j

Tactic:
t'

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
⊢ t ≠ t' → Function.onFun Disjoint (fun t ↦ [c - x -[ℝ] c + t • y] ∩ s) t t'
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: n✝ : ℕ
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 := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
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
n : (SimplexCategory.Truncated 2)ᵒᵖ
⊢ X.obj n ⟶ Y.obj n

Tactic:
obtain ⟨⟨n⟩, hn⟩ := n
  match n with
  | 0 => exact ↾f₀
  | 1 => exact ↾f₁
  | 2 => exact ↾(f₂ f₀ f₁ hδ₁ hδ₀ hY)

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

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this✝ : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
hgt : 1 < (v u) (a w)⁻¹
this : Tendsto (fun n ↦ (v u) (1 / (1 + (a w)⁻¹ ^ n))) atTop (𝓝 0)
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a w)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v w)) (z w)))
    atTop (𝓝 0)

Tactic:
← WithAbs.norm_toAbs_eq

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this✝ : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
hgt : 1 < (v u) (a w)⁻¹
this : Tendsto (fun n ↦ ‖WithAbs.toAbs (v u) (1 / (1 + (a w)⁻¹ ^ n))‖) atTop (𝓝 0)
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a w)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v w)) (z w)))
    atTop (𝓝 0)