mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : NoMaxOrder ι
j : ι
s : (range (f.m j)).N
⊢ (f.mapN s).simplex ∈ X.nonDegenerate (f.mapN s).dim

Tactic:
obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ (f.mapN (Cell.type₁ f c)).simplex ∈ X.nonDegenerate (f.mapN (Cell.type₁ f c)).dim

case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ (f.mapN (Cell.type₂ f c)).simplex ∈ X.nonDegenerate (f.mapN (Cell.type₂ f c)).dim
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✝ : NoMaxOrder ι
j : ι
s t : (range (f.m j)).N
h : f.mapN s = f.mapN t
⊢ s = t

Tactic:
obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
t : (range (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN t
⊢ Cell.type₁ f c = t

case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
t : (range (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN t
⊢ Cell.type₂ f c = t
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
P₁ P₂ : Cᵒᵖ ⥤ A
i : P₁ ⟶ P₂
x✝ : Mono i
hi : ∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i
⊢ IsIso i

Tactic:
NatTrans.isIso_iff_isIso_app

Goal state after:
A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
P₁ P₂ : Cᵒᵖ ⥤ A
i : P₁ ⟶ P₂
x✝ : Mono i
hi : ∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i
⊢ ∀ (X : Cᵒᵖ), IsIso (i.app X)
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
i : Fin (m + 2)
hi : i ≠ k.castSucc
⊢ i ∈ Set.range ⇑(x.cast hd).simplex.1

Tactic:
subst hd

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (m + 2)
hi : i ≠ k.castSucc
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.1
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
i : Fin (n + 1)
⊢ i ∈ Set.range ⇑(x.cast hd).simplex.2

Tactic:
subst hd

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (n + 1)
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.2
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 α
⊢ (Arrow.mk f₂).hom ≫ adj₂.homEquiv l.l = Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)

Tactic:
have := l.fac_left
        dsimp at this ⊢
        simp only [← adj₂.homEquiv_naturality_two, ← this,
          sq₁₂.inl_ι_assoc]

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

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

Tactic:
have := l.fac_right

Goal state after:
case h₁
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct α
this : l.l ≫ (Arrow.mk f₃).hom = Arrow.Hom.right α
⊢ (adj₂.homEquiv l.l ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.snd = Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α) ≫ sq₁₃.snd
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₂.arrowHomEquiv sq₁₂ sq₁₃) α)
⊢ adj₂.homEquiv.symm l.l ≫ (Arrow.mk f₃).hom = Arrow.Hom.right α

Tactic:
by
        have := l.fac_right =≫ sq₁₃.snd
        dsimp at this ⊢
        simp only [Category.assoc, sq₁₃.π_snd, arrowHomEquiv_apply_right_snd,
          Arrow.mk_right] at this
        rw [← adj₂.homEquiv_symm_naturality_three, this,
          Equiv.symm_apply_apply]

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

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ 0 ≫ fromChainComplexXZero X R = 0

Tactic:
zero_comp

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ 0 = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.right.inr
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
i : Fin (d + 1)
⊢ it.succ.succAbove i ∈ St ↔ it.succ.succAbove i ∈ Finset.image it.succ.succAbove Sδ ∪ {it.succ}

Tactic:
· simp [hSt]

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

Goal state before:
pp: case pos
m✝ : ℕ
k : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
⊢ (if hk : Fin.last (m + 1) = Fin.last (m + 1) then
      (pairingCore 0 n).pairing.op.ofIso
        (((stdSimplex.opIso ⦋m + 1⦌).symm ⊗ᵢ (stdSimplex.opIso ⦋n⦌).symm) ≪≫
          Functor.Monoidal.μIso opFunctor Δ[m + 1] Δ[n])
        ⋯
    else (pairingCore ((Fin.last (m + 1)).castPred hk) n).pairing).IsRegular

Tactic:
dif_pos rfl

Goal state after:
case pos
m✝ : ℕ
k : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
⊢ ((pairingCore 0 n).pairing.op.ofIso
      (((stdSimplex.opIso ⦋m + 1⦌).symm ⊗ᵢ (stdSimplex.opIso ⦋n⦌).symm) ≪≫
        Functor.Monoidal.μIso opFunctor Δ[m + 1] Δ[n])
      ⋯).IsRegular
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1))) default)) = 0

Tactic:
rw [← stdSimplexHomeomorphUnitInterval_zero]

Goal state after:
⊢ stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1))) default)) =
    stdSimplexHomeomorphUnitInterval ⟨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⦌
⊢ ((ConcreteCategory.hom ((sSetTopAdj.unit.app (TopCat.toSSet.obj X)).app (Opposite.op ⦋n⦌))) i).down ≫
      sSetTopAdj.counit.app X =
    i.down

Tactic:
exact congr(($(sSetTopAdj.right_triangle_components X).app (.op ⦋n⦌) i).down)

Goal state after:
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
H : ¬interior s = ∅
⊢ False

Tactic:
apply lt_irrefl (ℵ₀ : Cardinal.{u})

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
H : ¬interior s = ∅
⊢ ℵ₀ < ℵ₀
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
⊢ {c + x} ∩ s = ∅

Tactic:
simpa only [singleton_inter_eq_empty, mem_compl_iff, Ib] using hb

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

Goal state before:
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)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
⊢ y ∈ f '' closedBall b ε

Tactic:
have usucc : ∀ n, u (n + 1) = g (u n) := by simp [hu, ← iterate_succ_apply' g _ b]

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)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
⊢ y ∈ f '' closedBall b ε
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case refine_1.succ.zero.«2»
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
hn : 0 + 1 < 2
⊢ naturalityProperty f₀ f₁ hδ₁ hδ₀ hY (δ 2 ((fun i ↦ i) ⟨2, ⋯⟩) ⋯ ⋯)

