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

Goal state before:
pp: case h_fst
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

pp: case h_snd
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
<;>

Goal state after:
case h_fst
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

case h_snd
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: case h_fst
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

pp: case h_snd
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
<;>

Goal state after:
case h_fst
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

case h_snd
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj 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
⊢ Dense sᶜ

Tactic:
← interior_eq_empty_iff_dense_compl

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
⊢ interior s = ∅
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₁ : v (b ^ q.den / a ^ q.num) < 1
hq₂ : log (w a ^ q.num) < log (w b ^ q.den)
⊢ False

Tactic:
log_lt_log_iff (zpow_pos (by linarith) _) (pow_pos (by linarith) _),

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₁ : v (b ^ q.den / a ^ q.num) < 1
hq₂ : w a ^ q.num < w b ^ q.den
⊢ False
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
⊢ v.IsEquiv w ↔ ∃ c, 0 < c ∧ (fun x ↦ v x ^ c) = ⇑w

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨t, ht, h⟩ ↦ isEquiv_iff_lt_one_iff.2
    fun x ↦ h ▸ (rpow_lt_one_iff' (v.nonneg x) ht).symm⟩

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
⊢ ∃ c, 0 < c ∧ (fun x ↦ v x ^ c) = ⇑w
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inl
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
⊢ v 0 ^ 1 = w 0

pp: case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
x : F
h₀ : x ≠ 0
⊢ v x ^ 1 = w x

Tactic:
<;>

Goal state after:
case inl
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
⊢ v 0 ^ 1 = w 0

case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
x : F
h₀ : x ≠ 0
⊢ v x ^ 1 = w x
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₀ : 𝕜
h : AnalyticAt 𝕜 f z₀
h✝ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
hf : ⊤ = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
h : AnalyticAt 𝕜 f z₀
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
hf : ↑⋯.choose = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
h : ¬AnalyticAt 𝕜 f z₀
hf : 0 = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
h : AnalyticAt 𝕜 f z₀
h✝ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
hf : ⊤ = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
h : AnalyticAt 𝕜 f z₀
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
hf : ↑⋯.choose = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
h : ¬AnalyticAt 𝕜 f z₀
hf : 0 = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
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 : analyticOrderAt f z₀ ≠ 0
hf' : AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ 0
hf' : ¬AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ 0
hf' : AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ 0
hf' : ¬AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0
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 : analyticOrderAt f z₀ ≠ 0
hf' : AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

Tactic:
simp_all [analyticOrderAt_eq_zero]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ 0
hf' : ¬AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

Tactic:
simp_all [analyticOrderAt_eq_zero]

Goal state after:
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 : analyticOrderNatAt f z₀ ≠ 0
hf' : AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderNatAt f z₀ ≠ 0
hf' : ¬AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderNatAt f z₀ ≠ 0
hf' : AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderNatAt f z₀ ≠ 0
hf' : ¬AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg✝ : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)

Tactic:
· simpa [hfg.le] using analyticOrderAt_add_eq_left_of_lt hfg

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g 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 : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this✝ : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
this : analyticOrderAt (fun y ↦ (s + 1) • (y - x) ^ s • F y) x = ↑s
⊢ analyticOrderAt (fun x_1 ↦ (x_1 - x) ^ (s + 1) • deriv F x_1 + (s + 1) • (x_1 - x) ^ s • F x_1) x = ↑s

Tactic:
rwa [← Pi.add_def, analyticOrderAt_add_eq_right_of_lt]

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 = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this✝ : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
this : analyticOrderAt (fun y ↦ (s + 1) • (y - x) ^ s • F y) x = ↑s
⊢ analyticOrderAt (fun x_1 ↦ (s + 1) • (x_1 - x) ^ s • F x_1) x <
    analyticOrderAt (fun x_1 ↦ (x_1 - x) ^ (s + 1) • deriv F x_1) x
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
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ (toOpenPartialHomeomorph f univ hf hc ⋯).target = univ

Tactic:
rw [toOpenPartialHomeomorph_target, image_univ, range_eq_univ]

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

Goal state before:
pp: case convert_3
this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ CompleteSpace ℂ

pp: case convert_4
this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ CharZero ℂ

pp: case convert_7
this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ AnalyticAt ℂ log 1

Tactic:
<;>

Goal state after:
case convert_3
this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ CompleteSpace ℂ

case convert_4
this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ CharZero ℂ

case convert_7
this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ AnalyticAt ℂ log 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

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

pp: case e'_11
⊢ 0 = 1 + -1

Tactic:
<;>

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

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

Goal state before:
pp: case e'_9
x✝ : ℝ
⊢ 1 + x✝ = x✝ - -1

pp: case e'_11
⊢ 0 = 1 + -1

Tactic:
<;>

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: 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

pp: 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)

