mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
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
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
⊢ (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x

Tactic:
subst hik

Goal state after:
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 : ℕ
hij : i ≤ i + (k + 1)
hj : i + (k + 1) ≤ n
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨i + (k + 1), ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨i + (k + 1), ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + (k + 1), ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
⊢ (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of.inl.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ (mk n✝).len < (mk (n✝ + 1)).len

Tactic:
exact Nat.lt_add_one _

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

Goal state before:
pp: X Y : Truncated 2
inst✝¹ : Unique (Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 }))
inst✝ : Subsingleton (Y.obj (Opposite.op { obj := ⦋1⦌, property := isoTerminal._proof_1 }))
⊢ CategoryTheory.Prod.fst X.HomotopyCategory ↑Cat.chosenTerminal =
    (𝟭 X.HomotopyCategory).prod (isoTerminal Y).inv.toFunctor ⋙ inverse X Y ⋙ mapHomotopyCategory (fst X Y)

Tactic:
inverse_comp_mapHomotopyCategory_fst

Goal state after:
X Y : Truncated 2
inst✝¹ : Unique (Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 }))
inst✝ : Subsingleton (Y.obj (Opposite.op { obj := ⦋1⦌, property := isoTerminal._proof_1 }))
⊢ CategoryTheory.Prod.fst X.HomotopyCategory ↑Cat.chosenTerminal =
    (𝟭 X.HomotopyCategory).prod (isoTerminal Y).inv.toFunctor ⋙
      CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
i : Fin (n + 1)
⊢ i.castSucc ∈ finset f x ↔ x ≤ (f i).castSucc

Tactic:
by
  simp [mem_finset_iff, Fin.castPred_castSucc]

Goal state after:
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, { as := f i.as }.as ≤ k

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

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

Goal state before:
pp: case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)

