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

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
⊢ δ j ≫ toMk₁ i.succ = toMk₁ i

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Goal state after:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (δ j ≫ toMk₁ i.succ)) k = (ConcreteCategory.hom (toMk₁ i)) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ σ j ≫ toMk₁ i = toMk₁ i.castSucc

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ (ConcreteCategory.hom (σ j ≫ toMk₁ i)) k = (ConcreteCategory.hom (toMk₁ i.castSucc)) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ σ j ≫ toMk₁ i = toMk₁ i.succ

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
⊢ (ConcreteCategory.hom (σ j ≫ toMk₁ i)) k = (ConcreteCategory.hom (toMk₁ i.succ)) k
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
hx : x ∈ P.I
hy : ↑⟨x, hx⟩ ∈ P.II
⊢ False

Tactic:
have : x ∈ P.I ∩ P.II := ⟨hx, hy⟩

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
hx : x ∈ P.I
hy : ↑⟨x, hx⟩ ∈ P.II
this : x ∈ P.I ∩ P.II
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i j : Fin (n + 2)
hij : (ConcreteCategory.hom (SimplicialObject.δ X i)) x = (ConcreteCategory.hom (SimplicialObject.δ X j)) x
⊢ SimplexCategory.δ i = SimplexCategory.δ j

Tactic:
apply stdSimplex.objEquiv.symm.injective

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i j : Fin (n + 2)
hij : (ConcreteCategory.hom (SimplicialObject.δ X i)) x = (ConcreteCategory.hom (SimplicialObject.δ X j)) x
⊢ stdSimplex.objEquiv.symm (SimplexCategory.δ i) = stdSimplex.objEquiv.symm (SimplexCategory.δ j)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (X.map (monoOfLE h).op)) y.simplex) = yonedaEquiv.symm x.simplex

Tactic:
map_monoOfLE

Goal state after:
X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
⊢ yonedaEquiv.symm x.simplex = yonedaEquiv.symm x.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s + 1, simplex := h.simplex s }
⊢ x = h.type₁ s

Tactic:
by rwa [N.ext_iff, SSet.N.ext_iff]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index s))) (h.simplex s) }
⊢ x = h.type₂ s

Tactic:
by rwa [N.ext_iff, SSet.N.ext_iff]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.pairing.IsRegular ↔ h.IsRegular

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsRegular
⊢ h.IsRegular
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
⊢ ⨆ j, Subcomplex.range (c.ι.app j) = ⊤

Tactic:
ext n x

Goal state after:
J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
n : SimplexCategoryᵒᵖ
x : c.1.obj n
⊢ x ∈ (⨆ j, Subcomplex.range (c.ι.app j)).obj n ↔ x ∈ ⊤.obj n
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ (X ⨿ Y).Finite

Tactic:
by
  apply finite_of_isColimit (coprodIsCoprod X Y)
  rintro ⟨_ | _⟩ <;> dsimp <;> infer_instance

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

Goal state before:
pp: case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
hd : x.dim ≤ x.dim
i : Fin (x.dim + 2)
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) ∈
    (f.sigmaStdSimplex j).nonDegenerate x.dim
hs : Mono (SimplexCategory.δ i)
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) ∉
    (range (f.m j)).obj (op ⦋x.dim⦌)
hs' : stdSimplex.objEquiv.symm (SimplexCategory.δ i) ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)))
          hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.δ i)))
          hs✝ hs'✝ =
        Cell.type₂ f c

Tactic:
obtain rfl := (objEquiv_symm_δ_notMem_horn_iff _ _).mp hs'

Goal state after:
case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
hd : x.dim ≤ x.dim
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ x.index)) ∈
    (f.sigmaStdSimplex j).nonDegenerate x.dim
hs : Mono (SimplexCategory.δ x.index)
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ x.index)) ∉
    (range (f.m j)).obj (op ⦋x.dim⦌)
