mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ ∀ (j : WalkingParallelPair),
    ((Cocone.precompose
                    (NatIso.ofComponents
                        (fun X ↦
                          WalkingParallelPair.casesOn X
                            (Iso.refl
                              ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                    (pullback.cone (f.app k) (f.app k)).snd).obj
                                WalkingParallelPair.zero))
                            (Iso.refl
                              ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                    (pullback.cone (f.app k) (f.app k)).snd).obj
                                WalkingParallelPair.one)))
                        ⋯).inv).obj
                (Cofork.ofπ (f.app k) ⋯)).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose
                    (NatIso.ofComponents
                        (fun X ↦
                          WalkingParallelPair.casesOn X
                            (Iso.refl
                              ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                    (pullback.cone (f.app k) (f.app k)).snd).obj
                                WalkingParallelPair.zero))
                            (Iso.refl
                              ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                    (pullback.cone (f.app k) (f.app k)).snd).obj
                                WalkingParallelPair.one)))
                        ⋯).inv).obj
                (Cofork.ofπ (f.app k) ⋯)).pt).hom =
      (((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯)).ι.app j

Tactic:
by rintro (_ | _ | _); all_goals cat_disch

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

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
t : ↑P.II
hs : (↑(P.p t)).subcomplex ≤ c.horn.image c.map
⊢ (↑t).subcomplex ≤ c.horn.image c.map

Tactic:
refine le_trans ?_ hs
            rw [← S.le_def]
            exact (P.isUniquelyCodimOneFace t).le

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
⊢ ∃ J x, P.colimitsOfShape J X

Tactic:
obtain ⟨_, _, _, hX⟩ := h.exists_colimitsOfShape X

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
w✝² : Type w
w✝¹ : SmallCategory w✝²
w✝ : IsCardinalFiltered w✝² κ
hX : P.colimitsOfShape w✝² X
⊢ ∃ J x, P.colimitsOfShape J X
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ P.retractClosure ≤ isCardinalPresentable C κ

Tactic:
· simpa only [ObjectProperty.retractClosure_le_iff] using h.le_isCardinalPresentable

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
⊢ IsFinitelyPresentable X

Tactic:
obtain ⟨Y, _, _, p, _⟩ := exists_epi_from_isCardinalPresentable X
  obtain ⟨Z, _, _, q, _⟩ := exists_epi_from_isCardinalPresentable (pullback p p)
  have := Cardinal.fact_isRegular_aleph0.{u}
  have := IsRegularEpiCategory.regularEpiOfEpi p
  apply +allowSynthFailures isCardinalPresentable_of_isColimit' _
      (isCoequalizerEpiComp ((EffectiveEpi.getStruct p).isColimitCoforkOfIsPullback
        (IsPullback.of_hasPullback p p)) q) _
  · exact hasCardinalLT_of_finite _ _ (by rfl)
  · rintro (_ | _) <;> dsimp <;> infer_instance

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

Goal state before:
pp: ⊢ modelCategoryQuillen.J.rlp.llp =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0

Goal state after:
⊢ ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ innerHornInclusions.rlp.llp =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0

Goal state after:
⊢ ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : l.castSucc < i
⊢ i = l.castSucc ∨ i = l.succ

Tactic:
obtain rfl | hi := (Fin.castSucc_lt_iff_succ_le.1 hi).eq_or_lt
    · exact Or.inr rfl
    · obtain ⟨l, rfl⟩ := Fin.eq_castSucc_of_ne_last (x := l) (by grind)
      refine (hu _ rfl l.succ ?_).elim
      simp [isIndex_succ, hu', stdSimplex.δ_apply,
        Fin.succAbove_of_castSucc_lt i l.castSucc (by grind),
        Fin.succAbove_of_castSucc_lt i l.succ (by grind),
        dsimp% hl.simplex_fst_castSucc, dsimp% hl.simplex_snd_succ,
        dsimp% hl.simplex_fst_succ]

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 : ℕ
s : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hds : s.dim = d + 1
is : Fin (d + 1)
hs : IsIndex s hds is.succ
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hdt : t.dim = d' + 1
it : Fin (d' + 1)
ht : IsIndex t hdt it.succ
h₁ :
  { x := s, d := d, hd := hds, index := is, isIndex := hs } ≠ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₂ :
  (pairingCore k n).type₂ { x := s, d := d, hd := hds, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
⊢ (pairingCore k n).dim { x := s, d := d, hd := hds, index := is, isIndex := hs } =
      (pairingCore k n).dim { x := t, d := d', hd := hdt, index := it, isIndex := ht } →
    (finset { x := s, d := d, hd := hds, index := is, isIndex := hs }.x ⋯).card <
      (finset { x := t, d := d', hd := hdt, index := it, isIndex := ht }.x ⋯).card

Tactic:
h₃

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
s : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hds : s.dim = d + 1
is : Fin (d + 1)
hs : IsIndex s hds is.succ
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hdt : t.dim = d' + 1
it : Fin (d' + 1)
ht : IsIndex t hdt it.succ
h₁ :
  { x := s, d := d, hd := hds, index := is, isIndex := hs } ≠ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₂ :
  (pairingCore k n).type₂ { x := s, d := d, hd := hds, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₃ :
  (pairingCore k n).dim { x := s, d := d, hd := hds, index := is, isIndex := hs } =
    (pairingCore k n).dim { x := t, d := d', hd := hdt, index := it, isIndex := ht }
⊢ (finset { x := s, d := d, hd := hds, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := t, d := d', hd := hdt, index := it, isIndex := ht }.x ⋯).card
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ IsColimit (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    (Preadditive.isColimitCokernelCoforkOfCofork
      ((isColimitMapCoconeCoforkEquiv _ _).1
        (isColimitOfPreserves (sigmaConst.obj R) X.isColimitCoforkπ₀)))
  · refine parallelPair.ext (-Iso.refl _) (Iso.refl _) ?_ (by simp)
    simp [chainComplex, SSet.chainComplexFunctor, sub_eq_neg_add]
  · refine Cofork.ext (Iso.refl _) ?_
    ext
    simp [chainComplex, SSet.chainComplexFunctor, π₀.fromChainComplexXZero]

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

Goal state before:
pp: p : ℕ
⊢ Function.Bijective fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩

Tactic:
refine ⟨fun _ _ h ↦ ?_, fun ⟨⟨s₁, s₂⟩, hs⟩ ↦ ?_⟩

Goal state after:
case refine_1
p : ℕ
x✝¹ x✝ : Fin (p + 1)
h :
  (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) x✝¹ =
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) x✝
⊢ x✝¹ = x✝

case refine_2
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
s₂ : Δ[1] _⦋p + 1⦌
hs : (s₁, s₂) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
⊢ ∃ a, (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a = ⟨(s₁, s₂), hs⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
⊢ φ ≫ s.map = const x

Tactic:
by
  refine (Subcomplex.lift φ ?_) ≫= s.comm
  rw [stdSimplex.le_boundary_iff]
  intro h
  have : IsIso (Subcomplex.range φ).ι := by rw [h]; infer_instance
  exact stdSimplex.not_hasDimensionLT n
    ((hasDimensionLT_iff_of_iso (asIso (Subcomplex.range φ).ι) n).mp inferInstance)

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

Goal state before:
pp: case e_6
⊢ ⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1))) default) = ⟨Pi.single 0 1, ⋯⟩

Tactic:
refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_

Goal state after:
case e_6
⊢ stdSimplex.map (⇑(ConcreteCategory.hom (SimplexCategory.δ 1))) (⦋0⦌.toTopHomeo default) = ⟨Pi.single 0 1, ⋯⟩
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ Sigma.ι (fun x ↦ ((evaluation TopCat C).obj (SimplexCategory.toTop.{w} ^⦋n⦌)).obj F) i ≫
      ((singularChainComplexFunctorAdjunction C n).counit.app F).app X =
    F.map i.down

Tactic:
trans F.map (SSet.toTopSimplex.inv.app ⦋n⦌ ≫ SSet.toTop.map (SSet.yonedaEquiv.symm i) ≫
      sSetTopAdj.counit.app X)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ Sigma.ι (fun x ↦ ((evaluation TopCat C).obj (SimplexCategory.toTop.{w} ^⦋n⦌)).obj F) i ≫
      ((singularChainComplexFunctorAdjunction C n).counit.app F).app X =
    F.map (toTopSimplex.inv.app ⦋n⦌ ≫ toTop.map (SSet.yonedaEquiv.symm i) ≫ sSetTopAdj.counit.app X)

C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ F.map (toTopSimplex.inv.app ⦋n⦌ ≫ toTop.map (SSet.yonedaEquiv.symm i) ≫ sSetTopAdj.counit.app X) = F.map i.down
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: case e_6
⊢ ⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 0))) default) = ⟨Pi.single 1 1, ⋯⟩

Tactic:
refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_

Goal state after:
case e_6
⊢ stdSimplex.map (⇑(ConcreteCategory.hom (SimplexCategory.δ 0))) (⦋0⦌.toTopHomeo default) = ⟨Pi.single 1 1, ⋯⟩
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
h : ∀ (x : R), v x < 1 ↔ w x < 1
x y : R
hy₀ : v x ≠ 0
⊢ v y * (v x)⁻¹ < 1 ↔ w y < w x

Tactic:
← one_mul (w x),

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
h : ∀ (x : R), v x < 1 ↔ w x < 1
x y : R
hy₀ : v x ≠ 0
⊢ v y * (v x)⁻¹ < 1 ↔ w y < 1 * w x
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 })
⊢ f₁
      ((ConcreteCategory.hom (X.map (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4).op))
        ((ConcreteCategory.hom (X.map (δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op)) x)) =
    (ConcreteCategory.hom (Y.map (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ f₂._proof_4).op))
      ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))

Tactic:
hσ,

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 })
⊢ (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op))
      (f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op)) x)) =
    (ConcreteCategory.hom (Y.map (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ f₂._proof_4).op))
      ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
