Zulip Chat Archive

I've noticed recently that sometimes, when I write have h := SomeLemma as an intermediate step in a proof, sometimes Lean goes a step too far in filling in assumptions for the have. For instance, in the following def, when I try to work with Equiv.ofBijective , the tactic state assumes that the function is already bijective and produces an equivalence without me providing a proof.

import Mathlib.LinearAlgebra.FiniteDimensional

open scoped Classical

universe u v

variable {V : Type v} {K : Type u} [Field K] [AddCommGroup V] [Module K V]

noncomputable def isoThing (r : {X : Submodule K (V × K) | ¬ Submodule.map (LinearMap.inr K V K) ⊤ ≤ X}) :
  r ≃ₗ[K] Submodule.map (LinearMap.fst K V K) r := by
  have h4 := Equiv.ofBijective ((LinearMap.fst K V K).restrict (λ x (hx : x ∈ r.1) =>
    Submodule.mem_map_of_mem hx))

    sorry

  apply Equiv.toLinearEquiv h4

  sorry

If I instead provide it with a hole, ?_, it gives me the correct goal in the tactic state, but goes a step further and h4 becomes a term of type ↥(Submodule.map (LinearMap.fst K V K) ↑r), as if I evaluated the equivalence at some element of the submodule, and which gives me an error when I try to apply it to my goal with Equiv.toLinearEquiv.

Alena Gusakov (May 17 2024 at 21:23):

Here is the tactic state without the hole

**V** : Type v
**K** : Type u
**inst✝²** : Field K
**inst✝¹** : AddCommGroup V
**inst✝** : Module K V
**r** : ↑{X | ¬Submodule.map (LinearMap.inr K V K) ⊤ ≤ X}
**h4** : ↥↑r ≃ ↥(Submodule.map (LinearMap.fst K V K) ↑r)
**⊢** ↥↑r ≃ₗ[K] ↥(Submodule.map (LinearMap.fst K V K) ↑r)

Expected type
**V** : Type v
**K** : Type u
**inst✝²** : Field K
**inst✝¹** : AddCommGroup V
**inst✝** : Module K V
**r** : ↑{X | ¬Submodule.map (LinearMap.inr K V K) ⊤ ≤ X}
**⊢** ↥↑r → ↥(Submodule.map (LinearMap.fst K V K) ↑r)

and here's the tactic state with the hole

2 goals
case refine_2
V : Type v
K : Type u
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
r : ↑{X | ¬Submodule.map (LinearMap.inr K V K) ⊤ ≤ X}
h4 : ↥(Submodule.map (LinearMap.fst K V K) ↑r)
⊢ ↥↑r ≃ₗ[K] ↥(Submodule.map (LinearMap.fst K V K) ↑r)
case refine_1
V : Type v
K : Type u
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
r : ↑{X | ¬Submodule.map (LinearMap.inr K V K) ⊤ ≤ X}
⊢ Function.Bijective ⇑(LinearMap.restrict (LinearMap.fst K V K) _)
Messages (1)
mwe2.lean:17:28
application type mismatch
  Equiv.toLinearEquiv h4
argument
  h4
has type
  ↥(Submodule.map (LinearMap.fst K V K) ↑r) : Type v
but is expected to have type
  ?m.6769 ≃ ?m.6770 : Type (max ?u.6766 ?u.6767)