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

Goal state before:
pp: case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i : J
⊢ ∀ (j : J) (xi : (fun X ↦ X) ((F ⋙ functorToTypes).obj i)) (xj : (fun X ↦ X) ((F ⋙ functorToTypes).obj j)),
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi =
        (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) xi = (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) xj

Tactic:
j

Goal state after:
case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i j : J
⊢ ∀ (xi : (fun X ↦ X) ((F ⋙ functorToTypes).obj i)) (xj : (fun X ↦ X) ((F ⋙ functorToTypes).obj j)),
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi =
        (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) xi = (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) xj
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

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

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

Goal state after:
n : ℕ
i : Fin (n + 2)
⊢ ι i = (stdSimplex.faceSingletonComplIso i).hom ≫ faceι i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ (skeletonOfMono i) 0 = Subcomplex.range i

Tactic:
simp [skeletonOfMono]

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ ((skeletonOfMono i) n).obj (op ⦋d⦌) = ⊤

Tactic:
← top_le_iff,

Goal state after:
X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ ⊤ ⊆ ((skeletonOfMono i) n).obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton (n + 1) ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

pp: case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton (n + 1)

Tactic:
· simp only [sup_le_iff, iSup_le_iff, skeleton_succ]
    refine ⟨le_sup_left.trans le_sup_left,
      le_sup_right.trans le_sup_left, fun x ↦ ?_⟩
    by_cases hx : x.1 ∈ (Subcomplex.range i).obj _
    · exact le_trans (le_trans (by simpa) le_sup_left) le_sup_left
    · exact (le_trans (by exact le_trans (by rfl) (le_iSup _ hx))
        (le_iSup _ x)).trans le_sup_right

Goal state after:
case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsColimit (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.mapCocone (PushoutCocone.mk (r i d) (b i d) ⋯))

Tactic:
refine (isColimitMapCoconePushoutCoconeEquiv _ _).2
      (IsPushout.isColimit ?_)
    refine Types.isPushout_of_isPullback_of_mono' ?_ ?_ ?_
    · exact (isPullback i d).map ((evaluation _ _).obj _)
    · exact range_r_app_union_range_b_app _ _ _
    · dsimp
      intro x₁ x₂ hx₁ hx₂ h
      obtain ⟨c₁, f₁, _, rfl⟩ := isPushout_aux x₁ hx₁
      obtain ⟨c₂, f₂, _, rfl⟩ := isPushout_aux x₂ hx₂
      rw [Subtype.ext_iff] at h
      replace h : Y.map f₁.op c₁.simplex = Y.map f₂.op c₂.simplex := by
        rwa [← c₁.b_app_ι_app_objEquiv_symm_val f₁, ← c₂.b_app_ι_app_objEquiv_symm_val f₂]
      obtain rfl : c₁ = c₂ := by
        ext
        exact Subtype.ext_iff.mp
          (Y.unique_nonDegenerate_simplex _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
            f₂ ⟨_, c₂.nonDegenerate⟩ h)
      obtain rfl : f₁ = f₂ :=
        Y.unique_nonDegenerate_map _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
          f₂ ⟨_, c₁.nonDegenerate⟩ 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 h : Edge x y
hfg : HomotopicL f g
hgh : HomotopicL g h
⊢ HomotopicL f h

Tactic:
by
  rcases hfg with ⟨hfg⟩
  rcases hgh with ⟨hgh⟩
  exact Quasicategory₂.fill32 hfg (idComp (id y)) hgh

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

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

Tactic:
j

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Tactic:
by
  apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.δ_comp_δ H

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

Goal state before:
pp: case inr.inl
n : ℕ
i : Fin (n + 2)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.castSucc ≫ σ i = σ j ≫ δ j'

Tactic:
exact Or.inl δ_comp_σ_self

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

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
⊢ W = ⊤

Tactic:
have hW (d : ℕ) : W.inverseImage (Truncated.inclusion d) = ⊤ :=
    Truncated.morphismProperty_eq_top _ (fun _ _ i ↦ δ_mem i)
      (fun _ _ i ↦ σ_mem i)

Goal state after:
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
⊢ W = ⊤
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
⊢ (fun j ↦ if j.castSucc < i then 0 else 1) j₁ ≤ (fun j ↦ if j.castSucc < i then 0 else 1) j₂

Tactic:
by
        dsimp
        split_ifs <;> grind

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ ∀ ⦃a₂ : Fin (n + 2)⦄, toMk₁ i = toMk₁ a₂ → i = a₂

Tactic:
j

Goal state after:
n : ℕ
i j : Fin (n + 2)
⊢ toMk₁ i = toMk₁ j → i = j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
h : WithInitial.of x = WithInitial.of y
⊢ x.len = y.len

Tactic:
injection h with h