Tactic:
ext; apply hδ'₂ f₀ f₁ hδ₁ hδ₀ hY

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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
n : ℕ
x✝ :
  (∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ∧
    ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z
F : 𝕜 → E
hF : AnalyticAt 𝕜 F z₀
hF' : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • F z
G : 𝕜 → E
hG : AnalyticAt 𝕜 G z₀
hG' : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • G z
z : 𝕜
⊢ f z = (z - z₀) ^ n • F z → g z = (z - z₀) ^ n • G z → (f + g) z = (z - z₀) ^ n • (F + G) z

Tactic:
by simp +contextual

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

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ Surjective f

Tactic:
rcases hc with hE | hc
  · have : Subsingleton F := (Equiv.subsingleton_congr f'.toEquiv).1 hE
    exact surjective_to_subsingleton _
  · apply forall_of_forall_mem_closedBall (fun y : F => ∃ a, f a = y) (f 0) _
    have hc' : (0 : ℝ) < N⁻¹ - c := by rw [sub_pos]; exact hc
    let p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ Set.range f
    have hp : ∀ᶠ r : ℝ in atTop, p ((N⁻¹ - c) * r) := by
      have hr : ∀ᶠ r : ℝ in atTop, 0 ≤ r := eventually_ge_atTop 0
      refine hr.mono fun r hr => Subset.trans ?_ (image_subset_range f (closedBall 0 r))
      refine hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr ?_
      exact subset_univ _
    refine ((tendsto_id.const_mul_atTop hc').frequently hp.frequently).mono ?_
    exact fun R h y hy => h hy

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
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
⊢ ∀ a ∈ U,
    F a = if a ∈ U then F a else (a ^ n)⁻¹ • (f a - ∑ i ∈ Finset.range n, (a ^ i / ↑i.factorial) • iteratedDeriv i f 0)

Tactic:
by simp +contextual

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

Goal state before:
pp: D X : SSet
H : ∀ (m : ℕ), IsIso (prodComparison hoFunctor D Δ[m])
⊢ IsIso
    ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}).whiskerLeft
      (prodComparisonNatTrans hoFunctor D))

Tactic:
NatTrans.isIso_iff_isIso_app

Goal state after:
D X : SSet
H : ∀ (m : ℕ), IsIso (prodComparison hoFunctor D Δ[m])
⊢ ∀ (X_1 : CostructuredArrow uliftYoneda.{u, 0, 0} X),
    IsIso
      (((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}).whiskerLeft
            (prodComparisonNatTrans hoFunctor D)).app
        X_1)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
⊢ MeromorphicAt (-f) x

Tactic:
convert (MeromorphicAt.const (-1 : 𝕜) x).smul hf

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
⊢ -f = (fun x ↦ -1) • f
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✝ : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
⊢ f = 0 → ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0

Tactic:
by simp +contextual

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✝ : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z = ⊤ ↔ f = 0

Tactic:
by
  refine analyticOrderAt_eq_top.trans ⟨fun h ↦ eqOn_univ .. |>.mp ?_, by simp +contextual⟩
  apply eqOn_zero_of_preconnected_of_frequently_eq_zero (fun z _ ↦ hf z) isPreconnected_univ trivial
  exact hf z |>.frequently_eq_iff_eventually_eq analyticAt_const |>.mpr h

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ (ascPochhammer ℕ n).smeval (-↑n) * (-↑n + n • 1) = 0

Tactic:
nsmul_eq_mul,

Goal state after:
n : ℕ
⊢ (ascPochhammer ℕ n).smeval (-↑n) * (-↑n + ↑n * 1) = 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ (-1) ^ n * ↑n.factorial = n.factorial • (-1) ^ n

Tactic:
nsmul_eq_mul,

Goal state after:
n : ℕ
⊢ (-1) ^ n * ↑n.factorial = ↑n.factorial * (-1) ^ n
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n k : ℕ
⊢ (descPochhammer ℤ k).smeval ↑n = k.factorial • ↑(n.choose k)

Tactic:
nsmul_eq_mul,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n k : ℕ
⊢ (descPochhammer ℤ k).smeval ↑n = ↑k.factorial * ↑(n.choose k)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (descPochhammer ℤ (k + 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r

Tactic:
descPochhammer_succ_left

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (X * (descPochhammer ℤ k).comp (X - 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ r * (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r =
    (descPochhammer ℤ k).smeval r + r * (descPochhammer ℤ k).smeval r - ↑k • 1 * (descPochhammer ℤ k).smeval r +
      k • (descPochhammer ℤ k).smeval r

Tactic:
nsmul_eq_mul,

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ r * (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r =
    (descPochhammer ℤ k).smeval r + r * (descPochhammer ℤ k).smeval r - ↑k • 1 * (descPochhammer ℤ k).smeval r +
      ↑k * (descPochhammer ℤ k).smeval r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun x ↦ (-↑x) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)) ((-↑x) ^ r * cexp (↑π * I * r)) x

Tactic:
suffices HasDerivAt (fun y : ℝ => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)))
        ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x by
      convert! this.div_const (r + 1) using 1
      conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]

Goal state after:
case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
this :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
⊢ (descPochhammer ℤ n).smeval a = iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0

Tactic:
specialize this (show 0 ∈ _ by simp [B])

Goal state after:
a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
this : iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B 0 = (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) 0
⊢ (descPochhammer ℤ n).smeval a = iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0