mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H✝ H : Homotopy f g
n : ℕ
⊢ ((alternatingFaceMapComplex C).map f).f (n + 1) =
    (dNext (n + 1)) (ToChainHomotopy.hom H) + (prevD (n + 1)) (ToChainHomotopy.hom H) +
      ((alternatingFaceMapComplex C).map g).f (n + 1)

Tactic:
rw [dNext_eq (i' := n) (w := by simp), prevD_eq (j' := n + 2) (w := by simp)]

Goal state after:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H✝ H : Homotopy f g
n : ℕ
⊢ ((alternatingFaceMapComplex C).map f).f (n + 1) =
    ((alternatingFaceMapComplex C).obj X).d (n + 1) n ≫ ToChainHomotopy.hom H n (n + 1) +
        ToChainHomotopy.hom H (n + 1) (n + 2) ≫ ((alternatingFaceMapComplex C).obj Y).d (n + 2) (n + 1) +
      ((alternatingFaceMapComplex C).map g).f (n + 1)
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 f₂ ⟶ Arrow.mk sq₁₃.π
⊢ (F.map f₁).app X₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.left β) =
    (F.obj X₁).map f₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)

Tactic:
have := Arrow.w β =≫ sq₁₃.fst

Goal state after:
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 f₂ ⟶ Arrow.mk sq₁₃.π
this : (Arrow.Hom.left β ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.fst = ((Arrow.mk f₂).hom ≫ Arrow.Hom.right β) ≫ sq₁₃.fst
⊢ (F.map f₁).app X₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.left β) =
    (F.obj X₁).map f₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)
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
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : i ∈ finset x hd
⊢ l.succ ≤ i

Tactic:
mem_finset_iff

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : (x.cast hd).simplex.1 i = k.succ
⊢ l.succ ≤ i
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₂.arrowHomEquiv sq₁₂ sq₁₃) α)
⊢ sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ adj₂.homEquiv.symm l.l = sq₁₂.inr ≫ Arrow.Hom.left α

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

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)
isIndex : IsIndex x hd l.succ
hs :
  min { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x ⋯ =
    { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.index.succ
y : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hd' : y.dim = d' + 1
l' : Fin (d' + 1)
isIndex' : IsIndex y hd' l'.succ
ht :
  min { x := y, d := d', hd := hd', index := l', isIndex := isIndex' }.x ⋯ =
    { x := y, d := d', hd := hd', index := l', isIndex := isIndex' }.index.succ
h :
  { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x =
    { x := y, d := d', hd := hd', index := l', isIndex := isIndex' }.x
⊢ { x := x, d := d, hd := hd, index := l, isIndex := isIndex } =
    { x := y, d := d', hd := hd', index := l', isIndex := isIndex' }

Tactic:
subst h

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
isIndex : IsIndex x hd l.succ
hs :
  min { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x ⋯ =
    { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.index.succ
d' : ℕ
l' : Fin (d' + 1)
hd' : { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x.dim = d' + 1
isIndex' : IsIndex { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x hd' l'.succ
ht :
  min
      { x := { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x, d := d', hd := hd', index := l',
          isIndex := isIndex' }.x
      ⋯ =
    { x := { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x, d := d', hd := hd', index := l',
          isIndex := isIndex' }.index.succ
⊢ { x := x, d := d, hd := hd, index := l, isIndex := isIndex } =
    { x := { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x, d := d', hd := hd', index := l',
      isIndex := isIndex' }
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' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
⊢ StrictMono (φ x hd)

Tactic:
Fin.strictMono_iff_lt_succ

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
⊢ ∀ (i : Fin (d + 1)), φ x hd i.castSucc < φ x hd i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
m : ℕ
X Y : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
this : anodyneExtensions sq₁₂.ι
⊢ fibrations SSet p

Tactic:
rwa [← HomotopicalAlgebra.fibration_iff]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
X : WalkingIso
⊢ ∀ (Y : WalkingIso) (f : X ⟶ Y),
    ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f =
      eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
X Y : WalkingIso
⊢ ∀ (f : X ⟶ Y),
    ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f =
      eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case sq
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₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))

Tactic:
exact ⟨hX₁.hom_ext _ _⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (Cocone.precompose
          (parallelPair.ext
              (-Iso.refl
                  ((parallelPair
                        ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                          (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                        0).obj
                    WalkingParallelPair.zero))
              (Iso.refl
                ((parallelPair
                      ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                        (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                      0).obj
                  WalkingParallelPair.one))
              ⋯ ⋯).inv).obj
      (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯)) ≅
    CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯

Tactic:
refine Cofork.ext (Iso.refl _) ?_

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ Cofork.π
        ((Cocone.precompose
              (parallelPair.ext
                  (-Iso.refl
                      ((parallelPair
                            ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                              (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                            0).obj
                        WalkingParallelPair.zero))
                  (Iso.refl
                    ((parallelPair
                          ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                            (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                          0).obj
                      WalkingParallelPair.one))
                  ⋯ ⋯).inv).obj
          (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯))) ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPair.ext
                      (-Iso.refl
                          ((parallelPair
                                ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                  (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                                0).obj
                            WalkingParallelPair.zero))
                      (Iso.refl
                        ((parallelPair
                              ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                              0).obj
                          WalkingParallelPair.one))
                      ⋯ ⋯).inv).obj
              (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯))).pt).hom =
    Cofork.π (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case sq
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 : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op X₁))
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op Y₁))
h : IsTerminal Y₃
hX₁ : IsTerminal ((G.obj (op X₁)).obj Y₃) := ⋯
hY₁ : IsTerminal ((G.obj (op Y₁)).obj Y₃) := ⋯
⊢ CommSq (𝟙 ((G.obj (op X₁)).obj X₃)) ((IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h).from ((G.obj (op X₁)).obj X₃))
    ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)

Tactic:
exact ⟨hX₁.hom_ext _ _⟩

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ 0)) ≫
      δ Y 0 =
    g.app (op ⦋n⦌)

