Fin problems with https://live.lean-lang.org

Stream: new members

[Andre Maute]

Hi all,

I wonder why I see different behavior between my local lean installation and the online web editor.
The two small questions are embedded below in the code. What am I missing?
My lakefile.toml contains the following snippet.

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.27.0-rc1"

Regards Andre

import Mathlib.Tactic

variable (d k l m : ℕ)

example
  (hk : k ≤ d)
  (hl : l ≤ d)
  (hkl : k ≠ l)
  (hk2 : k < d + 1)
  (kFin : Fin (d + 1) := ⟨k, hk2⟩)
  (hl2 : l < d + 1)
  (lFin : Fin (d + 1) := ⟨l, hl2⟩)
  : 1 = 2 := by
    -- Question 1: what am I missing here, while observing this different behavior?
    -- This closes with local lean installation but not on 'live.lean-lang.org'
    have hk3 : k = kFin.val := by rfl
    -- This closes with local lean installation but not on 'live.lean-lang.org'
    have hl3 : l = lFin.val := by rfl
    -- This closes with local lean installation but not on 'live.lean-lang.org'
    have hkl2a : kFin ≠ lFin := by
      -- exact Fin.ne_of_val_ne hkl
      sorry
    -- This doesn't work locally either
    -- have hkl2b := Fin.ne_of_val_ne hkl
    -- Question 2: what is the difference locally between hkl2a and hkl2b?
    sorry

[Aaron Liu]

The behavior you observe locally should be completely impossible, since kFin and lFin are arbitrary variables of the specified type

[Andre Maute]

Ah, I can resolve the different behavior question if I convert the kFin and lFin lines into 'let' lines
and insert them before the 'have' lines. Indeed my local code does that.

  let kFin := Fin.mk k hk2
  let lFin := Fin.mk l hl2

Though I wonder why this results in different behavior, but the info view looks the same?

Any idea for my Question 2?

[Aaron Liu]

Andre Maute said:

Though I wonder why this results in different behavior, but the info view looks the same?

Surely this is not the case? Can you show what the infoview look like in each scenario?

[Andre Maute]

Oh I see,

until now, I had assumed that one could simply copy the content of an existing info view state
and paste them in an example for a mwe with some minor tweaks.

Question 3: So what is the recommended way for reproducing a given info view state for a mwe?

import Mathlib.Tactic

variable (d k l m : ℕ)

example
  (hk : k ≤ d)
  (hk2 : k < d + 1)
  : 1 = 2 := by
    let kFin : Fin (d + 1) := ⟨k, hk2⟩
    -- Info view shows 'kFin : Fin (d + 1) := ⟨k, hk2⟩'
    have hk3 : k = kFin.val := by rfl
  sorry

example
  (hk : k ≤ d)
  (hk2 : k < d + 1)
  (kFin : Fin (d + 1) := ⟨k, hk2⟩)
  : 1 = 2 := by
    -- Info view shows 'kFin : Fin (d + 1)'
    have hk3 : k = kFin.val := by rfl
  sorry