let with proposition in tactic mode

Stream: new members

[Kenny Lau]

import tactic.interactive

open function

meta def tactic.interactive.result : tactic unit :=
do e ← tactic.result, tactic.trace e

theorem cantor_surjective
  (X : Type) (f : X → set X) (Hf : surjective f) : false :=
begin
  let H := Hf {x | x ∉ f x},
  cases H with D e,
  result
  -- ⊢ (let H : ∃ (a : X), f a = {x : X | x ∉ f x} := Hf {x : X | x ∉ f x} in false) (Exists.intro D e)
end

/-
let H : ∃ (a : X), f a = {x : X | x ∉ f x} := _,
    H_1 : ∃ (a : X), f a = {x : X | x ∉ f x} := _
in Exists.dcases_on H_1 (λ (D : X) (e : f D = {x : X | x ∉ f x}), ?m_1[H, H_1, D, e])
-/

[Kenny Lau]

somehow there's a strange goal if we use let instead of have with a proposition in tactic mode

[Kenny Lau]

compare this:

[Kenny Lau]

import tactic.interactive

open function

meta def tactic.interactive.result : tactic unit :=
do e ← tactic.result, tactic.trace e

theorem cantor_surjective
  (X : Type) (f : X → set X) (Hf : surjective f) : false :=
begin
  have H := Hf {x | x ∉ f x},
  cases H with D e,
  result
  -- ⊢ false
end

/-
Exists.dcases_on (Hf {x : X | x ∉ f x})
  (λ (D : X) (e : f D = {x : X | x ∉ f x}), ?m_1[Hf {x : X | x ∉ f x}, Hf {x : X | x ∉ f x}, D, e])
-/

[Kevin Buzzard]

Moral: don't use let with propositions?

[Kevin Buzzard]

Background: Kenny just watched me giving a live Lean talk and I used let with a proposition :P