gcongr chokes on docs#Submodule.finrank_mono

Stream: mathlib4

[Yaël Dillies]

I am quite disappointed by the following behavior. Is this due to the goal being finrank K { x // x ∈ U } ≤ finrank K { x // x ∈ W } and gcongr not looking inside the types?

import Mathlib.LinearAlgebra.FiniteDimensional.Defs

open FiniteDimensional

@[gcongr]
protected lemma GCongr.submoduleFinrank_mono {K V : Type*} [DivisionRing K] [AddCommGroup V]
    [Module K V] [FiniteDimensional K V] {U W : Submodule K V} (h : U ≤ W) :
    finrank K U ≤ finrank K W := Submodule.finrank_mono h

/-
@[gcongr] attribute only applies to lemmas proving f x₁ ... xₙ ∼ f x₁' ... xₙ'.
 Not all arguments are free variables in the conclusion of ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K]
  [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : FiniteDimensional K V] {U W : Submodule K V},
  U ≤ W → finrank K { x // x ∈ U } ≤ finrank K { x // x ∈ W }
-/

[Yaël Dillies]

@[gcongr] lemma iSup_le_iSup_of_imp {p q : Prop} {α : Type*} [CompleteLattice α] (a : α) (h : p → q) : ⨆ h : p, a ≤ ⨆ h : q, a := sorry suffers from the same issue, sadly