hs' : stdSimplex.objEquiv.symm (SimplexCategory.δ x.index) ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim⦌)
⊢ ∃ c,
    N.mk
          ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.δ x.index)))
          hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.δ x.index)))
          hs✝ hs'✝ =
        Cell.type₂ f c
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
hQ : ∀ (J : Type w) [inst : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J
h : P ≤ Q
this : ∀ (i : SmallCategoryCardinalLT κ), Q.IsClosedUnderColimitsOfShape (SmallCategoryCardinalLT.categoryFamily κ i)
⊢ P.colimitsCardinalClosure κ ≤ Q

Tactic:
exact colimitsClosure_le h

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:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Goal state after:
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
x✝ : (G ⋙ F).IsDense
⊢ F.IsDense
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 : D ⥤ C'
inst✝ : G.IsEquivalence
⊢ (F ⋙ G).IsDense ↔ F.IsDense

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Goal state after:
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 : D ⥤ C'
inst✝ : G.IsEquivalence
x✝ : (F ⋙ G).IsDense
⊢ F.IsDense
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
this : IsCardinalPresentable G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
⊢ ∃ j φ₁ φ₂, φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂

Tactic:
obtain ⟨j₂, f₂, hf₂⟩ :=
          IsCardinalPresentable.exists_hom_of_isColimit κ (colimit.isColimit _) g₂

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
this : IsCardinalPresentable G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ ∃ j φ₁ φ₂, φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
hA : strongInnerAnodyneExtensions A.ι
⊢ ∃ P, ∃ (x : P.IsRegular), P.IsInner

Tactic:
by
    obtain ⟨_, P, _, ⟨_, rfl⟩⟩ :
        ∃ (B : X.Subcomplex) (P : B.Pairing) (h : P.IsRegular), P.IsInner ∧ B = A := by
      obtain ⟨_, P₁, _, P₂⟩ := hA
      exact ⟨_, P₁, inferInstance, ⟨P₂, by simp⟩⟩
    exact ⟨P, ⟨inferInstance, inferInstance⟩⟩

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasColimitsOfSize.{w, w, v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : IsCardinalLocallyPresentable C κ
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasColimitsOfSize.{w, w, v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ IsCardinalLocallyPresentable C κ

Tactic:
· obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_small_generator C κ
    exact ⟨_, inferInstance, hP.isStrongGenerator, hP.le_isCardinalPresentable⟩

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasColimitsOfSize.{w, w, v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ IsCardinalLocallyPresentable C κ
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

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₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝² x✝¹ : Arrow C₃
x✝ : x✝² ⟶ x✝¹
⊢ (G.leibnizPullback.obj (op X₁) ⋙ F.leibnizPushout.obj X₁).map x✝ ≫
      Arrow.homMk
        (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝¹).left))
          (adj₂.homEquiv.symm
            (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom) ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
          ⋯)
        (adj₂.homEquiv.symm
          (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom) ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
        ⋯ =
    Arrow.homMk
        (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝²).left))
          (adj₂.homEquiv.symm
            (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝².hom) ((G.map (unop (op X₁)).hom.op).app x✝².right)))
          ⋯)
        (adj₂.homEquiv.symm
          (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝².hom) ((G.map (unop (op X₁)).hom.op).app x✝².right)))
        ⋯ ≫
      (𝟭 (Arrow C₃)).map x✝

Tactic:
ext
    · apply pushout.hom_ext <;> simp [← homEquiv_symm_naturality_two,
        ← homEquiv_symm_naturality_three]
    · simp [← homEquiv_symm_naturality_two, ← homEquiv_symm_naturality_three]

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

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

Tactic:
simp [SimplexCategory.δ_comp_σ_of_gt hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]
      rfl

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

Goal state before:
pp: ⊢ HasFPowerSeriesAt (fun x ↦ log (1 + x)) (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 0

Tactic:
convert HasFPowerSeriesAt.comp_sub hasFPowerSeriesAt_clog_one (-1) using 3

Goal state after:
case e'_9
x✝ : ℂ
⊢ 1 + x✝ = x✝ - -1

case e'_11
⊢ 0 = 1 + -1
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      0 ^ n =
    Pi.single 0 1 n

Tactic:
cases n <;> simp

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
⊢ (∀ (m : ℕ), ↑m + 1 ≤ analyticOrderAt f z₀) ↔ ∀ (m : ℕ), ↑m ≤ analyticOrderAt f z₀

Tactic:
exact ⟨fun h m ↦ le_self_add.trans (h m), fun h m ↦ h (m + 1)⟩

Goal state after:
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
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : y ∉ {z₀}
⊢ f y = 0

Tactic:
Set.mem_singleton_iff,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : ¬y = z₀
⊢ f y = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
hU : IsConnected U
⊢ (∃ u, analyticOrderAt f ↑u ≠ ⊤) ↔ ∀ (u : ↑U), analyticOrderAt f ↑u ≠ ⊤

Tactic:
have : ConnectedSpace U := Subtype.connectedSpace hU
  obtain ⟨v⟩ : Nonempty U := inferInstance
  suffices (∀ (u : U), analyticOrderAt f u ≠ ⊤) ∨ ∀ (u : U), analyticOrderAt f u = ⊤ by tauto
  simpa [Set.eq_empty_iff_forall_notMem, Set.eq_univ_iff_forall] using
      isClopen_iff.1 hf.isClopen_setOfPred_analyticOrderAt_eq_top

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

Goal state before:
pp: a : ℂ
n : ℕ
⊢ Ring.choose a n = iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !

Tactic:
eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero]),