Goal state after:
x y : SimplexCategory
h : x = y
⊢ x.len = y.len
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
⊢ ∀ k ∈ ⇑f '' I.I, k ≤ { as := f j.as }.as

Tactic:
rintro _ ⟨k, hk, rfl⟩; exact f.monotone (I.le_right k hk)

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

Goal state before:
pp: case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ ∀ i_1 < x, i.succAbove i_1 < x.castSucc

Tactic:
· intro j hj
          rwa [Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx),
            Fin.castSucc_lt_castSucc_iff]

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

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
i : Δ[n] _⦋k⦌
⊢ ∀ ⦃a₂ : Δ[n] _⦋k⦌⦄,
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) i =
        (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) a₂ →
      i = a₂

Tactic:
j

Goal state after:
X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) i =
      (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) j →
    i = j
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ ↑⟨↑(z.1 a) + ↑(z.2 a), ⋯⟩ = ↑⟨↑(z.1 b) + ↑(z.2 b), ⋯⟩

Tactic:
change ((objEquiv z a).1 : ℕ) + (objEquiv z a).2 = (objEquiv z b).1 + (objEquiv z b).2

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ ↑((objEquiv z) a).1 + ↑((objEquiv z) a).2 = ↑((objEquiv z) b).1 + ↑((objEquiv z) b).2
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X✝ Y✝ Z✝ : ↑h.smallCategoryOfSet.obj
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ h.homEquiv (x✝¹ ≫ x✝) = h.homEquiv x✝¹ ≫ h.homEquiv x✝

Tactic:
SmallCategoryOfSet.comp_def

Goal state after:
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X✝ Y✝ Z✝ : ↑h.smallCategoryOfSet.obj
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ h.homEquiv (h.smallCategoryOfSet.comp x✝¹ x✝) = h.homEquiv x✝¹ ≫ h.homEquiv x✝
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
⊢ ∀ ⦃X Y_1 : Cᵒᵖ⦄ (f : X ⟶ Y_1),
    (((restrictedULiftYoneda F).obj Y).map f ≫
        match Y_1 with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) =
      (match X with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) ≫
        ((restrictedULiftYoneda F).obj s.pt).map f

Tactic:
by
          rintro ⟨X₁⟩ ⟨X₂⟩ ⟨f⟩
          ext ⟨x⟩
          let α : CostructuredArrow.mk (F.map f ≫ x) ⟶ CostructuredArrow.mk x :=
            CostructuredArrow.homMk f
          exact ULift.down_injective (s.w α).symm

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

Goal state before:
pp: A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
P : ObjectProperty A
w✝ : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
⊢ (ObjectProperty.ofObj fun T ↦ freeYoneda T.1 ↑T.2) ≤ isCardinalPresentable (Cᵒᵖ ⥤ A) κ

Tactic:
rintro _ ⟨X, G, hG⟩

Goal state after:
A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
P : ObjectProperty A
w✝ : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
X : C
G : A
hG : P G
⊢ isCardinalPresentable (Cᵒᵖ ⥤ A) κ (freeYoneda (X, ⟨G, hG⟩).1 ↑(X, ⟨G, hG⟩).2)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: X : SSet
inst✝ : X.Finite
⊢ ∃ Y, ∃ (_ : Y.Finite) (_ : IsFinitelyPresentable Y), ∃ p, Epi p

Tactic:
refine ⟨∐ (fun (s : X.N) ↦ Δ[s.dim]), inferInstance, ?_,
    Sigma.desc (fun s ↦ yonedaEquiv.symm s.simplex), ?_⟩
  · apply +allowSynthFailures isCardinalPresentable_of_isColimit' _ (coproductIsCoproduct _)
    · exact hasCardinalLT_of_finite _ _ (by rfl)
    · rintro s
      dsimp
      infer_instance
  · simp only [← Subcomplex.range_eq_top_iff, range_eq_iSup_sigma_ι,
        colimit.ι_desc, Cofan.mk_ι_app, ← N.iSup_subcomplex_eq_top,
        Subcomplex.range_eq_ofSimplex, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ IsSmall.{u, u, u + 1} innerHornInclusions

Tactic:
innerHornInclusions_eq_iSup

Goal state after:
⊢ IsSmall.{u, u, u + 1} (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι)
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
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) ⊤

Tactic:
by rw [← f.iSup_filtration]; apply isLUB_iSup

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 : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
⊢ (∀ (x_1 : Fin (n + 1)), ∃ x_2, (x.cast hd).simplex.2 (l.castSucc.succAbove x_2) = x_1) ∧
    ∀ (x_1 : Fin (m + 1 + 1)), ¬x_1 = k.castSucc → ∃ x_2, (x.cast hd).simplex.1 (l.castSucc.succAbove x_2) = x_1