Tactic:
ext x
    simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.δ_naturality_apply, ← H.h₁]
    dsimp
    apply congr_arg
    ext k : 2
    · simp [dsimp% SimplexCategory.δ_comp_σ_self (i := (0 : Fin (n + 1)))]
    · rw [stdSimplex.δ_objMk₁_of_lt _ _ (by tauto)]
      rfl

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j.succ)) ≫
      δ Y i.castSucc =
    δ X i ≫
      ↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j)

Tactic:
by
    ext x
    simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.δ_naturality_apply]
    dsimp
    apply congr_arg
    ext k : 2
    · simpa [stdSimplex.δ_objEquiv_symm_apply,
        SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}] using!
          ConcreteCategory.congr_hom (X.δ_comp_σ_of_le hij) x
    · rw [stdSimplex.δ_objMk₁_of_lt, Fin.pred_succ]
      rw [Fin.castSucc_lt_succ_iff, ← Fin.castSucc_succ]
      simp only [Fin.castSucc_le_castSucc_iff]
      exact hij.trans (j.castSucc_le_succ)

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

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.succ.succ)).2
      k =
    ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).2
      k

Tactic:
· rw [stdSimplex.δ_objMk₁_of_lt _ _ (by simp), stdSimplex.δ_objMk₁_of_le _ _ (by simp)]
      rfl

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

Goal state before:
pp: case «0»
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 := ⦋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 := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x))).arrow
      0 =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))).arrow 0

Tactic:
spineEquiv_f₂_arrow_zero

Goal state after:
case «0»
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 := ⦋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 := ⦋1⦌, property := _proof_12 })
⊢ f₁
      ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op))
        ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x)) =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))).arrow 0
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

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

Tactic:
let ⟨x₀, hx₀⟩ := hv.exists_abv_lt_one

Goal state after:
case inr
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
⊢ v a < 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «0»
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 := ⦋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 := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_15 _proof_12).op)) x))).arrow
      0 =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))).arrow 0

Tactic:
spineEquiv_f₂_arrow_zero

Goal state after:
case «0»
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 := ⦋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 := ⦋1⦌, property := _proof_12 })
⊢ f₁
      ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op))
        ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_15 _proof_12).op)) x)) =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))).arrow 0
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case inl
𝕜 : 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
⊢ y ∈ f '' closedBall b ε

pp: case inr
𝕜 : 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 : ↑c < (↑f'symm.nnnorm)⁻¹
⊢ y ∈ f '' closedBall b ε

Tactic:
· refine ⟨b, by simp [ε0], ?_⟩
    have : dist y (f b) ≤ 0 :=
      (mem_closedBall.1 hy).trans (mul_nonpos_of_nonpos_of_nonneg (by linarith) ε0)
    simp only [dist_le_zero] at this
    rw [this]

Goal state after:
case inr
𝕜 : 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 : ↑c < (↑f'symm.nnnorm)⁻¹
⊢ y ∈ f '' closedBall b ε
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ Filter.comap (⇑(WithAbs.congr v w (RingEquiv.refl F))) (𝓝 0)
⊢ U ∈ 𝓝 0

Tactic:
· rw [← RingEquiv.coe_toEquiv, ← Filter.map_equiv_symm] at hU
    obtain ⟨s, hs, hss⟩ := Filter.mem_map_iff_exists_image.1 hU
    rw [← RingEquiv.coe_toEquiv_symm, WithAbs.congr_symm] at hss
    exact Filter.mem_of_superset (h.symm.equivWithAbs_image_mem_nhds_zero hs) hss

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀

Tactic:
by_cases hf : AnalyticAt 𝕜 f z₀
  · by_cases hg : AnalyticAt 𝕜 g z₀
    · refine ENat.forall_natCast_le_iff_le.mp fun n ↦ ?_
      simp only [le_min_iff, natCast_le_analyticOrderAt, hf, hg, hf.add hg]
      refine fun ⟨⟨F, hF, hF'⟩, ⟨G, hG, hG'⟩⟩ ↦ ⟨F + G, hF.add hG, ?_⟩
      filter_upwards [hF', hG'] with z using by simp +contextual
    · simp [*]
  · simp [*]

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

Goal state before:
pp: case succ
n : ℕ
⊢ (-1) ^ n / (↑n + 1) = (-1) ^ n * ↑n.factorial / ((↑n + 1) * ↑n.factorial)

Tactic:
field_simp [show n.factorial ≠ 0 by positivity]

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

Goal state before:
pp: X Y : SSet
m : ℕ
⊢ IsIso (prodComparison hoFunctor X Δ[m])

Tactic:
convert_to IsIso (hoFunctor.map (prod.braiding _ _).hom ≫
    prodComparison hoFunctor Δ[m] X ≫ (prod.braiding _ _).hom)
  · ext <;> simp [← Functor.map_comp]
  suffices IsIso (prodComparison hoFunctor Δ[m] X) by infer_instance
  exact isIso_prodComparison_of_stdSimplex _ (isIso_prodComparison_stdSimplex _)

Goal state after: