no goals
k : Type u_1
P₁ : Type u_2
P₂ : Type ?u.663302
P₃ : Type ?u.663305
P₄ : Type ?u.663308
V₁ : Type u_3
V₂ : Type ?u.663314
V₃ : Type ?u.663317
V₄ : Type ?u.663320
inst✝¹³ : Ring k
inst✝¹² : AddCommGroup V₁
inst✝¹¹ : Module k V₁
inst✝¹⁰ : AffineSpace V₁ P₁
inst✝⁹ : AddCommGroup V₂
inst✝⁸ : Module k V₂
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AddCommGroup V₃
inst✝⁵ : Module k V₃
inst✝⁴ : AffineSpace V₃ P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AffineSpace V₄ P₄
inst✝ : Invertible 2
x y : V₁
h : bit0 x = bit0 y
⊢ x = y
rwa [bit0, bit0, ← two_smul k x, ← two_smul k y,
  (isUnit_of_invertible (2 : k)).smul_left_cancel] at h