coercion in inequalities

Stream: Lean for teaching

[Guy]

hi i'm trying to prove Bernoulli's inequality in lean.

this is what I got so far, getting into trouble handling the nat->real coercion

import tactic

import data.real.basic
import data.rat.basic
import data.nat.basic

/-
-/
open_locale classical -- allow proofs by contradiction
/-
-/
noncomputable theory -- don't fuss about the reals being noncomputable

namespace infi1

theorem bernoulli_ineq {x : ℝ} {n : ℕ} [h : x ≥ -1] : (1+x) ^ n ≥ 1 + (n * x) :=
begin
  induction n with d hd,
  rw pow_zero,
  norm_cast,
  linarith,

  have h3 : ((1 + x) ^ d) * (1+x) ≥ (1 + ↑d * x) * (1+x),
    nlinarith,

  rw nat.succ_eq_add_one,
  rw pow_add,
  rw pow_one,

  have h4 : (1 + ↑d * x) * (1 + x) ≥ 1 + ↑(d + 1) * x,
    -- what now
end

end infi1

by the end of the proof, h3 looks alot like the goal, just need to prove h4. I failed to find the right coercion dance to solve h4, would appreciate some help :^)

[Johan Commelin]

Does norm_cast help?

[Johan Commelin]

Maybe exact_mod_cast h3?

[Johan Commelin]

Also, you should change your assumption [h : x ≥ -1] to (h : x ≥ -1) since you can't use typeclass inference there.

[Guy]

thanks for the ( ) tip. norm_cast doesn't do apparent help unfortunately. the main issue (i think?) is the split from ↑(d + 1) to ↑d + 1

[Kevin Buzzard]

@Guy your message would get a lot more eyes on it if you posted it in #new members rather than in the teaching stream. You can probably move the message, or maybe you have to ask a moderator to do so.

[Guy]

@Kevin Buzzard thanks for the tip, may I just repost?

[Kevin Buzzard]

Yeah that would work.