## Stream: new members

### Topic: let with proposition in tactic mode

#### Kenny Lau (Dec 13 2018 at 15:45):

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 (Dec 13 2018 at 15:45):

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

compare this:

#### Kenny Lau (Dec 13 2018 at 15:46):

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 (Dec 13 2018 at 16:08):

Moral: don't use let with propositions?

#### Kevin Buzzard (Dec 13 2018 at 16:08):

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

Last updated: May 09 2021 at 19:11 UTC