# Zulip Chat Archive

## 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 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 (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