Goal state after:
a : ℂ
n : ℕ
⊢ Ring.choose a n * ↑n ! = iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0
Module: Mathlib.Analysis.Analytic.RadiusLiminf

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
⊢ 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)

Tactic:
hn

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
⊢ ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1
Module: Mathlib.Analysis.Analytic.RadiusLiminf

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
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
n : ℕ
⊢ ↑r < 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) → 0 < n → ‖‖p n‖ * ↑r ^ n‖ ≤ 1

Tactic:
hn

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
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
n : ℕ
hn : ↑r < 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
⊢ 0 < n → ‖‖p n‖ * ↑r ^ n‖ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case pos
x y : ℝ≥0∞
h : x < y
h✝¹ : x = 0
h✝ : y = 0
⊢ ⊥ < ⊥

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case pos
x y : ℝ≥0∞
h : x < y
h✝² : x = 0
h✝¹ : ¬y = 0
h✝ : y = ∞
⊢ ⊥ < ⊤

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case neg
x y : ℝ≥0∞
h : x < y
h✝² : x = 0
h✝¹ : ¬y = 0
h✝ : ¬y = ∞
⊢ ⊥ < ↑(Real.log y.toReal)

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case pos
x y : ℝ≥0∞
h : x < y
h✝² : ¬x = 0
h✝¹ : x = ∞
h✝ : y = 0
⊢ ⊤ < ⊥

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case pos
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : x = ∞
h✝¹ : ¬y = 0
h✝ : y = ∞
⊢ ⊤ < ⊤

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case neg
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : x = ∞
h✝¹ : ¬y = 0
h✝ : ¬y = ∞
⊢ ⊤ < ↑(Real.log y.toReal)

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case pos
x y : ℝ≥0∞
h : x < y
h✝² : ¬x = 0
h✝¹ : ¬x = ∞
h✝ : y = 0
⊢ ↑(Real.log x.toReal) < ⊥

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case pos
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : ¬x = ∞
h✝¹ : ¬y = 0
h✝ : y = ∞
⊢ ↑(Real.log x.toReal) < ⊤

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case neg
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : ¬x = ∞
h✝¹ : ¬y = 0
h✝ : ¬y = ∞
⊢ ↑(Real.log x.toReal) < ↑(Real.log y.toReal)

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ ∞ = ∞ * ENNReal.ofReal (Real.exp a✝)

Tactic:
rw [ENNReal.top_mul]

Goal state after:
case top.coe
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: x y : EReal
⊢ (x + y).exp = x.exp * y.exp

Tactic:
induction x
  · simp
  · induction y
    · simp
    · simp only [← EReal.coe_add, exp_coe]
      rw [← ENNReal.ofReal_mul (Real.exp_nonneg _), Real.exp_add]
    · simp only [EReal.coe_add_top, exp_top, exp_coe]
      rw [ENNReal.mul_top]
      simp [Real.exp_pos]
  · induction y
    · simp
    · simp only [EReal.top_add_coe, exp_top, exp_coe]
      rw [ENNReal.top_mul]
      simp [Real.exp_pos]
    · simp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f)

Tactic:
induction n with
  | zero => simpa only [one_mul, pow_zero] using hf
  | succ n hn => simpa only [pow_succ', mul_assoc] using hn.param_mul

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
P : Set X → Prop
⊢ (∃ᶠ (t : Set X) in v.filterAt x, P t) ↔ ∀ ε > 0, ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ P t

Tactic:
by
  simp only [(v.filterAt_basis_closedBall x).frequently_iff, ← and_assoc, subset_def, mem_ofPred]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u ⊔ v) = max (expGrowthSup u) (expGrowthSup v)

Tactic:
rw [expGrowthSup, expGrowthSup, expGrowthSup, ← limsup_max]
  refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
  rw [Pi.sup_apply, log_monotone.map_max]
  exact (monotone_div_right_of_nonneg n.cast_nonneg').map_max

Goal state after: