tendsto_cont tactic

A tactic for proving goals of the form Tendsto (fun z => expr(f₁ z, ..., fₙ z)) l (nhds c) where atomic limits Tendsto fᵢ l (nhds aᵢ) are known from context and the expression is continuous in the atoms (proved via fun_prop).

This handles any expression where fun_prop can prove continuity of the abstracted body — including polynomials, trigonometric functions, exponentials, and other compositions.

Strategy

1. Parse the goal to extract the body, filter, and target limit.
2. Scan context for Tendsto hypotheses matching the goal filter.
3. Identify which atoms appear in the goal body.
4. Bundle atoms into a right-associated product via prodMk_nhds.
5. Abstract the body: replace fᵢ(z) with projections from the product.
6. Prove continuity of the abstracted function via fun_prop.
7. Combine via tendsto_continuousAt_comp and close the goal.

theorem tendsto_continuousAt_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] {l : Filter α} {f : α → β} {h : β → γ} {b : β} (hh : ContinuousAt h b) (hf : Filter.Tendsto f l (nhds b)) : Filter.Tendsto (fun (x : α) => h (f x)) l (nhds (h b))

Compose a continuous function with a convergent one. Stated with an explicit lambda (no Function.comp) so the kernel sees the right type.

structure TendstoCont.Atom : Type

An atom: a context hypothesis Tendsto f l (nhds a) appearing in the goal body.

• fn : Lean.Expr
• limit : Lean.Expr
• hyp : Lean.Expr
• codTy : Lean.Expr

def TendstoCont.instInhabitedAtom.default : Atom

Equations

• TendstoCont.instInhabitedAtom.default = { fn := default, limit := default, hyp := default, codTy := default }

@[implicit_reducible]

instance TendstoCont.instInhabitedAtom : Inhabited Atom

Equations

• TendstoCont.instInhabitedAtom = { default := TendstoCont.instInhabitedAtom.default }

def TendstoCont.tacticTendsto_cont : Lean.ParserDescr

Equations

• TendstoCont.tacticTendsto_cont = Lean.ParserDescr.node `TendstoCont.tacticTendsto_cont 1024 (Lean.ParserDescr.nonReservedSymbol "tendsto_cont" false)