Tactic:
rw [map'_eq_last_iff] at hx ⊢

Goal state after:
case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : ∀ (i : Fin (m + 1)), (g i).castSucc < x.castSucc
⊢ ∀ (i : Fin (n + 1)), ((g.comp f) i).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom
        (inr' (tensorObjOf x y) z ≫ WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom))
      i =
    (SimplexCategory.Hom.toOrderHom (inr' y z ≫ inr' x (tensorObjOf y z))) i

Tactic:
dsimp [MonoidalCategoryStruct.associator, associator]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom
        (inl' x y ≫
          inl' (tensorObjOf x y) z ≫
            WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom))
      i =
    (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i

Tactic:
dsimp [MonoidalCategoryStruct.associator, associator]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) ((SimplexCategory.Hom.toOrderHom (inl' x y)) i)) =
    (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom
        (inr' x y ≫
          inl' (tensorObjOf x y) z ≫
            WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom))
      i =
    (SimplexCategory.Hom.toOrderHom (inl' y z ≫ inr' x (tensorObjOf y z))) i

Tactic:
dsimp [MonoidalCategoryStruct.associator, associator]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
⊢ (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.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj : j < Order.succ i
c : f.Cell j
⊢ (↑(P.p c.s)).subcomplex ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex

Tactic:
rw [Order.lt_succ_iff_of_not_isMax hi] at hj

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj : j ≤ i
c : f.Cell j
⊢ (↑(P.p c.s)).subcomplex ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ f.filtration i ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j

Tactic:
conv_lhs => rw [filtration_def]
    simp only [sup_le_iff, iSup_le_iff]
    refine ⟨?_, fun j hj c ↦ ?_⟩
    · refine le_trans ?_ (le_iSup _ ⊥)
      exact le_trans (by simp) (le_iSup _ hi.bot_lt)
    · refine le_trans ?_ (le_iSup _ (Order.succ j))
      refine le_trans ?_ (le_iSup _
        (by rwa [← Order.IsSuccLimit.succ_lt_iff hi] at hj))
      exact f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hj.not_isMax)

Goal state after:
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
⊢ sq.LiftStruct

Tactic:
have := ExtremalEpi.isIso f (pullback.lift _ _ sq.w)
    (pullback.snd _ _) (by simp)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (pullback.snd i b)
⊢ sq.LiftStruct
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ c.horn ≤ (f.filtration j).preimage c.map

Tactic:
rw [← Subcomplex.image_le_iff, N.subcomplex_le_iff]
    intro s hs
    cases s using N.cases A with
    | mem s hs' => exact hs'.trans (by simp)
    | notMem s =>
      obtain ⟨t, ht⟩ := P.exists_or s
      rw [← c.rank_s]
      refine le_trans ?_ (f.subcomplex_le_filtration ⟨t, rfl⟩ (f.lt ?_))
      · obtain rfl | rfl := ht
        · exact P.le t
        · simp
      · replace hs : t.val.subcomplex ≤ c.horn.image c.map := by
          obtain rfl | rfl := ht
          · exact hs
          · refine le_trans ?_ hs
            rw [← S.le_def]
            exact (P.isUniquelyCodimOneFace t).le
        refine ⟨?_, ?_⟩
        · rintro rfl
          exact c.subcomplex_not_le_image_horn hs
        · rw [Subcomplex.N.lt_iff, SSet.N.lt_iff]
          exact lt_of_le_of_lt hs (c.image_horn_lt_subcomplex)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
hP : P.IsStrongGenerator
X Y : C
i : X ⟶ Y
inst✝ : Mono i
hi : ¬IsIso i
⊢ ∃ G, ∃ (_ : P G), ∃ g, ∀ (f : G ⟶ X), f ≫ i ≠ g

Tactic:
by_contra!
  exact hi (hP.isIso_of_mono i this)

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : LocallySmall.{w, v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
inst✝² : HasLimitsOfShape Kᵒᵖ (Type w)
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
e : C ≌ ShrinkHoms.{u} C := ShrinkHoms.equivalence C
⊢ IsCardinalPresentable c.pt κ

Tactic:
have (k : K) : IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ := by
    dsimp; infer_instance

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : LocallySmall.{w, v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
inst✝² : HasLimitsOfShape Kᵒᵖ (Type w)
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
e : C ≌ ShrinkHoms.{u} C := ShrinkHoms.equivalence C
this : ∀ (k : K), IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ
⊢ IsCardinalPresentable c.pt κ
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

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₂
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 = Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)

Tactic:
by
        apply sq₁₃.isPullback.hom_ext
        · 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]
        · have := l.fac_right
          dsimp at this ⊢
          simp only [Category.assoc, sq₁₃.π_snd, ← this, adj₂.homEquiv_naturality_three,
            arrowHomEquiv_apply_right_snd, Arrow.mk_right]

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h : s.x = t.x
⊢ s = t

Tactic:
have hs := s.isIndex.min_eq

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h : s.x = t.x
hs : min s.x ⋯ = s.index.succ
⊢ s = t
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h : s.x = t.x
hs : min s.x ⋯ = s.index.succ
⊢ s = t

Tactic:
have ht := t.isIndex.min_eq

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h : s.x = t.x
hs : min s.x ⋯ = s.index.succ
ht : min t.x ⋯ = t.index.succ
⊢ s = t
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

Goal state before:
pp: case neg
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : ¬j ≤ i.castSucc
⊢ ↑((stdSimplex.objEquiv.symm (SimplexCategory.σ i)) j) + ↑((objMk₁ i.castSucc.succ) j) = ↑j

Tactic:
simp only [not_le] at hj
        rw [objMk₁_of_le_castSucc _ _ (by simpa), objEquiv_symm_apply]
        change (i.predAbove j : ℕ) + 1 = _
        rw [Fin.predAbove_of_castSucc_lt _ _ hj, Fin.val_pred]
        lia

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

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
h : is.castSucc ∈ Ss
⊢ False

Tactic:
have : s.1 is.castSucc ≤ k.castSucc := by
              simpa using (hs.simplex_fst_le_castSucc_iff is.castSucc).2 (by simp)
            simp_all [Ss]

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

Tactic:
← h.δ_succ_succ_map,

Goal state after:
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
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.castSucc.rev ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.succ.succ ≫ h.map)))
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2.inr.inl.inl
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
a b c : R
k : ι
hk hj : k ≠ i
ha :
  1 < (restrict (fun k_1 ↦ k_1 ≠ k) v ⟨i, ⋯⟩) a ∧
    ∀ (j : { k_1 // k_1 ≠ k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 ≠ k) v j) a < 1
hb :
  1 < (restrict (fun k_1 ↦ k_1 = i ∨ k_1 = k) v ⟨i, ⋯⟩) b ∧
    ∀ (j : { k_1 // k_1 = i ∨ k_1 = k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 = i ∨ k_1 = k) v j) b < 1
ha₁ : (v k) a = 1
hc :
  1 < (restrict (fun k_1 ↦ k_1 ≠ k) v ⟨i, ⋯⟩) c ∧
    (∀ (j : { k_1 // k_1 ≠ k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 ≠ k) v j) c < 1) ∧ (v k) c < 1
⊢ (v k) c < 1

pp: case refine_2.inr.inl.inr
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h✝ : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a = 1
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
k : ι
hk : k ≠ i
h : k ≠ j
⊢ (v k) c < 1

Tactic:
try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
⊢ AnalyticAt 𝕜 g (f x)

Tactic:
have hra : AnalyticAt 𝕜 r (f x) := hf.analyticAt_localInverse hf'

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
⊢ AnalyticAt 𝕜 g (f x)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2.inr.inr.inr.inl
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
a b c : R
k : ι
hk hj : k ≠ i
ha :
  1 < (restrict (fun k_1 ↦ k_1 ≠ k) v ⟨i, ⋯⟩) a ∧
    ∀ (j : { k_1 // k_1 ≠ k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 ≠ k) v j) a < 1
hb :
  1 < (restrict (fun k_1 ↦ k_1 = i ∨ k_1 = k) v ⟨i, ⋯⟩) b ∧
    ∀ (j : { k_1 // k_1 = i ∨ k_1 = k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 = i ∨ k_1 = k) v j) b < 1
ha₁ : (v k) a ≠ 1
ha_gt : 1 < (v k) a
hc :
  1 < (restrict (fun k_1 ↦ k_1 ≠ k) v ⟨i, ⋯⟩) c ∧
    (∀ (j : { k_1 // k_1 ≠ k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 ≠ k) v j) c < 1) ∧ (v k) c < 1
⊢ (v k) c < 1

pp: case refine_2.inr.inr.inr.inr
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h✝ : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a ≠ 1
ha_gt : 1 < (v j) a
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
k : ι
hk : k ≠ i
h : k ≠ j
⊢ (v k) c < 1

Tactic:
try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 1 n = 1
⊢ 1 = 0 + 1

Tactic:
exact (@zero_add R _ 1).symm

Goal state after: