recursor 'Exists.dcases_on' can only eliminate into Prop

Stream: new members

[Xavier Roblot]

I already got this error in the past and I do not understand what causes it and how to fix it. Here is a #mwe

import data.complex.module
import algebra.algebra.tower

open_locale complex_conjugate

lemma exist_i {S : Type*} [comm_ring S] [algebra ℝ S] [algebra S ℂ]
  (h : is_scalar_tower ℝ S ℂ) (hc : conj ∘ (algebra_map S ℂ) ≠ algebra_map S ℂ) :
  ∃ s : S, (algebra_map S ℂ) s = complex.I := by sorry

def iso_sc {S : Type*} [comm_ring S] [algebra ℝ S] [algebra S ℂ]
  (h : is_scalar_tower ℝ S ℂ) (hc : conj ∘ (algebra_map S ℂ) ≠ algebra_map S ℂ) :
  S ≃+* ℂ :=
begin
  obtain ⟨s, hs⟩ := exist_i h hc,
  sorry,
end

[Reid Barton]

The short and inaccurate explanation is that there could be multiple s with (algebra_map S ℂ) s = complex.I, and then which one do you want to pick in the definition of iso_sc?

[Kevin Buzzard]

Your goal is not a Prop so some tactics don't work properly (you shouldn't be in tactic mode at all really). Use exists.some instead.

[Eric Rodriguez]

essentially this is because all terms of a Prop are defeq to each other; for example, for ∃ n : nat, true, both 0 and 1 work, so what should Lean choose? Even with a unique existence, this isn't enough for Lean to find out, as in certain cases it couldn't compute what it is! (For example, consider ∃! o : real, is_champernownes_constant o...)