## Stream: Lean for teaching

### Topic: coercion in inequalities

#### Guy (Dec 10 2022 at 17:26):

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 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 (Dec 10 2022 at 17:28):

Does norm_cast help?

#### Johan Commelin (Dec 10 2022 at 17:28):

Maybe exact_mod_cast h3?

#### Johan Commelin (Dec 10 2022 at 17:29):

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

#### Guy (Dec 10 2022 at 17:34):

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 (Dec 10 2022 at 17:35):

@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 (Dec 10 2022 at 17:36):

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

#### Kevin Buzzard (Dec 10 2022 at 17:38):

Yeah that would work.

Last updated: Dec 20 2023 at 11:08 UTC