mathlib-initiative/mathlib-tactics huggingface dataset:
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
i : J.L
⊢ (Iso.refl ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)).pt).hom ≫ (c.map F).ι i =
    ι ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)) i

Tactic:
by dsimp only [Multifork.ι]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
⊢ ∀ (X₁ X₂ : T → Type u) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : T) → X₁ j ⟶ X₂ j),
    (∀ (j : T), monomorphisms (Type u) (f j)) → monomorphisms (Type u) (Limits.Sigma.map f)

Tactic:
intro X₁ X₂ _ _ f h
    simp only [monomorphisms.iff, mono_iff_injective] at h ⊢
    intro x₁ x₂ hx
    obtain ⟨i₁, x₁, rfl⟩ := Cofan.inj_jointly_surjective_of_isColimit
      (coproductIsCoproduct X₁) x₁
    obtain ⟨i₂, x₂, rfl⟩ := Cofan.inj_jointly_surjective_of_isColimit
      (coproductIsCoproduct X₁) x₂
    simp only [cofan_mk_inj] at hx ⊢
    replace hx : Sigma.ι X₂ i₁ (f i₁ x₁) = Sigma.ι X₂ i₂ (f i₂ x₂) := by
      have h₁ := congr_hom (Sigma.ι_map f i₁) x₁
      have h₂ := congr_hom (Sigma.ι_map f i₂) x₂
      simp only [comp_apply] at h₁ h₂ hx
      simpa [← h₁, ← h₂]
    obtain rfl := Cofan.eq_of_inj_apply_eq_of_isColimit (coproductIsCoproduct X₂) _ _ hx
    obtain rfl := h _ (Cofan.inj_injective_of_isColimit (coproductIsCoproduct X₂) i₁ hx)
    rfl

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

Goal state before:
pp: case succ
n : ℕ
inst✝ : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ J Λ[n + 1, i].ι

Tactic:
· simp only [J, iSup_iff]
    exact ⟨n, ⟨i⟩⟩

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

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

Tactic:
exact hf _ (horn_ι_mem_J _ _)

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

Goal state before:
pp: S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
⊢ ∃ σ, σ₀ = Λ[n + 2, i].ι ≫ σ

Tactic:
obtain ⟨σ, h⟩ := filler σ₀ h₀ hₙ

Goal state after:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
⊢ ∃ σ, σ₀ = Λ[n + 2, i].ι ≫ σ
Module: Mathlib.AlgebraicTopology.Quasicategory.Basic

Goal state before:
pp: S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
⊢ ∃ σ, σ₀ = Λ[n + 2, i].ι ≫ σ

Tactic:
refine ⟨yonedaEquiv.symm σ, ?_⟩

Goal state after:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
⊢ σ₀ = Λ[n + 2, i].ι ≫ yonedaEquiv.symm σ
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
⊢ IsIso φ

Tactic:
isIso_iff_bijective

Goal state after:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
⊢ Function.Bijective ⇑(ConcreteCategory.hom φ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
x : Y.obj (op n)
hx✝ : x ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨x, hx✝⟩ ∈ ⊤.obj (op n)
hx :
  x ∈ ((skeletonOfMono i) d).obj (op n) ∨
    ∃ i_1 ∈ Y.nonDegenerate d,
      (∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (i.app (op ⦋d⦌))) x = i_1) ∧ x ∈ (Subcomplex.ofSimplex i_1).obj (op n)
⊢ ⟨x, hx✝⟩ ∈ Set.range ⇑{ toFun := fun x ↦ ⟨↑x, ⋯⟩ } ∪ Set.range ⇑(ConcreteCategory.hom ((b i d).app (op n)))

Tactic:
obtain hx | ⟨y, hy₁, hy₂, f, rfl⟩ := hx

Goal state after:
case inl
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
x : Y.obj (op n)
hx✝ : x ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨x, hx✝⟩ ∈ ⊤.obj (op n)
hx : x ∈ ((skeletonOfMono i) d).obj (op n)
⊢ ⟨x, hx✝⟩ ∈ Set.range ⇑{ toFun := fun x ↦ ⟨↑x, ⋯⟩ } ∪ Set.range ⇑(ConcreteCategory.hom ((b i d).app (op n)))

case inr
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (i.app (op ⦋d⦌))) x = y
f : op ⦋d⦌ ⟶ op n
hx : (ConcreteCategory.hom (Y.map f)) y ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈ ⊤.obj (op n)
⊢ ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈
    Set.range ⇑{ toFun := fun x ↦ ⟨↑x, ⋯⟩ } ∪ Set.range ⇑(ConcreteCategory.hom ((b i d).app (op n)))
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) := ⋯
hlt : ksucc < j
⊢ ↑((horn.spineId i h₀ hₙ).arrow k.castSucc) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩

Tactic:
dsimp [horn.face, CosimplicialObject.δ]

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 =
    (ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op))
      ↑(yonedaEquiv (Subfunctor.lift (stdSimplex.map (SimplexCategory.δ j)) ⋯))
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.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) := ⋯
hgt : j < ksucc
⊢ ↑((horn.spineId i h₀ hₙ).arrow k.succ) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩

Tactic:
dsimp [horn.face, CosimplicialObject.δ]

Goal state after:
case h.inr.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
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ =
    (ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op))
      ↑(yonedaEquiv (Subfunctor.lift (stdSimplex.map (SimplexCategory.δ j)) ⋯))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i ≫ δ j).op)) (sx.spineToSimplex f) = f.arrow i.castSucc

Tactic:
rw [mkOfSucc_δ_lt h, spineToSimplex_arrow]

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
X X' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ eHomWhiskerRight V f Z = (eHomWhiskerRight V f Y ▷ Y ⟶[V] Z) ≫ eComp V X Y Z

