Prove the existence of a structure which satisfy property

Stream: general

[Alice Laroche]

I have this code :

import tactic

structure Foo :=
  (p₁ : ℕ)

theorem bar : ∃foo : Foo, foo.p₁ = 1:=
begin
  have foo : Foo := {
    p₁ := 1
  },
  use foo,
end

How do i resolve the goal ?

[Patrick Massot]

Zulip tip: you need to put the closing backticks on their own line.

[Patrick Massot]

Then your problem is you used have instead of let

[Patrick Massot]

have is meant to be used for proposition, so the value is immediately forgotten (because of the proof irrelevance axiom).

[Alice Laroche]

Thank you, yeah i understand that but i didn't know the let alternative.

[Filippo A. E. Nuccio]

See also here https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/difference.20.60let.60.20and.20.60have.60