specialize h hx
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : ↑S x = 0 → x = 0
⊢ x = 0
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : x = 0
⊢ x = 0