Tactic:
refine ⟨fun j ↦ ?_, fun j hj ↦ ?_⟩

Goal state after:
case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (n + 1)
⊢ ∃ x_1, (x.cast hd).simplex.2 (l.castSucc.succAbove x_1) = j

case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (m + 1 + 1)
hj : ¬j = k.castSucc
⊢ ∃ x_1, (x.cast hd).simplex.1 (l.castSucc.succAbove x_1) = j
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 : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
t : Fin d
ht : IsIndex hl.δ ⋯ t.succ
⊢ False

Tactic:
obtain rfl : l = t.succ := by rw [← ht.min_eq, hl.min_δ]

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
t : Fin d
hl : IsIndex x hd t.succ.succ
ht : IsIndex hl.δ ⋯ t.succ
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case pos
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
i : Fin (((ht.type₁ ⋯).x.cast ⋯).dim + 1)
hi : i = s.index.castSucc
⊢ φ s.δ ⋯ i = (objEquiv (s.x.cast ⋯).simplex) i

pp: case neg
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
i : Fin (((ht.type₁ ⋯).x.cast ⋯).dim + 1)
hi : i ≠ s.index.castSucc
⊢ φ s.δ ⋯ i = (objEquiv (s.x.cast ⋯).simplex) i

Tactic:
· subst hi
    conv_lhs => rw [← s.isIndex.min_δ]
    dsimp
    rw [φ_castSucc]
    ext : 1
    · simp [← s.isIndex.simplex_fst_castSucc]
      rfl
    · change (s.x.cast s.hd).simplex.2
        (s.index.castSucc.succAbove (min s.δ rfl)) = _
      rw [s.isIndex.min_δ, Fin.succAbove_castSucc_self]
      exact s.isIndex.simplex_snd_succ

Goal state after:
case neg
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
i : Fin (((ht.type₁ ⋯).x.cast ⋯).dim + 1)
hi : i ≠ s.index.castSucc
⊢ φ s.δ ⋯ i = (objEquiv (s.x.cast ⋯).simplex) i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
⊢ (fun j ↦ if j.castSucc < i then 0 else 1) j₁ ≤ (fun j ↦ if j.castSucc < i then 0 else 1) j₂

Tactic:
by
        dsimp
        split_ifs <;> grind

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
⊢ stdSimplex.δ j.castSucc.succ ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = fg.op.map

Tactic:
rw [stdSimplex.δ_comp_yonedaEquiv_symm, op_δ, Equiv.apply_symm_apply,
      ← stdSimplex.yonedaEquiv_δ_comp, opEquiv_symm_apply_map, ← h.δ_succ_castSucc_map,
      Fin.rev_succ, Fin.rev_castSucc, Fin.castSucc_succ, ← hij, Fin.rev_rev]

Goal state after:
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
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
⊢ (Y.spine 1 f₂._proof_6 (f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x))).vertex 1 =
    (Y.spine 1 f₂._proof_6 (f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x))).vertex 0

Tactic:
simp only [spine_vertex]
        rw [← δ₂_one_eq_const, ← δ₂_zero_eq_const, ← hδ₁, ← hδ₀]
        simp only [← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_δ₂_two]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
⊢ IsPreconnected (sphere x r)

Tactic:
by
  rcases le_or_gt 0 r with hr | hr
  · exact (isConnected_sphere h x hr).isPreconnected
  · simpa [hr] using isPreconnected_empty

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

Goal state before:
pp: 𝕜 : 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 : (↑f'symm.nnnorm)⁻¹ ≤ ↑c
⊢ b ∈ closedBall b ε

Tactic:
by simp [ε0]

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

Goal state before:
pp: case inr
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
⊢ 1 < v b⁻¹

Tactic:
simpa using one_lt_inv_iff₀.2 ⟨v.pos hb₀, hb₁.lt_of_le hb⟩

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

Goal state before:
pp: 𝕜 : 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' s)

Tactic:
by
  rcases hc with hE | hc
  · exact isOpen_discrete _
  simp only [isOpen_iff_mem_nhds, nhds_basis_closedBall.mem_iff, forall_mem_image] at hs ⊢
  intro x hx
  rcases hs x hx with ⟨ε, ε0, hε⟩
  refine ⟨(f'symm.nnnorm⁻¹ - c) * ε, mul_pos (sub_pos.2 hc) ε0, ?_⟩
  exact (hf.surjOn_closedBall_of_nonlinearRightInverse f'symm (le_of_lt ε0) hε).mono hε Subset.rfl

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ cexp (log (f z) * g z)
⊢ AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) s x

Tactic:
apply AnalyticWithinAt.congr_of_eventuallyEq_insert _ e

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ cexp (log (f z) * g z)
⊢ AnalyticWithinAt ℂ (fun z ↦ cexp (log (f z) * g z)) s x