no goals
R : Type ?u.366237
R₂ : Type ?u.366240
K : Type u_1
M : Type ?u.366246
M₂ : Type ?u.366249
V : Type u_2
S : Type ?u.366255
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
x : V
hx : ↑f x ≠ 0
y : V
x✝ : y ∈ ⊤
⊢ y - (↑f y * (↑f x)⁻¹) • x ∈ ker f
rw [LinearMap.mem_ker, f.map_sub, f.map_smul, smul_eq_mul, mul_assoc, inv_mul_cancel hx,
  mul_one, sub_self]
no goals
R : Type ?u.366237
R₂ : Type ?u.366240
K : Type u_1
M : Type ?u.366246
M₂ : Type ?u.366249
V : Type u_2
S : Type ?u.366255
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
x : V
hx : ↑f x ≠ 0
y : V
x✝ : y ∈ ⊤
⊢ (↑f y * (↑f x)⁻¹) • x + (y - (↑f y * (↑f x)⁻¹) • x) = y
simp only [add_sub_cancel'_right]