Begin-end tactic

Stream: new members

[Atieh Hosseinizadeh]

Hello I tried to prove a simple equation by begin-end tactic:

import Lean
theorem Raoult_Dalton
  (pi1 pi2 xi Pstar yi Pt : Nat)
  (a1 : pi1 = xi * Pstar)
  (a2 : pi2 = yi * Pt)
  (a3 : pi1 = pi2)
  (a4 : xi = yi) :
  Pstar = Pt :=
begin
  rw [a1, a2, a4] at a3,
  exact a3.symm.subst rfl,
end

however 'begin' doesn't recognize by Lean and I got this error: unknown identifier 'begin'
I'm working with Lean 4
anybody has any idea how should I fix it?

Untitled.png

[Atieh Hosseinizadeh]

By the way I want to prove this:
pi = xi * Pstar
pi = yi * Pt

so:
xi * Pstar = yi * Pt

[Johan Commelin]

@Atieh Hosseinizadeh begin ... end is Lean 3 syntax. You are using Lean 4.

[Moritz Doll]

Lean 4 also got rid of the commas at the end of each line. Also you might want to have a look at #backticks

[Atieh Hosseinizadeh]

thank you
I changed my tactics to something in Lean 4:

I wrote this one:

theorem Rao_Dal
  (pi1 pi2 xi Pstar yi Pt : Nat)
  (a1 : pi1 = Pstar * xi )
  (a2 : pi2 = Pt * yi)
  (a3 : Pstar = Pt)
  (a4 : xi = yi) :
  pi1 = pi2 :=
  by simp [a3, a4] at a1;
     simp [(a2).symm] at a1;
      exact a1

I got this:

  /-
      pi1 pi2 xi Pstar yi Pt : Nat
      a2 : pi2 = Pt * yi
      a3 : Pstar = Pt
      a4 : xi = yi
      a1 : pi1 = pi2
      ⊢ pi1 = pi2
      -/

and it shows my conjecture is proved however I get "no goals" when I want to prove it. It's my screen shot:
Lean3.png

[Kevin Buzzard]

You might want to have a harder look at #backticks ( ` is what you're looking for)

[Kevin Buzzard]

Try dropping the semicolons in your proof, they're not necessary in lean 4