∀ {K : Type u_2} {V : Type u_1} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : V →ₗ[K] V}
  (motive : (∃ g, f ∘ₗ g = LinearMap.id) → Prop) (x : ∃ g, f ∘ₗ g = LinearMap.id),
  (∀ (g : V →ₗ[K] V) (hg : f ∘ₗ g = LinearMap.id), motive ⋯) → motive x