Tests for the tendsto_cont tactic

The #guard_msgs tests in this file are sensitive to any other diagnostics emitted at the guarded commands, so this file must keep a style-conformant header (otherwise linter.style.header warnings can leak into the #guard_msgs output and fail CI).

@[reducible, inline]

noncomputable abbrev myExpr (f g : ℝ → ℝ) : ℝ → ℝ

Equations

• myExpr f g z = f z ^ 2 + g z

@[reducible, inline]

noncomputable abbrev myExprMul (f g : ℝ → ℝ) : ℝ → ℝ

Equations

• myExprMul f g z = f z * g z

theorem notATendstoTheorem : True

theorem paramTendsto (_h : True) : Filter.Tendsto (fun (x : ℝ) => 0) Filter.atTop (nhds 0)

theorem wrongTargetFilter : Filter.Tendsto (fun (z : ℝ) => z) Filter.atTop Filter.atTop

theorem testScopeRejection : Filter.Tendsto (fun (x : ℝ) => 0) Filter.atTop (nhds 0)

@[implicit_reducible]

def instTopologicalSpaceBool_spherePacking : TopologicalSpace Bool

Equations

• instTopologicalSpaceBool_spherePacking = ⊤

@[implicit_reducible]

def instTopologicalSpaceBool_spherePacking_1 : TopologicalSpace Bool

Equations

• instTopologicalSpaceBool_spherePacking_1 = TopologicalSpace.mkOfNhds (Function.update pure false ⊤)