alternative to set

Stream: general

[Kenny Lau]

I noticed that the set tactic doesn't interact well with revert (because in its core it's still a let, and when you revert it you see a let _ := _ in in the goal)

and I've come up with an alternative:

example : true :=
begin
  have : ∃ n, n = 2 + 2 := ⟨_, rfl⟩, cases this with n hn,
/-
state:
n : ℕ,
hn : n = 2 + 2
⊢ true
-/
  trivial
end

[Kenny Lau]

example : true :=
begin
  have : ∃ n, n = 2 + 2 := ⟨_, rfl⟩, cases this with n hn,
/-
n : ℕ,
hn : n = 2 + 2
⊢ true
-/
  revert n,
/-
⊢ ∀ (n : ℕ), n = 2 + 2 → true
-/
  intros, trivial
end

example : true :=
begin
  set n := 2 + 2 with hn,
/-
n : ℕ := 2 + 2,
hn : n = 2 + 2
⊢ true
-/
  revert n,
/-
⊢ let n : ℕ := 2 + 2
  in n = 2 + 2 → true
-/
  intros, trivial
end

[Scott Morrison]

Can you do this with a sigma type when the goal isn't propositional?

[Kenny Lau]

I'd imagine not

[Rob Lewis]

Your example doesn't do the same thing. Using let means that the new variable is definitionally equal to the term you set it to, which is sometimes useful.