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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
this : IsEmpty { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑h.pairing.II
hf : ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.AncestralRel ((fun n ↦ h.equivII.symm (f n)) (n + 1)) ((fun n ↦ h.equivII.symm (f n)) n)

Tactic:
by simpa [ancestralRel_iff] using hf n

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ : h.pairing.IsRegular
this✝ : h.IsProper
this : IsEmpty { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
f : ℕ → h.ι
hf : ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.pairing.AncestralRel ((fun n ↦ h.equivII (f n)) (n + 1)) ((fun n ↦ h.equivII (f n)) n)

Tactic:
by simpa [ancestralRel_iff] using hf n

Goal state after:
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
j : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
hs : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∈ (f.sigmaStdSimplex j).nonDegenerate d
hs' : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∉ (range (f.m j)).obj (op ⦋d⦌)
h : s ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨s, h⟩) =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s

Tactic:
rw [← NatTrans.comp_app_apply]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
hs : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∈ (f.sigmaStdSimplex j).nonDegenerate d
hs' : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∉ (range (f.m j)).obj (op ⦋d⦌)
h : s ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((x.ιSigmaHorn ≫ f.m j).app (op ⦋d⦌))) ⟨s, h⟩ =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
  ⟨fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k), ⋯⟩
k : K
⊢ ↑y k =
    ↑((Types.isLimitEquivSections (hc cX.pt))
          ((ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j₁)) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s)))
      k

Tactic:
have h₁ := Types.isLimitEquivSections_apply (hc cX.pt) k
    (c.pt.map (cX.ι.app j₁) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
  ⟨fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k), ⋯⟩
k : K
h₁ :
  ↑((Types.isLimitEquivSections (hc cX.pt))
          ((ConcreteCategory.hom (c.pt.map (cX.ι.app j₁))) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s)))
      k =
    (ConcreteCategory.hom ((((evaluation C (Type w')).obj cX.pt).mapCone c).π.app k))
      ((ConcreteCategory.hom (c.pt.map (cX.ι.app j₁))) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))
⊢ ↑y k =
    ↑((Types.isLimitEquivSections (hc cX.pt))
          ((ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j₁)) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s)))
      k
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨b, hb⟩) =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b

Tactic:
rw [← NatTrans.comp_app_apply]

Goal state after:
case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((x.ιSigmaHorn ≫ f.m j).app (op ⦋d⦌))) ⟨b, hb⟩ =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b
Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
⊢ F.isDenseAt = G.isDenseAt

Tactic:
ext X
  exact ⟨fun ⟨h⟩ ↦ ⟨h.ofNatIso e⟩, fun ⟨h⟩ ↦ ⟨h.ofNatIso e.symm⟩⟩

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

Goal state before:
pp: case inl.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 c' : f.Cell j
h : P.p c.s = P.p c'.s
⊢ Cell.type₁ f c = Cell.type₁ f c'

Tactic:
obtain rfl : c = c' := by ext : 1; exact P.p.injective h
    rfl

Goal state after:
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
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
G : C' ⥤ C
inst✝ : G.IsEquivalence
⊢ (G ⋙ F).IsDense ↔ F.IsDense

Tactic:
by
  refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
  let e : G.inv ⋙ G ⋙ F ≅ F := (associator _ _ _).symm ≪≫
    isoWhiskerRight (G.asEquivalence.counitIso) _ ≪≫ F.leftUnitor
  exact of_iso e

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

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

Tactic:
rw [prevD_eq (j' := 1) (w := by simp), dNext_eq_zero _ _ (by simp), zero_add]

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H✝ H : Homotopy f g
⊢ ((alternatingFaceMapComplex C).map f).f 0 =
    ToChainHomotopy.hom H 0 1 ≫ ((alternatingFaceMapComplex C).obj Y).d 1 0 + ((alternatingFaceMapComplex C).map g).f 0
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ { hom := pushout.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯,
          inv :=
            (ρ_ X.left).inv ≫
              pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
                (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom),
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      X.hom =
    (X □ Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.right).hom

Tactic:
refine pushout.hom_ext ?_ (by simp)
    apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ (ConcreteCategory.hom (SimplicialObject.σ Δ[1] j)) (objMk₁ i) = objMk₁ i.castSucc

Tactic:
ext k : 1
  exact ConcreteCategory.congr_hom (SimplexCategory.σ_comp_toMk₁_of_le _ _ h) k

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₁ (Fin.last n))) ≫
      δ Y (Fin.last (n + 1)) =
    f.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
    · simp [dsimp% SimplexCategory.δ_comp_σ_succ (i := Fin.last n)]
    · simp [stdSimplex.δ_objMk₁_of_le, stdSimplex.objMk₁_apply_eq_zero_iff, ← Fin.castSucc_succ]

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ ∃ i, x ∈ i.subcomplex.obj (op ⦋n⦌)

Tactic:
exact ⟨N.mk x hx, Subcomplex.mem_ofSimplex_obj _⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
j : Fin (n + 2)
i : Fin n
hj : i.castSucc.succ < j
⊢ stdSimplex.δ j ≫ stdSimplex.σ i.castSucc ≫ f.map = const x

Tactic:
obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (by aesop)

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin n
j : Fin (n + 1)
hj : i.castSucc.succ < j.succ
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
x : ZerothHomotopy ↑X
⊢ SSet.π₀.lift (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) ⋯ (ZerothHomotopy.lift (SSet.π₀.mk ∘ ⇑toSSetObj₀Equiv.symm) ⋯ x) =
    x

Tactic:
by induction x; simp

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
x : (toSSet.obj X).π₀
⊢ ZerothHomotopy.lift (SSet.π₀.mk ∘ ⇑toSSetObj₀Equiv.symm) ⋯ (SSet.π₀.lift (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) ⋯ x) =
    x

Tactic:
by induction x; simp

Goal state after:
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
x₀ : R
hx₀ : x₀ ≠ 0 ∧ v x₀ < 1
hpow : ∀ (n : ℕ), 1 ≤ v a → w x₀ < w a ^ n
n : ℕ
hn : w a ^ n < w x₀
⊢ v a < 1

Tactic:
exact not_le.1 <| mt (hpow n) <| not_lt.2 hn.le

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
⊢ 0 < p.radius

Tactic:
order

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

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

Tactic:
· ext; apply hδ₁

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

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

Tactic:
· exact fun hz ↦ ⟨f, hf, hz.resolve_left <| not_not_intro hf, by simp⟩

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

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖⁻¹ *
                        ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
                      ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖⁻¹ *
                    ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹⁻¹ *
                  ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ *
                ‖↑n !‖⁻¹⁻¹ *
              ‖↑n !‖⁻¹ *
            ‖a + ↑n‖⁻¹ *
          ‖b + ↑n‖⁻¹ *
        ‖c + ↑n‖⁻¹⁻¹ *
      ‖1 + ↑n‖⁻¹⁻¹ =
    ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖

Tactic:
by
      simp only [inv_inv]
      repeat rw [DivisionRing.mul_inv_cancel, one_mul]
      all_goals
        rw [norm_ne_zero_iff]
      any_goals
        apply (ascPochhammer_eval_eq_zero_iff n _).not.2
        push Not
        exact fun kn hkn ↦ by simp [habc kn hkn]
      exact cast_ne_zero.2 (factorial_ne_zero n)

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

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹

Tactic:
mul_assoc,

Goal state after:
case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹

Tactic:
mul_assoc,

Goal state after:
case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * I * I) * 2⁻¹

Tactic:
mul_assoc,

Goal state after:
case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (I * I)) * 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv sin = cot

