# Zulip Chat Archive

## Stream: new members

### Topic: proof of two_mul from Mathematics in Lean

#### Mike (Aug 28 2020 at 12:18):

Hi,

Once again, I'm unable to get a proof to work in lean. I'm trying to prove

`theorem two_mul (a : R) : 2 * a = a + a :=`

from *Mathematics in Lean*

Here's what I'm trying to make work:

```
import algebra.ring
import tactic
namespace my_ring
variables {R : Type*} [ring R]
lemma one_and_one_eq_two : 1 + 1 = (2 : R) :=
by refl
theorem two_mul (a : R) : 2 * a = a + a :=
begin
have h₁ : (1 + 1)* a = 1*a + 1*a,
{rw add_mul},
have h₂ : 2*a = 1*a + 1*a,
{rw one_and_one_eq_two at h₁},
have h₃ : 2*a = a + a,
{
rw one_mul at h₂,
rw one_mul at h₂
},
exact h₃,
end
end my_ring
```

The proof fails at `{rw one_and_one_eq_two at h₁},`

with the message

/-

solve1 tactic failed, focused goal has not been solved

state:

R : Type u_1,

_inst_1 : ring R,

a : R,

h₁ : 2 * a = 1 * a + 1 * a

⊢ 2 * a = 1 * a + 1 * a

-/

Would appreciate someone showing me what the heck I'm doing wrong. Thanks!

#### Adam Topaz (Aug 28 2020 at 12:37):

The issue is that you've modified `h\_1`

in that line, but didn't tell lean to use the modified `h\_1`

as your proof of `h\_2`

. So a simple fix is to add `assumption`

after `rw one_and_one_eq_two at h₁`

(or even `exact h\_1`

).

#### Johan Commelin (Aug 28 2020 at 12:49):

@Adam Topaz Pro tip: `\1`

= `\_1`

#### Adam Topaz (Aug 28 2020 at 12:50):

WHOA!

#### Adam Topaz (Aug 28 2020 at 12:50):

I think you just saved me millions of keystrokes

#### Mike (Aug 28 2020 at 12:52):

Thank you! That fixes the proof of h₂. Now I just need to prove h₃.

I'm getting this error for that:

/-

rewrite tactic failed, did not find instance of the pattern in the target expression

1 * ?m_3

state:

R : Type u_1,

_inst_1 : ring R,

a : R,

h₁ : (1 + 1) * a = 1 * a + 1 * a,

h₂ : 2 * a = a + a

⊢ 2 * a = a + a

-/

Which seems odd, because there are two 1*a 's in h₂.

#### Adam Topaz (Aug 28 2020 at 13:02):

This is expected. `rw`

will change all instances of the first thing it matches with.

Here's your proof cut down a little bit (note that last `have`

isn't needed).

```
import algebra.ring
import tactic
namespace my_ring
variables {R : Type*} [ring R]
lemma one_and_one_eq_two : 1 + 1 = (2 : R) :=
by refl
theorem two_mul (a : R) : 2 * a = a + a :=
begin
have h₁ : (1 + 1)* a = 1*a + 1*a,
{rw add_mul},
have h₂ : 2*a = 1*a + 1*a,
{rwa one_and_one_eq_two at h₁},
rwa one_mul at h₂,
end
end my_ring
```

#### Kenny Lau (Aug 28 2020 at 19:58):

in mathlib we use 2-space indent as well as spaces after the opening curly bracket and before the closing one (i.e.

`{ lorem ipsum }`

)

#### Kenny Lau (Aug 28 2020 at 19:59):

```
import algebra.ring
import tactic
namespace my_ring
variables {R : Type*} [ring R]
lemma one_and_one_eq_two : 1 + 1 = (2 : R) :=
rfl
theorem two_mul (a : R) : 2 * a = a + a :=
begin
have h₁ : (1 + 1) * a = 1 * a + 1 * a,
{ rw add_mul},
have h₂ : 2 * a = 1 * a + 1 * a,
{ rwa one_and_one_eq_two at h₁ },
rwa one_mul at h₂,
end
end my_ring
```

#### Kenny Lau (Aug 28 2020 at 20:00):

we also use spaces around infixes (i.e. `1 * a`

not `1*a`

)

Last updated: May 16 2021 at 21:11 UTC