mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

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

Tactic:
split_ifs

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 0 ≤ 0

case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 0 ≤ 1

case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 1 ≤ 0

case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 1 ≤ 1
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
i j : Fin (n + 1)
hij : i ≤ j
⊢ (ConcreteCategory.hom (X.map (mkOfLe i j hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe i j hij) fac_aux₁._proof_1))) x

Tactic:
exact fac_aux₂ _ _ _ _ _ _ (by lia)

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

Goal state before:
pp: case mpr.inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
hi : Fin.last (n + 1) ∈ finset f x
⊢ y.castSucc ≤ Fin.last (n + 1)

Tactic:
· apply Fin.le_last

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

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)

Tactic:
simp only [NatTrans.mono_iff_mono_app, mono_iff_injective]

Goal state after:
X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
⊢ ∀ (k : SimplexCategoryᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom ((yonedaEquiv.symm x).app k))
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 ι
i₁ : ι
⊢ ∀ ⦃b : ι⦄, i₁ ≤ b → f.filtration i₁ ≤ f.filtration b

Tactic:
i₂

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
i₁ i₂ : ι
⊢ i₁ ≤ i₂ → f.filtration i₁ ≤ f.filtration i₂
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
⊢ F.isDenseAt Y

Tactic:
let φ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) :
        (restrictedULiftYoneda.{w} F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
      { app := fun ⟨X⟩ ↦ ↾fun ⟨x⟩ ↦ ULift.up (s.ι.app (.mk x))
        naturality := by
          rintro ⟨X₁⟩ ⟨X₂⟩ ⟨f⟩
          ext ⟨x⟩
          let α : CostructuredArrow.mk (F.map f ≫ x) ⟶ CostructuredArrow.mk x :=
            CostructuredArrow.homMk f
          exact ULift.down_injective (s.w α).symm }

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
⊢ F.isDenseAt Y
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
X : C
G : A
hG : P G
x : freeYoneda X G ⟶ P₁
⊢ (fun f ↦ f ≫ i.app (op X)) (freeYonedaHomEquiv x) = freeYonedaHomEquiv ((fun f ↦ f ≫ i) x)

Tactic:
by simp [freeYonedaHomEquiv_comp]

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

Goal state before:
pp: case inl.inr.refine_1
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
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ (x.cast hd).simplex.1 i.castSucc ≤ k.castSucc

Tactic:
rw [simplex_fst_le_castSucc_iff]

Goal state after:
case inl.inr.refine_1
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
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ i.castSucc < min x hd
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ (X₁ □ X₂ □ X₃).left ⟶ ((X₁ □ X₂) □ X₃).left

Tactic:
exact pushout.desc ((whiskerLeftIso _ _).hom.left ≫
          pushout.desc (pushout.inl _ _) ((pushout.inl _ _ ▷ _) ≫ pushout.inr _ _)
          (by simp [Limits.pushout.associator_inv_naturality_right_condition]))
        ((α_ _ _ _).inv ≫ (pushout.inr _ _) ▷ _ ≫ pushout.inr _ _)
        (((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
          (by simp [whisker_exchange_assoc,
            Limits.pushout.associator_inv_naturality_right_condition, ← whiskerLeft_comp_assoc])
          (by simp [whisker_exchange_assoc, Limits.pushout.condition_whiskerRight_assoc,
            ← whiskerLeft_comp_assoc]))

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

Goal state before:
pp: X : SSet
⊢ ¬X.Nonempty ↔ X.HasDimensionLT 0

Tactic:
simp only [not_nonempty_iff]

Goal state after:
X : SSet
⊢ IsEmpty (X _⦋0⦌) ↔ X.HasDimensionLT 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

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

Tactic:
split_ifs

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 0 ≤ 0

case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 0 ≤ 1

case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 1 ≤ 0

case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 1 ≤ 1
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 := ⋯
x : E := ⋯
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
B : {t | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t : ℝ
z : E := ⋯
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
⊢ [a -[ℝ] z] ⊆ sᶜ

Tactic:
rw [subset_compl_iff_disjoint_right, disjoint_iff_inter_eq_empty]

Goal state after:
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]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
B : {t | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t : ℝ
z : E := c + t • y
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
⊢ [a -[ℝ] z] ∩ 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 := ⋯
x : E := ⋯
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
B : {t | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t : ℝ
z : E := ⋯
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
JA : JoinedIn sᶜ a z
⊢ [b -[ℝ] z] ⊆ sᶜ

Tactic:
rw [subset_compl_iff_disjoint_right, disjoint_iff_inter_eq_empty]

Goal state after:
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]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
B : {t | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t : ℝ
z : E := c + t • y
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
JA : JoinedIn sᶜ a z
⊢ [b -[ℝ] z] ∩ s = ∅
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑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)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
z : E
hz : z ∈ closedBall b ε
⊢ g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y

Tactic:
hgz

Goal state after:
𝕜 : 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)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
⊢ dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
x✝ : ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne : ⋯.choose < n
this : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀
⊢ g z₀ = 0

Tactic:
tendsto_nhds_unique_of_eventuallyEq (l := 𝓝[≠] z₀)
        hg.continuousAt.continuousWithinAt this.continuousWithinAt ?_

Goal state after:
case neg.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
x✝ : ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne : ⋯.choose < n
this : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀
⊢ (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀ = 0

𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
x✝ : ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne : ⋯.choose < n
this : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀
⊢ g =ᶠ[𝓝[≠] z₀] fun z ↦ (z - z₀) ^ (n - m) • h z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case coe.e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
h : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ (s + 1) • g z
hrne : s + 1 ≠ 0
⊢ analyticOrderAt (deriv f) x = ↑s

Tactic:
obtain ⟨F, hFa, hFne, hfF⟩ := h

Goal state after:
case coe.e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ (s + 1) • F z
⊢ analyticOrderAt (deriv f) x = ↑s
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ AnalyticAt ℝ Real.log x

Tactic:
have : Real.log = fun x : ℝ ↦ (Complex.log x).re := by ext x; exact (Complex.log_ofReal_re x).symm
  rw [this]
  refine AnalyticAt.re_ofReal <| analyticAt_clog ?_
  simp [hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
⊢ ordinaryHypergeometricSeries 𝔸 a b c n = 0 ↔ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c

Tactic:
by
  refine ⟨fun h ↦ ?_, fun zero ↦ ?_⟩
  · rw [ordinaryHypergeometricSeries, ofScalars_eq_zero] at h
    simp only [_root_.mul_eq_zero, inv_eq_zero] at h
    rcases h with ((hn | h) | h) | h
    · simp [Nat.factorial_ne_zero] at hn
    all_goals
      obtain ⟨kn, hkn, hn⟩ := (ascPochhammer_eval_eq_zero_iff _ _).1 h
      exact ⟨kn, hkn, by tauto⟩
  · obtain ⟨_, h, hn⟩ := zero
    exact ordinaryHypergeometricSeries_eq_zero_of_neg_nat a b c hn h

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
z : 𝕜
hfz : (f ∘ g) z = ((fun x ↦ (x - g z₀) ^ r • F x) ∘ g) z
⊢ g z - g z₀ = (z - z₀) ^ s • G z → (f ∘ g) z = (z - z₀) ^ (r * s) • G z ^ r • F (g z)

Tactic:
hgz

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
z : 𝕜
hfz : (f ∘ g) z = ((fun x ↦ (x - g z₀) ^ r • F x) ∘ g) z
hgz : g z - g z₀ = (z - z₀) ^ s • G z
⊢ (f ∘ g) z = (z - z₀) ^ (r * s) • G z ^ r • F (g z)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Pow R ℕ
inst✝² : BinomialRing R
inst✝¹ : MulOneClass R
inst✝ : NatPowAssoc R
r : R
⊢ r ^ 0 = 1

Tactic:
npow_zero

Goal state after:
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Pow R ℕ
inst✝² : BinomialRing R
inst✝¹ : MulOneClass R
inst✝ : NatPowAssoc R
r : R
⊢ 1 = 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Pow R ℕ
inst✝² : BinomialRing R
inst✝¹ : MulOneClass R
inst✝ : NatPowAssoc R
r : R
⊢ multichoose r 1 = r

Tactic:
multichoose_one_right',

Goal state after:
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Pow R ℕ
inst✝² : BinomialRing R
inst✝¹ : MulOneClass R
inst✝ : NatPowAssoc R
r : R
⊢ r ^ 1 = r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
rw [mul_comm, ← mul_assoc]
    exact (hf.hasDerivWithinAt.const_cpow (Or.inl hc)).derivWithin h

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
⊢ (r + 1) ^ 0 = 1

Tactic:
npow_zero

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
⊢ 1 = 1
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (fun x ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
this : HasDerivWithinAt f e (Icc a b) a
⊢ HasDerivWithinAt f e (Ici a) a

Tactic:
exact this.mono_of_mem_nhdsWithin (Icc_mem_nhdsGE ab)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: 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)
this : HasDerivAt (fun y ↦ ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
⊢ HasDerivAt (fun y ↦ -↑(-y) ^ (r + 1) * cexp (↑π * I * r)) ((r + 1) * ↑(-x) ^ r * cexp (↑π * I * r)) x

Tactic:
by
      convert! this.neg.mul_const _ using 1; ring

Goal state after:
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 y ↦ ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x

Tactic:
suffices HasDerivAt (fun y : ℝ => (y : ℂ) ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x) by
      convert! @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
      rw [real_smul, ofReal_neg 1, ofReal_one]; ring

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)) ((r + 1) * ↑(-x) ^ r) (-x)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
hdx : (descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s = (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r
⊢ (r + s - k • 1) * (↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)) =
    ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ (ij.2 + 1)).smeval s) +
      ↑(k.choose ij.2) * ((descPochhammer ℤ (ij.1 + 1)).smeval r * (descPochhammer ℤ ij.2).smeval s)

Tactic:
rw [descPochhammer_succ_right, mul_comm, smeval_mul, descPochhammer_succ_right, mul_comm,
      smeval_mul, ← mul_assoc ((descPochhammer ℤ ij.1).smeval r), hdx]

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
hdx : (descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s = (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r
⊢ (r + s - k • 1) * (↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)) =
    ↑(k.choose ij.1) * ((X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s) +
      ↑(k.choose ij.2) * ((X - ↑ij.1).smeval r * (descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
⊢ (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ, (p n) fun i ↦ v (σ i)

Tactic:
let q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then (h ▸ p n) else 0

Goal state after:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
⊢ (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ, (p n) fun i ↦ v (σ i)