proof of two_mul from Mathematics in Lean

Stream: new members

[Mike]

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]

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]

@Adam Topaz Pro tip: \1 = \_1

[Adam Topaz]

WHOA!

[Adam Topaz]

I think you just saved me millions of keystrokes

[Mike]

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]

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]

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]

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]

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