mathlib

mathlib copied to clipboard

Uncomment each block of code one at a time:

import data.real.basic
import data.set.basic


-- library_search fails
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   library_search
-- end

-- This passes
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   tauto,
-- end

-- Try this: exact Exists.intro (λ (a : ℝ), a = a) rfl
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   suggest
-- end

-- Try this: exact Exists.intro (λ (a : ℝ), a = a) rfl
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   show_term {tauto}
-- end

-- Using exact Exists.intro (λ (a : ℝ), a = a) rfl
-- causes type mismatch at application
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   exact Exists.intro (λ (a : ℝ), a = a) rfl
-- end

The full type mismatch error message is:

type mismatch at application
  Exists.intro (λ (a : ℝ), a = a) rfl
term
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  ∀ (r : ℝ), r ∈ λ (a : ℝ), a = a
state:
⊢ ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s