Tactic:
<;>

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.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case h₁
X Y : SSet
m : ℕ
⊢ (prodComparison hoFunctor X Δ[m] ≫ prod.fst).toFunctor =
    ((hoFunctor.map (prod.braiding X Δ[m]).hom ≫
          prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom) ≫
        prod.fst).toFunctor

pp: case h₂
X Y : SSet
m : ℕ
⊢ (prodComparison hoFunctor X Δ[m] ≫ prod.snd).toFunctor =
    ((hoFunctor.map (prod.braiding X Δ[m]).hom ≫
          prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom) ≫
        prod.snd).toFunctor

Tactic:
<;>

Goal state after:
case h₁
X Y : SSet
m : ℕ
⊢ (prodComparison hoFunctor X Δ[m] ≫ prod.fst).toFunctor =
    ((hoFunctor.map (prod.braiding X Δ[m]).hom ≫
          prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom) ≫
        prod.fst).toFunctor

case h₂
X Y : SSet
m : ℕ
⊢ (prodComparison hoFunctor X Δ[m] ≫ prod.snd).toFunctor =
    ((hoFunctor.map (prod.braiding X Δ[m]).hom ≫
          prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom) ≫
        prod.snd).toFunctor
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

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

Tactic:
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: case neg
𝕜 : 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₀ = ⊤
this : analyticOrderAt (fun x ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : ¬f (g z₀) = 0
⊢ analyticOrderAt (f ∘ g) z₀ = 0

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₀ = ⊤
this : analyticOrderAt (fun x ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : ¬f (g z₀) = 0
⊢ analyticOrderAt f (g z₀) = 0

Tactic:
<;>

Goal state after:
case neg
𝕜 : 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₀ = ⊤
this : analyticOrderAt (fun x ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : ¬f (g z₀) = 0
⊢ analyticOrderAt (f ∘ g) z₀ = 0

𝕜 : 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₀ = ⊤
this : analyticOrderAt (fun x ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : ¬f (g z₀) = 0
⊢ analyticOrderAt f (g z₀) = 0
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ↑n ! ≠ 0

Tactic:
apply (ascPochhammer_eval_eq_zero_iff n _).not.2
        push Not
        exact fun kn hkn ↦ by simp [habc kn hkn]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ↑n ! ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval c (ascPochhammer 𝕂 n) ≠ 0

Tactic:
apply (ascPochhammer_eval_eq_zero_iff n _).not.2
        push Not
        exact fun kn hkn ↦ by simp [habc kn hkn]

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

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval b (ascPochhammer 𝕂 n) ≠ 0

Tactic:
apply (ascPochhammer_eval_eq_zero_iff n _).not.2
        push Not
        exact fun kn hkn ↦ by simp [habc kn hkn]

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

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval a (ascPochhammer 𝕂 n) ≠ 0

Tactic:
apply (ascPochhammer_eval_eq_zero_iff n _).not.2
        push Not
        exact fun kn hkn ↦ by simp [habc kn hkn]

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

Goal state before:
pp: case convert_5.hf
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ Tendsto (fun x ↦ (c + ↑x) / (a + ↑x)) atTop (𝓝 1)

pp: case convert_5.hg
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ Tendsto (fun x ↦ (1 + ↑x) / (b + ↑x)) atTop (𝓝 1)

Tactic:
<;>

Goal state after:
case convert_5.hf
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ Tendsto (fun x ↦ (c + ↑x) / (a + ↑x)) atTop (𝓝 1)

case convert_5.hg
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ Tendsto (fun x ↦ (1 + ↑x) / (b + ↑x)) atTop (𝓝 1)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 1 n = 1
⊢ multichoose (0 + 1) (n + 1) = 0 + 1

Tactic:
multichoose_succ_succ,

Goal state after:
case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 1 n = 1
⊢ multichoose 0 (n + 1) + multichoose (0 + 1) n = 0 + 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 2 n = ↑n + 1
⊢ multichoose (1 + 1) (n + 1) = ↑(n + 1) + 1

Tactic:
multichoose_succ_succ,

Goal state after:
case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 2 n = ↑n + 1
⊢ multichoose 1 (n + 1) + multichoose (1 + 1) n = ↑(n + 1) + 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
⊢ (ascPochhammer ℕ k).smeval ↑n = ↑((ascPochhammer ℕ k).smeval n)

Tactic:
smeval_at_natCast (ascPochhammer ℕ k) n

Goal state after:
R : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
⊢ ↑((ascPochhammer ℕ k).smeval n) = ↑((ascPochhammer ℕ k).smeval n)