## Stream: new members

### Topic: x * x = 100 → x = 10

#### Huỳnh Trần Khanh (Mar 28 2021 at 08:24):

this proof is way too complicated i'm pretty sure there is a very simple way to prove this can anyone help me out

import tactic.linarith

example { x y a : ℕ } { h : x < y } : x + a < y + a := add_lt_add_right h a

lemma less ( x : ℕ ) ( h : x < 10 ) : x * x < 100 := begin
dec_trivial!,
end

lemma greater : ∀ x : ℕ, ∀ h : x > 10, x * x > 100
| 0 h := by linarith
| (n + 1) h := begin
have : (n + 1) * (n + 1) = n * n + 2 * n + 1 := by ring,
rw this,
exact if equal: n = 10 then begin
rw equal,
linarith,
end else begin
have : n * n > 100 := greater n begin
have : n ≤ 10 := by linarith,
have : n < 10 ∨ n = 10 := lt_or_eq_of_le this,
cases this with a b,
{
linarith,
},
{
exact equal b,
}
end,
linarith,
end
end

lemma something { x : { x : ℕ // x * x = 100 } } : (x : ℕ) = 10 := begin
cases x with x hx,
exact if h: x > 10 then begin
have := greater x h,
linarith,
end else begin
exact if h1: x < 10 then begin
have := less x h1,
linarith,
end else begin
have : x = 10 := by linarith,
exact this,
end,
end
end


#### Huỳnh Trần Khanh (Mar 28 2021 at 08:25):

and i wanna keep the lemma signature too

#### Ruben Van de Velde (Mar 28 2021 at 08:37):

import data.nat.basic
import tactic

lemma something' (n : ℕ) (h : n * n = 100) : n = 10 :=
begin
have h1 : 100 = 10 * 10,
{ norm_num },
rw h1 at h,
zify at *,
rw mul_self_eq_mul_self_iff at h,
apply h.resolve_right,
linarith,
end

lemma something { x : { x : ℕ // x * x = 100 } } : (x : ℕ) = 10 := something' x x.prop


or without the auxiliary lemma:

import data.nat.basic
import tactic

lemma something { x : { x : ℕ // x * x = 100 } } : (x : ℕ) = 10 := begin
have h := x.prop,
have h1 : 100 = 10 * 10,
{ norm_num },
simp_rw h1 at h,
zify at *,
rw mul_self_eq_mul_self_iff at h,
apply h.resolve_right,
linarith,
end


#### Mario Carneiro (Mar 28 2021 at 08:43):

There should be a version of this for nat that doesn't have the disjunction

#### Ruben Van de Velde (Mar 28 2021 at 08:46):

You expect there to be one or you think it would be a useful addition?

#### Shing Tak Lam (Mar 28 2021 at 08:48):

Here's a different proof of the auxiliary lemma

import tactic

example (n : ℕ) (hn : n * n = 100) : n = 10 :=
by rw [←nat.sqrt_eq n, hn, (show 100 = 10 * 10, from rfl), nat.sqrt_eq]


#### Eric Wieser (Mar 28 2021 at 08:51):

I'd expect norm_num to be faster than rfl there

#### Shing Tak Lam (Mar 28 2021 at 08:55):

Eric Wieser said:

I'd expect norm_num to be faster than rfl there

import tactic

set_option profiler true

-- elaboration of foo took 28.5ms
lemma foo (n : ℕ) (hn : n * n = 100) : n = 10 :=
by rw [←nat.sqrt_eq n, hn, (show 100 = 10 * 10, from rfl), nat.sqrt_eq]

-- elaboration of bar took 61.2ms
lemma bar (n : ℕ) (hn : n * n = 100) : n = 10 :=
by rw [←nat.sqrt_eq n, hn, (show 100 = 10 * 10, by norm_num), nat.sqrt_eq]


I'm not sure that's the case.

import tactic

set_option profiler true

-- elaboration of foo took 4.52ms
lemma foo : 100 = 10 * 10 := rfl

-- elaboration of bar took 34.2ms
lemma bar : 100 = 10 * 10 := by norm_num


#### Ruben Van de Velde (Mar 28 2021 at 15:20):

Turns out it's called nat.mul_self_inj

Last updated: May 18 2021 at 16:25 UTC