Tactic:
by
  ext
  rw [logDeriv, Complex.deriv_sin, Pi.div_apply, Complex.cot]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case negSucc
k n : ℕ
⊢ ↑(↑k).negOnePow * ↑((n + 1).choose k) * ↑k.factorial = (ascPochhammer ℕ k).smeval -[n+1]

Tactic:
mul_assoc,

Goal state after:
case negSucc
k n : ℕ
⊢ ↑(↑k).negOnePow * (↑((n + 1).choose k) * ↑k.factorial) = (ascPochhammer ℕ k).smeval -[n+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
f : 𝕜 → E
c : 𝕜
R : ℝ
⊢ MeromorphicOn (f ∘ fun x ↦ x - c) (ball c R) ↔ MeromorphicOn f (ball 0 R)

Tactic:
rw [meromorphicOn_comp_sub_const_iff_meromorphicOn, ball_sub_singleton, sub_self]

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) * cexp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x
| (r + 1) * (-↑x) ^ r * cexp (↑π * I * r) / (r + 1)

Tactic:
mul_assoc,

Goal state after:
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) * cexp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x
| (r + 1) * ((-↑x) ^ r * cexp (↑π * I * r)) / (r + 1)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ (p.1 ^ p.2 * (p.2 * p.1⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + (p.1 ^ p.2 * p.2 * p.1⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ

Tactic:
mul_assoc,

Goal state after:
case e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ (p.1 ^ p.2 * (p.2 * p.1⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + (p.1 ^ p.2 * (p.2 * p.1⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1

Tactic:
have H : ((binomialSeries ℂ (-a)).compContinuousLinearMap (-1)) =
      .ofScalars ℂ fun n ↦ Ring.choose (a + n - 1) n := by
    ext n; simp [FormalMultilinearSeries.compContinuousLinearMap, binomialSeries, Ring.choose_neg,
      Units.smul_def, ← pow_add, ← mul_assoc]

Goal state after:
a : ℂ
H :
  (binomialSeries ℂ (-a)).compContinuousLinearMap (-1) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    (k.choose x.1 * x.1.factorial * x.2.factorial) • (choose r x.1 * choose s x.2)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    (k.choose x.1 * (x.1.factorial * x.2.factorial)) • (choose r x.1 * choose s x.2)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    ↑(k.choose x.1) * ↑x.1.factorial * (choose r x.1 * x.2.factorial • choose s x.2)

Tactic:
simp [mul_assoc, descPochhammer_eq_factorial_smul_choose]

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

Goal state before:
pp: case inr
p : ℝ
h : 1 ≤ p
⊢ HasDerivAt (fun x ↦ x ^ p) (p * 0 ^ (p - 1)) 0

Tactic:
apply hasDerivAt_of_hasDerivAt_of_ne fun x hx =>
    (hasStrictDerivAt_rpow_const_of_ne hx p).hasDerivAt

Goal state after:
case inr.hf
p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (fun x ↦ x ^ p) 0

case inr.hg
p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (fun x ↦ p * x ^ (p - 1)) 0
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
n✝ : ℕ
⊢ ((binomialSeries ℝ a n✝) fun x ↦ 1) =
    (Complex.reCLM.compFormalMultilinearSeries ((binomialSeries ℂ a).compContinuousLinearMap Complex.ofRealCLM) n✝)
      fun x ↦ 1

Tactic:
simp [Function.comp_def]

Goal state after:
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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) = iteratedFDerivWithin 𝕜 n f s x

Tactic:
by
  ext
  exact h.iteratedFDerivWithin_comp_perm hs hx _ _

Goal state after:
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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) = iteratedFDerivWithin 𝕜 n f s x

Tactic:
by
  ext
  exact h.iteratedFDerivWithin_comp_perm hs hx _ _

Goal state after: