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

Goal state before:
pp: case inl.inr.refine_3
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
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
this : φ x hd ((min x hd).castSucc.succAbove (min x hd)) = (objEquiv (x.cast hd).simplex) (min x hd)
⊢ (x.cast hd).simplex.1 i.succ = k.succ

Tactic:
rw [Fin.succAbove_castSucc_self] at this

Goal state after:
case inl.inr.refine_3
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
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
this : φ x hd (min x hd).succ = (objEquiv (x.cast hd).simplex) (min x hd)
⊢ (x.cast hd).simplex.1 i.succ = k.succ
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: 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₃) ≅ X₁ □ X₂ □ X₃

Tactic:
refine Arrow.isoMk ?_ (α_ _ _ _) ?_
  · refine Iso.mk ?_ ?_ ?_ ?_
    · exact pushout.desc ((α_ _ _ _).hom ≫ _ ◁ pushout.inl _ _ ≫ pushout.inl _ _)
        ((whiskerRightIso _ _).hom.left ≫
          pushout.desc (_ ◁ pushout.inr _ _ ≫ pushout.inl _ _) (pushout.inr _ _)
          (by simp [Limits.pushout.associator_naturality_left_condition]))
        (((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
          (by simp [Limits.pushout.whiskerLeft_condition_assoc, ← whisker_exchange_assoc,
            ← comp_whiskerRight_assoc])
          (by simp [← whisker_exchange_assoc, Limits.pushout.associator_naturality_left_condition,
            ← comp_whiskerRight_assoc]))
    · 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]))
    · apply pushout.hom_ext (by simp)
      apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;> simp
    · refine pushout.hom_ext ?_ (by simp)
      apply ((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;> simp
  · apply pushout.hom_ext (by simp [← MonoidalCategory.whiskerLeft_comp])
    · apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
      · simp [← MonoidalCategory.whiskerLeft_comp, ← MonoidalCategory.comp_whiskerRight_assoc]
      · simp [← MonoidalCategory.comp_whiskerRight_assoc]

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

Goal state before:
pp: X : SSet
hX : ¬X.Nonempty
⊢ IsInitial X

Tactic:
simp only [not_nonempty_iff] at hX
  have (n : SimplexCategoryᵒᵖ) : IsEmpty (X.obj n) :=
    Function.isEmpty (X.map (⦋0⦌.const n.unop 0).op)
  exact IsInitial.ofUniqueHom (fun _ ↦
    { app _ := ↾fun x ↦ isEmptyElim x
      naturality _ _ _  := by ext x; exact isEmptyElim x })
    (fun _ _ ↦ by ext _ x; exact isEmptyElim x)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

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₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝ : Arrow C₂
⊢ Arrow.Hom.right
      ((F.leibnizPushout.obj X₁).map
          ({
                app := fun X₂ ↦
                  Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                    (pullback.lift
                      (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                      (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯)
                    ⋯,
                naturality := ⋯ }.app
            x✝) ≫
        {
              app := fun 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)))
                  ⋯,
              naturality := ⋯ }.app
          ((F.leibnizPushout.obj X₁).obj x✝)) =
    Arrow.Hom.right (𝟙 ((F.leibnizPushout.obj X₁).obj x✝))

Tactic:
simp [← homEquiv_symm_naturality_two]

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

Goal state before:
pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
g : X.PtSimplex (n + 1) x
i : Fin (n + 2)
⊢ boundary.ι i ≫ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)) =
    boundary.ι i ≫ const ⟨opObjEquiv.symm x, ⋯⟩ ≫ (Subcomplex.ofSimplex (opObjEquiv.symm x)).ι

Tactic:
simp [stdSimplex.δ_comp_yonedaEquiv_symm, op_δ,
            ← stdSimplex.yonedaEquiv_δ_comp,
            opObjEquiv_symm_yonedaEquiv_const]

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
j : Fin (n + 2)
hj : i.succ < j
⊢ stdSimplex.δ j ≫ r.map = const x

Tactic:
rw [δ_map_of_gt _ j hj]

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

Goal state before:
pp: ⊢ stdSimplex.δ 1 ≫ toSSetObjI = SSet.const (TopCat.toSSetObj₀Equiv.symm 0)

Tactic:
dsimp only [toSSetObjI, toTopObjIsoI, TopCat.stdSimplexHomeomorphI]
  rw [← Adjunction.homEquiv_naturality_left, sSetTopAdj_homEquiv_stdSimplex_zero]
  congr 2
  have : stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo
      (((toTop.{u}.map (stdSimplex.δ 1)).hom) default)) = 0 := by
    rw [← stdSimplexHomeomorphUnitInterval_zero]
    congr 1
    refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_
    rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]
    rfl
  exact congr_arg ULift.up.{u} this

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

Goal state before:
pp: X : TopCat
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₀

Tactic:
rw [← cancel_mono (μIso _ _ _).inv, Category.assoc, Category.assoc, μIso_inv,
    μ_δ, Category.comp_id]

Goal state after:
X : TopCat
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₁

Tactic:
rw [← cancel_mono (μIso _ _ _).inv, Category.assoc, Category.assoc, μIso_inv,
    μ_δ, Category.comp_id]

Goal state after:
X : TopCat
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
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
⊢ interior s = ∅

Tactic:
by_contra H

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 = ∅
⊢ False
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)
hg : HasFPowerSeriesOnBall g p x p.radius
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
hf : HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x
⊢ ∃ ε > 0, Metric.eball x ε ⊆ {x | (fun x ↦ f x = g x) x}

Tactic:
obtain ⟨ε, hf⟩ := hf

Goal state after:
𝕜 : 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)
hg : HasFPowerSeriesOnBall g p x p.radius
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
ε : ENNReal
hf : HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x ε
⊢ ∃ ε > 0, Metric.eball x ε ⊆ {x | (fun x ↦ f x = g x) x}
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: case h₂.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ sphere x r
H : y = x
⊢ False

Tactic:
simp only [H, mem_sphere_iff_norm, sub_self, norm_zero] at hy

Goal state after:
case h₂.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
H : y = x
hy : 0 = r
⊢ False
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : log (v b) / log (v a) < ↑q
hq₂ : ↑q < log (w b) / log (w a)
⊢ False

Tactic:
← Rat.num_div_den q,

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : log (v b) / log (v a) < ↑(↑q.num / ↑q.den)
hq₂ : ↑(↑q.num / ↑q.den) < log (w b) / log (w a)
⊢ False
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀

Tactic:
refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_
    simp only [natCast_le_analyticOrderAt, hf, hf.neg]
    exact (Equiv.neg _).exists_congr <| by simp [neg_eq_iff_eq_neg]

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 : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R ↦ closedBall (f 0) R ⊆ range f
hr✝ : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall 0 r ⊆ univ

Tactic:
exact subset_univ _

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

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
s : X.obj (op { obj := ⦋1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom ((homToNerveMk (descOfTruncation φ)).app (op { obj := ⦋1⦌, property := ⋯ }))) s =
    (ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) s

Tactic:
obtain ⟨x₀, x₁, f, rfl⟩ := Edge.exists_of_simplex s

Goal state after:
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ConcreteCategory.hom ((homToNerveMk (descOfTruncation φ)).app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝¹ : SmallCategory C
D : Type u
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
s : X.obj (op { obj := ⦋1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom ((homToNerveMk (F ⋙ G)).app (op { obj := ⦋1⦌, property := ⋯ }))) s =
    (ConcreteCategory.hom ((homToNerveMk F ≫ (truncation 2).map (nerveMap G)).app (op { obj := ⦋1⦌, property := ⋯ }))) s

Tactic:
obtain ⟨x₀, x₁, f, rfl⟩ := Edge.exists_of_simplex s

Goal state after:
X : Truncated 2
C : Type u
inst✝¹ : SmallCategory C
D : Type u
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ConcreteCategory.hom ((homToNerveMk (F ⋙ G)).app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom ((homToNerveMk F ≫ (truncation 2).map (nerveMap G)).app (op { obj := ⦋1⦌, property := ⋯ })))
      f.edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ homEquiv ((edgeMk (f ≫ g)).toTruncated.map φ) =
    homEquiv ((edgeMk f).toTruncated.map φ) ≫ homEquiv ((edgeMk g).toTruncated.map φ)

Tactic:
obtain ⟨h⟩ := (nerve.nonempty_compStruct_iff f g (f ≫ g)).2 rfl
    exact (nerve.homEquiv_comp (h.toTruncated.map φ)).symm

Goal state after:
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

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

case succ
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n✝ : ℕ
⊢ ((↑(n✝ + 1)!)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 (n✝ + 1)) * Polynomial.eval b (ascPochhammer 𝕂 (n✝ + 1)) *
        (Polynomial.eval c (ascPochhammer 𝕂 (n✝ + 1)))⁻¹) •
      0 ^ (n✝ + 1) =
    Pi.single 0 1 (n✝ + 1)
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ HasFDerivWithinAt f f' (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) x

Tactic:
hasFDerivWithinAt_iff_isLittleO,

Goal state after:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (fun x' ↦ f x' - f x - f' (x' - x)) =o[𝓝[closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s] x] fun x' ↦
    x' - x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: n : ℕ
x : ℝ
⊢ |iteratedDeriv 1 sin x| ≤ 1

Tactic:
simpa using Real.abs_cos_le_one x

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

Goal state before:
pp: n : ℕ
x : ℝ
⊢ |iteratedDeriv 0 cos x| ≤ 1

Tactic:
simpa using Real.abs_cos_le_one x

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Module ℚ≥0 R
inst✝ : Pow R ℕ
r : R
n : ℕ
⊢ n.factorial • (↑n.factorial)⁻¹ • (ascPochhammer ℕ n).smeval r = (ascPochhammer ℕ n).smeval r

Tactic:
by
    match_scalars
    field

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
U : Set 𝕜
inst✝¹ : SecondCountableTopology 𝕜
inst✝ : CompleteSpace E
h : MeromorphicOn f U
⊢ {z | AnalyticAt 𝕜 f z}ᶜᶜ ∈ codiscreteWithin U

Tactic:
simpa using! eventually_codiscreteWithin_analyticAt f h

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

Goal state before:
pp: case pos
𝕂 : Type u_1
inst✝² : RCLike 𝕂
𝔸 : Type u_2
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
⊢ 1 ≤ (binomialSeries 𝔸 a).radius

Tactic:
binomialSeries_radius_eq_one ha

Goal state after:
case pos
𝕂 : Type u_1
inst✝² : RCLike 𝕂
𝔸 : Type u_2
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
⊢ 1 ≤ 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
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| (r ^ ↑n * ‖p n‖₊) ^ (↑n)⁻¹ ≤ 1 ^ (↑n)⁻¹

Tactic:
NNReal.rpow_le_rpow_iff (inv_pos.2 this),

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
this : 0 < ↑n
| r ^ ↑n * ‖p n‖₊ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: ⊢ Function.Surjective log

Tactic:
by
  intro y
  cases y with
  | bot => use 0; simp
  | top => use ⊤; simp
  | coe y => use ENNReal.ofReal (Real.exp y); simp [Real.exp_pos]

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

Goal state before:
pp: case inr.inl.inl
⊢ (∞ * 0).log = ⊤ + log 0

Tactic:
rw [mul_zero, log_zero, EReal.add_bot]

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

Goal state before:
pp: case e'_5
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ = ⊤ * b.log

pp: case convert_2
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊥

pp: case convert_3
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊤

Tactic:
· rw [EReal.top_mul_of_pos (zero_lt_log_iff.2 hb)]

Goal state after:
case convert_2
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊥

case convert_3
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊤
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a ↦ k a ^ z)⁻¹ = fun a ↦ k a ^ (-z)
⊢ Tendsto (f / fun a ↦ k a ^ z) l (𝓝 0)

Tactic:
rw [div_eq_mul_inv, mul_comm f, this]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a ↦ k a ^ z)⁻¹ = fun a ↦ k a ^ (-z)
⊢ Tendsto ((fun a ↦ k a ^ (-z)) * f) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : μ t = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∉ t

Tactic:
change μ _ = 0

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : μ t = 0
⊢ μ {x | (fun x ↦ x ∉ t) x}ᶜ = 0