⊢ Dense sᶜ

Tactic:
rw [← interior_eq_empty_iff_dense_compl]

Goal state after:
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
⊢ interior s = ∅
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «1»
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 (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4).op))
        ((ConcreteCategory.hom (X.map (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op)) x)) =
    (ConcreteCategory.hom (Y.map (Hom.tr (SimplexCategory.mkOfSucc 1) ⋯ f₂._proof_4).op))
      ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))

Tactic:
hσ,

Goal state after:
case «1»
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 })
⊢ (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op))
      (f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op)) x)) =
    (ConcreteCategory.hom (Y.map (Hom.tr (SimplexCategory.mkOfSucc 1) ⋯ f₂._proof_4).op))
      ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inl
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
⊢ v 0 ^ 1 = w 0

Tactic:
aesop (add simp [h.isNontrivial_congr])

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
hw : ¬w.IsNontrivial
x : F
h₀ : x ≠ 0
⊢ v x ^ 1 = w x

Tactic:
aesop (add simp [h.isNontrivial_congr])

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ (∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (-f) z = (z - z₀) ^ n • g z) ↔
    ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
exact (Equiv.neg _).exists_congr <| by simp [neg_eq_iff_eq_neg]

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₀ : 𝕜
hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀
⊢ analyticOrderAt f z₀ ≤ analyticOrderAt (f + g) z₀

Tactic:
by simpa [hfg.le] using le_analyticOrderAt_add (f := f) (g := g) (z₀ := z₀)

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 : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
⊢ analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = 1

Tactic:
generalize h : analyticOrderAt (f · - f x) x = r
  cases r with
  | top =>
    simp_rw [analyticOrderAt_eq_top, sub_eq_zero] at h
    refine (hf' ?_).elim
    rw [EventuallyEq.deriv_eq h, deriv_const]
  | coe r =>
    norm_cast
    obtain ⟨F, hFa, hFne, hfF⟩ := (analyticOrderAt_eq_natCast (by fun_prop)).mp h
    apply eq_of_ge_of_le
    · by_contra! hr
      have := hfF.self_of_nhds
      simp_all
    · contrapose! hf'
      simp_rw [sub_eq_iff_eq_add] at hfF
      rw [EventuallyEq.deriv_eq hfF, deriv_add_const, deriv_fun_smul (by fun_prop) (by fun_prop),
        deriv_fun_pow (by fun_prop), sub_self, zero_pow (by lia), zero_pow (by lia),
        mul_zero, zero_mul, zero_smul, zero_smul, add_zero]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∈ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (fun z ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0))
          z

Tactic:
simpa [hz] using hU' z hz

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
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
⊢ ↑n ≤ analyticOrderAt (deriv f) z₀ ↔ ↑n + 1 ≤ analyticOrderAt f z₀

Tactic:
rw [natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero hf.deriv,
    ← Nat.cast_add_one, natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero hf]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
⊢ (∀ i < n, iteratedDeriv i (deriv f) z₀ = 0) ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0