linear_independent subtypes

Stream: new members

[Alena Gusakov]

Hi everyone,

I'm trying to essentially show that linear_independent 𝔽 (λ (x : ↥I), φ x) ↔ linear_independent 𝔽 (λ (x : ↥I), (⟨φ x, h3 x⟩ : span 𝔽 (range ⇑φ))) where h3 is a proof that φ x is in the submodule spanned by the range of φ, but whenever I try to use linear_independent_span or linear_independent.of_comp I get deterministic timeout. Does anyone know why that might be? I can make an MWE if needed (though it would be a bit hard to do so because I'm working in a project).

[Kevin Buzzard]

What do you mean by "use"? In the past I've seen timeouts in linear algebra because of miscounting function inputs and accidentally telling lean to figure out that a complex term is a vector space when it isn't.

[Kevin Buzzard]

Try using the theorems with refine and see if you get more helpful errors

[Michael Stoll]

I've also noticed that linear algebra can be slow, in particular when Lean is trying to interpret some intermediate not-completely-correct state of the code. Fairly frequently, this resulted in orange bars that wouldn't go away, and I had to restart the Lean server... (this is Lean3/mathlib)

[Eric Wieser]

Usually my approach in such a situation is to use have := @some_lemma instead of rw some_lemma or apply some_lemma, and fill out the implicit arguments one by one until I find which one is causing the trouble

[Michael Stoll]

It tends to occur while editing; I assume because some intermediate state of the text is hard to digest...

[Michael Stoll]

... more precisely, it happened rather frequently when editing rado_linear_algebra.lean in #18789.