Tactic:
dsimp [eHomWhiskerRight]
  rw [leftUnitor_inv_naturality_assoc, whisker_exchange_assoc]
  simp [e_assoc']

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
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : ForgetEnrichment W (TransportEnrichment F D)
⊢ eId W (ForgetEnrichment.to W X) = Functor.LaxMonoidal.ε F ≫ F.map (eId V (ForgetEnrichment.to W X))

Tactic:
TransportEnrichment.eId_eq

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : ForgetEnrichment W (TransportEnrichment F D)
⊢ Functor.LaxMonoidal.ε F ≫ F.map (eId V (ForgetEnrichment.to W X)) =
    Functor.LaxMonoidal.ε F ≫ F.map (eId V (ForgetEnrichment.to W X))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
h : x.as.as = y.as.as
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective
  obtain ⟨y, rfl⟩ := y.mk_surjective
  obtain rfl : x = y := h
  rfl

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
hfg : HomotopicR f g
⊢ HomotopicR g f

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

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : SimplexCategory
ha : a.len ≤ d
b : SimplexCategory
hb : b.len ≤ d
f : { obj := a, property := ha } ⟶ { obj := b, property := hb }
⊢ W f

Tactic:
induction a using SimplexCategory.rec with

Goal state after:
case mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
b : SimplexCategory
hb : b.len ≤ d
a : ℕ
ha : { len := a }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := b, property := hb }
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
K : AbstractSimplicialComplex ι
x✝ : Finset ι
ht : x✝ ∈ (fun K ↦ K.faces) ⊥
⊢ x✝ ∈ (fun K ↦ K.faces) K

Tactic:
obtain ⟨v, hv⟩ := ht
    exact hv ▸ K.singleton_mem v

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) ((SimplexCategory.Hom.toOrderHom (inr' x y)) i)) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inl' y z)) i)

Tactic:
have e₃ := inl'_eval (tensorObjOf x y) z <| Fin.cast (by simp +arith) <| i.natAdd (x.len + 1)

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) ((SimplexCategory.Hom.toOrderHom (inr' x y)) i)) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inl' y z)) i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsRegular
⊢ h.IsProper

Tactic:
rw [← isProper_pairing_iff]

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsRegular
⊢ h.pairing.IsProper
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
⊢ IsIso i

Tactic:
have sq : CommSq p f i (𝟙 Y) := { }
    exact ⟨sq.lift, by simp [← cancel_mono i], by simp⟩

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 ((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

Tactic:
ι_m,

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'.horn.ι ≫ x'.ιSigmaStdSimplex).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 ((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

Tactic:
ι_m,

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'.horn.ι ≫ x'.ιSigmaStdSimplex).app (op ⦋c.dim⦌))) ⟨y, hy'⟩ =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: 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
⊢ IsFinitelyPresentable X

Tactic:
have := Cardinal.fact_isRegular_aleph0.{u}

Goal state after:
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
⊢ IsFinitelyPresentable X
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ anodyneExtensions Λ[n, i].ι

Tactic:
by
  rw [anodyneExtensions_eq_llp_rlp]
  exact le_llp_rlp _ _ (modelCategoryQuillen.horn_ι_mem_J n i)

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

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

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

Tactic:
· have := l.fac_left
          dsimp at this ⊢
          simp only [Category.assoc, sq₁₃.π_fst, ← adj₂.homEquiv_naturality_one,
            arrowHomEquiv_apply_right_fst, Arrow.mk_left, ← this, sq₁₂.inr_ι_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
⊢ X.ιChainComplex x ≫ (chainComplexMap f R).f n = Y.ιChainComplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)

Tactic:
dsimp [chainComplexMap, chainComplexFunctor, ιChainComplex, Sigma.map',
    chainComplex, chainComplexFunctor]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
⊢ (Sigma.ι (fun x ↦ R) x ≫
      Sigma.desc fun a ↦ 𝟙 R ≫ Sigma.ι (fun x ↦ R) ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) a)) =
    Sigma.ι (fun x ↦ R) ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X : SSet
motive : X.π₀ → Prop
mk : ∀ (x : X _⦋0⦌), motive (π₀.mk x)
x : X.π₀
⊢ motive x

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective
  exact mk x

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

Goal state before:
pp: case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
k : Fin (m + 1)
hk : k.castSucc ≠ Fin.last (m + 1)
⊢ (pairing k.castSucc n).IsRegular

Tactic:
pairing_castSucc

Goal state after:
case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
k : Fin (m + 1)
hk : k.castSucc ≠ Fin.last (m + 1)
⊢ (pairingCore k n).pairing.IsRegular
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
n : ℕ
inst✝ : HasPullbacks C
X : C
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ Mono (((singularChainComplexFunctor C).obj X).map f)

Tactic:
dsimp [singularChainComplexFunctor, SSet.chainComplexFunctor]
    apply +allowSynthFailures Functor.map_mono
    apply +allowSynthFailures Functor.map_mono
    dsimp [SSet, SimplicialObject.whiskering, SimplicialObject]
    infer_instance

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

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddGroup E
inst✝³ : MulActionWithZero 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝²] s
h's : s.Nonempty
⊢ #↑s = #E

Tactic:
by
  rcases h's with ⟨x, hx⟩
  exact cardinal_eq_of_mem_nhds 𝕜 (hs.mem_nhds hx)

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall g p x p.radius
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
ε : ENNReal
hf : HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x ε
⊢ ∃ ε > 0, Metric.eball x ε ⊆ {x | (fun x ↦ f x = g x) x}

Tactic:
exact ⟨ε, hf.r_pos, hf.unique (hg.mono hf.r_pos hf.r_le)⟩

Goal state after: