Is there code to substitute values into a hypothesis?

Stream: new members

[Andre Maute]

Hi there,

It looks like I'm missing something here,
suppose I have a lower and upper bound on a variable 'j'
and I have already a hypothesis with 'j' in it.
I would like to substitute the lower and upper bound for 'j'
and create two new hypotheses.

Kind regards
Andre

variable (d i j : Nat)
variable (hd : d > 1)
variable (hilb : 1 ≤ i)
variable (hiub : i ≤ d)
variable (hjlb : 1 ≤ j)
variable (hjub : j ≤ d)
variable (pp : Nat → Nat → Nat)
variable (hpp : pp i j = i)
variable (ppinv : Nat → Nat → Nat)
variable (gg1 : j = ppinv i (pp i j))
variable (gg2 : j = pp i (ppinv i j))

example : False := by
  rw [gt_iff_lt] at hd
  have h1le1 := Nat.le_refl 1
  have h1led := Nat.le_of_lt hd
  let ff (j : Nat) (hlb : 1 ≤ j) (hub : j ≤ d) :=
    hpp
  have ff1 := ff 1 h1le1 h1led
  sorry

[Ruben Van de Velde]

What are the new hypotheses you want to create, exactly?

[Andre Maute]

These two
hpp1 : pp i 1 = i
hppd : pp i d = i

[Ruben Van de Velde]

And why are those true, mathematically?

[Andre Maute]

As being said, I might be missing something ;-)
My hypotheses are from a large split_ifs.
So this is only doable with quantifiers?

[Riccardo Brasca]

Can you write in English the precise statement you want?

[Riccardo Brasca]

I mean, the full one

[Andre Maute]

@Riccardo Brasca Looks like I'll have to first reanalyze my hypotheses before my large split_ifs, sorry.