closing a case

Stream: new members

[Joseph Corneli]

Would you please help me understand why the case does not close, and what to do here instead?

import topology.basic data.set.intervals analysis.exponential
open real set

def punctured_line := (Iio (0:ℝ)) ∪ (Ioi (0:ℝ))
noncomputable def punctured_inv := function.restrict (λ (x:ℝ), 1/x) punctured_line

lemma punctured_reals_are_nonzero : ∀ (a : subtype punctured_line), a.val ≠ 0 :=
begin
intro,
let a2 := a.2,                         -- (a.property)
cases a2 with l r,                     -- we can decompose the property using cases
have h : a.val < 0, from mem_Iio.mp l,
have h1 : a.val ≠ 0, from ne_of_lt h,  -- This is the relevant fact
exact h1,                              -- *** But I can't close the case here
end

[Joseph Corneli]

I also can't close it with sorry; trying tells me that a function is expected. But what function would that be?

infer type failed, function expected at
  (let a2 : punctured_line (a.val) := a.property in a.val ≠ 0) (or.inl l)
term
  let a2 : punctured_line (a.val) := _
  in a.val ≠ 0
has type
  Prop
state:
2 goals
a : subtype punctured_line,
l : a.val ∈ Iio 0,
h : a.val < 0,
h1 : a.val ≠ 0
⊢ (let a2 : punctured_line (a.val) := a.property in a.val ≠ 0) (or.inl l)

case or.inr
a : subtype punctured_line,
r : a.val ∈ Ioi 0
⊢ (let a2 : punctured_line (a.val) := a.property in a.val ≠ 0) (or.inr r)

[Sebastien Gouezel]

Why do you use cases a2 instead of cases a.2?

[Joseph Corneli]

@Sebastien Gouezel ah, I thought that was just shorthand

[Joseph Corneli]

Thanks! I guess the lesson here is that "shorthand" isn't likely to be a good idea.

[Sebastien Gouezel]

Shorthands are equivalent in exact ... (as everything is expanded by the kernel), but otherwise it can lead to different behavior.