Restrict the conclusion of the current proposition about n-1

Stream: mathlib4

[yh]

I have a proposition about the natural number n, how can I restrict the conclusion of the current proposition about n-1:

example (f : ℕ → ℝ) (hf : ∀ i, f i > 0) (n : ℕ) : ∃ g : ℕ → ℝ, ∀ i, g i > 0 := by sorry

Where f , hf and goal are simplified. Assuming that for each n, it gets g_n. How can I add " if n > 0, ∀ i ≤ n - 1, g_n (i) = g_(n-1) (i)" to the goal

[Kevin Buzzard]

Right now your example can be solved with

import Mathlib.Tactic

example (f : ℕ → ℝ) (hf : ∀ i, f i > 0) (n : ℕ) : ∃ g : ℕ → ℝ, ∀ i, g i > 0 := by
  use fun x ↦ 37
  intro i
  norm_num

Can you write a better #mwe or explain more what you mean by adding something? Why can't you just add it? (exists g, (forall i, g i > 0) \and (the thing you want))

[yh]

I need such a goal, but I can't use the theorem in itself

theorem tmp (f : ℕ → ℝ) (hf : ∀ i, f i > 0) (n : ℕ) : ∃ g : ℕ → ℝ, ∀ i, g i > 0 ∧

    let g' := (tmp f hf (n - 1)).choose

    (if n > 0 then (∀ i ≤ n - 1, g' i = g i)  else True) := by

  sorry

[A.]

Well I'm not sure this is entirely sane, but it does prove that ... something ... is possible

import Mathlib.Data.Real.Basic

inductive P : ℕ → (ℕ → ℝ) → Prop
  | c0 {g : ℕ → ℝ} : (∀ i, 0 < g i) → P 0 g
  | cn {n : ℕ} {g g' : ℕ → ℝ} : P n g' → (∀ i, 0 < g i) → (∀ i ≤ n, g' i = g i) → P (n + 1) g

theorem tmp {f : ℕ → ℝ} (hf : ∀ i, 0 < f i) (n : ℕ) : ∃ g : ℕ → ℝ, P n g :=
  match n with
  | 0 => ⟨f, .c0 hf⟩
  | m + 1 => ⟨f, .cn (tmp hf m).choose_spec hf sorry⟩