implicit parameters in iff lemma

EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean

@@ -60,9 +60,9 @@ theorem neg_vec_norm_eq (A B : P) : ‖- VEC A B‖ = ‖VEC A B‖ := by
 theorem vec_norm_eq_rev (A B : P) : ‖VEC A B‖ = ‖VEC B A‖ := by
   rw [← neg_vec, neg_vec_norm_eq]
 
-theorem eq_iff_vec_eq_zero (A B : P) : B = A ↔ VEC A B = 0 := vsub_eq_zero_iff_eq.symm
+theorem eq_iff_vec_eq_zero {A B : P} : B = A ↔ VEC A B = 0 := vsub_eq_zero_iff_eq.symm
 
-theorem ne_iff_vec_ne_zero (A B : P) : B ≠ A ↔ VEC A B ≠ 0 := (eq_iff_vec_eq_zero A B).not
+theorem ne_iff_vec_ne_zero {A B : P} : B ≠ A ↔ VEC A B ≠ 0 := eq_iff_vec_eq_zero.not
 
 @[simp]
 theorem vec_add_vec (A B C : P) : VEC A B + VEC B C = VEC A C := by
@@ -88,10 +88,10 @@ theorem vec_sub_vec' (O A B: P) : VEC A O - VEC B O = VEC A B := by
 theorem pt_eq_pt_of_eq_smul_smul {O A B : P} {v : Vec} {tA tB : ℝ} (h : tA = tB) (ha : VEC O A = tA • v) (hb : VEC O B = tB • v) : A = B := by
   have hc : VEC A B = VEC O B - VEC O A := (vec_sub_vec O A B).symm
   rw [ha, hb, ← sub_smul, Iff.mpr sub_eq_zero h.symm, zero_smul] at hc
-  exact ((eq_iff_vec_eq_zero A B).2 hc).symm
+  exact (eq_iff_vec_eq_zero.2 hc).symm
 
 
-def VecND.mkPtPt (A B : P) (h : B ≠ A) : VecND := ⟨Vec.mkPtPt A B, (ne_iff_vec_ne_zero A B).mp h⟩
+def VecND.mkPtPt (A B : P) (h : B ≠ A) : VecND := ⟨Vec.mkPtPt A B, ne_iff_vec_ne_zero.mp h⟩
 
 @[inherit_doc VecND.mkPtPt]
 scoped syntax "VEC_nd" ws term:max ws term:max (ws term:max)? : term

EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean

@@ -205,7 +205,7 @@ theorem pts_lieson_circle_perpfoot_eq_midpoint {A B : P} {ω : Circle P} [hne :
       _ = (1 / 2 : ℝ) • ((2 : ℝ) • VEC A (perp_foot ω.center (LIN A B))) := by rw [← (pts_lieson_circle_vec_eq hl₁ hl₂), two_smul]
       _ = VEC A (perp_foot ω.center (LIN A B)) := by simp
   have eq₂ : VEC A (SEG A B).midpoint = (1 / 2 : ℝ) • (VEC A B) := Seg.vec_source_midpt
-  apply (eq_iff_vec_eq_zero _ _).mpr
+  apply eq_iff_vec_eq_zero.mpr
   calc
     _ = VEC A (perp_foot ω.center (LIN A B)) - VEC A (SEG A B).midpoint := by rw [vec_sub_vec]
     _ = 0 := by rw [eq₁, eq₂]; simp
@@ -222,7 +222,7 @@ theorem three_pts_lieson_circle_not_collinear {A B C : P} {ω : Circle P} [hne
     calc
       _ = VEC (perp_foot ω.center (LIN A B)) C - VEC (perp_foot ω.center (LIN A B)) B := by rw [vec_sub_vec]
       _ = 0 := by rw [← eq₁, ← eq₂, sub_self]
-  have : VEC B C ≠ 0 := (ne_iff_vec_ne_zero _ _).mp hne₂.out
+  have : VEC B C ≠ 0 := ne_iff_vec_ne_zero.mp hne₂.out
   tauto
 
 end Circle

EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean

@@ -300,7 +300,7 @@ def Inxpts {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : C
   right := (- Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)) • (VEC_nd ω₁.center ω₂.center (intersected_centers_distinct h).symm).toDir.unitVec +ᵥ ω₁.center
 
 theorem inx_pts_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : (Inxpts h).left ≠ (Inxpts h).right := by
-  apply (ne_iff_vec_ne_zero _ _).mpr
+  apply ne_iff_vec_ne_zero.mpr
   unfold Vec.mkPtPt Inxpts
   simp only [neg_mul, vadd_vsub_vadd_cancel_right, ne_eq, ← sub_smul]
   simp only [add_sub_add_right_eq_sub, sub_neg_eq_add, smul_eq_zero, add_self_eq_zero, mul_eq_zero,
@@ -515,7 +515,7 @@ theorem inx_pts_line_perp_center_line {ω₁ : Circle P} {ω₂ : Circle P} (h :
         rw [← hn]
         show ‖VEC (Inxpts h).left (Inxpts h).right‖ ≠ 0
         apply norm_ne_zero_iff.mpr
-        apply (ne_iff_vec_ne_zero _ _).mp (inx_pts_distinct h).symm
+        apply ne_iff_vec_ne_zero.mp (inx_pts_distinct h).symm
   have hdir: (VEC_nd (Inxpts h).left (Inxpts h).right (inx_pts_distinct h).symm).toDir = - (Dir.I * (VEC_nd ω₁.center ω₂.center (intersected_centers_distinct h).symm).toDir) := by
     ext; rw [this]; rw [this]
   calc

EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean

@@ -96,7 +96,7 @@ theorem Collinear.perm₁₃₂ {A B C : P} (c : Collinear A B C) : Collinear A
     have ht : t ≠ 0 := by
       by_contra ht'
       rw [ht', zero_smul] at e
-      have _ : C = A := ((eq_iff_vec_eq_zero A C).2 e)
+      have _ : C = A := (eq_iff_vec_eq_zero.2 e)
       tauto
     exact collinear_of_vec_eq_smul_vec (Eq.symm ((inv_smul_eq_iff₀ ht).2 e))
   · rw [← iff_true (Collinear _ _ _), ← eq_iff_iff]
@@ -137,7 +137,7 @@ theorem collinear_of_collinear_collinear_ne {A B C D: P} (h₁ : Collinear A B C
   rcases ad with ⟨s,eq'⟩
   by_cases nd : r = 0
   . simp only [nd, zero_smul] at eq
-    have : C = A := (eq_iff_vec_eq_zero A C).mpr eq
+    have : C = A := eq_iff_vec_eq_zero.mpr eq
     rw [this] ; apply triv_collinear₁₂
   apply collinear_of_vec_eq_smul_vec'
   rw [eq,eq']
@@ -181,7 +181,7 @@ theorem Ray.collinear_of_lies_on {A B C : P} {ray : Ray P} (hA : A LiesOn ray) (
       apply add_right_cancel_iff.mp nd
     rw [this] at ab
     rw [sub_self, zero_smul] at ab
-    have : B = A := by apply (eq_iff_vec_eq_zero A B).mpr ab
+    have : B = A := by apply eq_iff_vec_eq_zero.mpr ab
     rw [this] ; apply triv_collinear₁₂
   apply collinear_of_vec_eq_smul_vec'
   use (c - a)/(b - a)
@@ -192,10 +192,10 @@ theorem Seg.collinear_of_lies_on {A B C : P} {seg : Seg P} (hA : A LiesOn seg) (
   by_cases nd : seg.source =seg.target
   . rcases hA with ⟨_,_,_,a⟩
     simp only [nd, vec_same_eq_zero, smul_zero] at a
-    have a_d : A = seg.target := by apply (eq_iff_vec_eq_zero seg.target A).mpr a
+    have a_d : A = seg.target := by apply eq_iff_vec_eq_zero.mpr a
     rcases hB with ⟨_,_,_,b⟩
     simp only [nd, vec_same_eq_zero, smul_zero] at b
-    have b_d : B = seg.target := by apply (eq_iff_vec_eq_zero seg.target B).mpr b
+    have b_d : B = seg.target := by apply eq_iff_vec_eq_zero.mpr b
     rw [a_d,b_d] ; apply triv_collinear₁₂
   rw [<-ne_eq] at nd
   let seg_nd := SegND.mk seg.source seg.target nd.symm

EuclideanGeometry/Foundation/Axiom/Linear/Line.lean

@@ -939,7 +939,7 @@ theorem SegND.line_midpt_target_eq_toLine {s : SegND P} : LIN s.midpoint s.targe
 theorem eq_or_vec_eq_of_dist_eq_of_lies_on_line_pt_pt {A B C : P} [hne : PtNe B A] (h : C LiesOn (LIN A B)) (heq : dist A C = dist A B) : (C = B) ∨ (VEC A C = VEC B A) := by
   rcases Ray.lies_on_toLine_iff_lies_on_or_lies_on_rev.mp h with h | h
   · left
-    apply (eq_iff_vec_eq_zero _ _).mpr
+    apply eq_iff_vec_eq_zero.mpr
     have : VEC A C = (dist A C) • (RAY A B).2.unitVec := Ray.vec_eq_dist_smul_toDir_of_lies_on h
     calc
       _ = VEC A C - VEC A B := by rw [vec_sub_vec]
@@ -982,7 +982,7 @@ theorem SegND.dist_midpt_eq_iff_eq_source_or_eq_target_of_lies_on_toLine {A : P}
     rcases eq_or_vec_eq_of_dist_eq_of_lies_on_line_pt_pt this hh with h₁ | h₂
     · exact .inl h₁
     right
-    apply (eq_iff_vec_eq_zero _ _).mpr
+    apply eq_iff_vec_eq_zero.mpr
     calc
       _ = VEC s.midpoint A - VEC s.midpoint s.target := by rw [vec_sub_vec]
       _ = VEC s.source s.midpoint - VEC s.midpoint s.target := by rw [h₂]

EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean

@@ -21,7 +21,7 @@ theorem ratio_is_real' (A B C : P) (colin : Collinear A B C) [cnea : PtNe C A] :
   have h0 : Collinear A C B := Collinear.perm₁₃₂ colin
   rw [collinear_iff_eq_smul_vec_of_ne] at h0
   rcases h0 with ⟨r , h1⟩
-  have h2 : VEC A C ≠ 0 := (ne_iff_vec_ne_zero A C).mp cnea.out
+  have h2 : VEC A C ≠ 0 := ne_iff_vec_ne_zero.mp cnea.out
   rw [h1]
   calc
     (r • VEC A C / VEC A C).im = ((r : ℂ) • VEC A C / VEC A C).im := rfl
@@ -37,7 +37,7 @@ theorem ratio_is_real (A B C : P) (colin : Collinear A B C) [cnea : PtNe C A] :
   exact Complex.ext h0 h1.symm
 
 theorem vec_eq_vec_smul_ratio (A B C : P) (colin : Collinear A B C) [cnea : PtNe C A] : VEC A B = (divratio A B C) • (VEC A C) := by
-  have h0 : VEC A C ≠ 0 := (ne_iff_vec_ne_zero A C).mp cnea.out
+  have h0 : VEC A C ≠ 0 := ne_iff_vec_ne_zero.mp cnea.out
   have h1 : VEC A B = ((VEC A B) / (VEC A C)) • VEC A C := by
     field_simp
   rw [h1, ratio_is_real A B C colin]
@@ -58,7 +58,7 @@ theorem ratio_eq_ratio_div_ratio_minus_one (A B C : P) [cnea : PtNe C A] (colin
     rw[h3]
   have h4 : VEC B A / VEC B C = (((divratio A B C / (divratio A B C - 1)) : ℝ ) : ℂ) := by
     rw [h0, h1]
-    have h5 : VEC A C ≠ 0 := (ne_iff_vec_ne_zero A C).mp cnea.out
+    have h5 : VEC A C ≠ 0 := ne_iff_vec_ne_zero.mp cnea.out
     field_simp
     norm_cast
     rw [Vec.neg_cdiv, Vec.smul_cdiv, Vec.cdiv_self h5, neg_div, ← div_neg]

EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean

@@ -243,7 +243,7 @@ abbrev target (seg_nd : SegND P) : P := seg_nd.1.target
 
 /-- Given a nondegenerate segment $AB$, this function returns the nondegenerate vector $\overrightarrow{AB}$. -/
 @[pp_dot]
-def toVecND (seg_nd : SegND P) : VecND := ⟨VEC seg_nd.source seg_nd.target, (ne_iff_vec_ne_zero _ _).mp seg_nd.2⟩
+def toVecND (seg_nd : SegND P) : VecND := ⟨VEC seg_nd.source seg_nd.target, ne_iff_vec_ne_zero.mp seg_nd.2⟩
 
 /-- Given a nondegenerate segment $AB$, this function returns the direction associated to the segment, defined by normalizing the nondegenerate vector $\overrightarrow{AB}$. -/
 @[pp_dot]
@@ -1233,7 +1233,7 @@ theorem target_lies_int_seg_source_pt_of_pt_lies_int_extn {X : P} {seg_nd : SegN
       linarith
     rw [this] at ha
     simp only [smul_neg, zero_smul, neg_zero] at ha
-    apply (eq_iff_vec_eq_zero _ _).mpr
+    apply eq_iff_vec_eq_zero.mpr
     exact ha
   have raysourcesource : seg_nd.extension.source = seg_nd.1.target := by
     rfl
@@ -1671,7 +1671,7 @@ theorem SegND.exist_pt_beyond_pt (l : SegND P) : (∃ q : P, l.target LiesInt (S
     If a segment contains an interior point, then it is nondegenerate-/
 theorem Seg.nd_of_exist_int_pt {X : P} {seg : Seg P} (h : X LiesInt seg) : seg.IsND := by
   rcases h with ⟨⟨_, ⟨_, _, e⟩⟩, p_ne_s, _⟩
-  have t : VEC seg.source X ≠ 0 := (ne_iff_vec_ne_zero seg.source X).mp p_ne_s
+  have t : VEC seg.source X ≠ 0 := ne_iff_vec_ne_zero.mp p_ne_s
   rw [e] at t
   exact Iff.mp vsub_ne_zero (right_ne_zero_of_smul t)
 

EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean

@@ -44,7 +44,7 @@ theorem collinear_iff_wedge_eq_zero (A B C : P) : (Collinear A B C) ↔ (wedge A
   dsimp only [wedge]
   by_cases h : PtNe B A
   · have vecabnd : VEC A B ≠ 0 := by
-      exact (ne_iff_vec_ne_zero A B).mp h.out
+      exact ne_iff_vec_ne_zero.mp h.out
     rw [← Vec.det_skew, neg_eq_zero, Vec.det_eq_zero_iff_eq_smul_right]
     simp only [vecabnd, false_or]
     constructor
@@ -54,7 +54,7 @@ theorem collinear_iff_wedge_eq_zero (A B C : P) : (Collinear A B C) ↔ (wedge A
       exact collinear_iff_eq_smul_vec_of_ne.mpr k
   · simp [PtNe, fact_iff] at h
     have vecab0 : VEC A B = 0 := by
-      exact (eq_iff_vec_eq_zero A B).mp h
+      exact eq_iff_vec_eq_zero.mp h
     constructor
     intro
     field_simp [vecab0]
@@ -109,9 +109,9 @@ theorem odist'_eq_length_mul_sin (A : P) (ray : Ray P) [h : PtNe A ray.source] :
 
 theorem wedge_eq_length_mul_odist' (A B C : P) [bnea : PtNe B A] : (wedge A B C) = (SEG A B).length * odist' C (RAY A B) := by
   by_cases p : C = A
-  · have vecrayc0 : VEC (RAY A B).source C = 0 := (eq_iff_vec_eq_zero A C).mp p
+  · have vecrayc0 : VEC (RAY A B).source C = 0 := eq_iff_vec_eq_zero.mp p
     dsimp only [wedge, odist']
-    field_simp [(eq_iff_vec_eq_zero A C).mp p, vecrayc0]
+    field_simp [eq_iff_vec_eq_zero.mp p, vecrayc0]
   · haveI cnea : PtNe C A := ⟨p⟩
     rw [wedge_eq_length_mul_length_mul_sin,
       @odist'_eq_length_mul_sin _ _ C (RAY A B) cnea, ← mul_assoc]

EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean

@@ -311,11 +311,11 @@ theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr
   unfold IsND
   rw [not_not]
   by_cases h₁ : VEC B C = 0
-  · simp only [(eq_iff_vec_eq_zero B C).2 h₁]
+  · simp only [eq_iff_vec_eq_zero.2 h₁]
     apply Collinear.perm₃₂₁
     exact triv_collinear₁₂ _ _
   · by_cases h₂ : VEC C A = 0
-    · simp only [(eq_iff_vec_eq_zero C A).2 h₂]
+    · simp only [eq_iff_vec_eq_zero.2 h₂]
       apply Collinear.perm₁₃₂
       exact triv_collinear₁₂ _ _
     · have g : SameRay ℝ (VEC B C) (VEC C A)

EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean

@@ -192,7 +192,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr
      unfold Quadrilateral.IsParallelogram at para
      have k₂₃: qdr_nd.point₁=qdr_nd.point₂ :=by
        rw [k₂₂] at para
-       simp only [para, (eq_iff_vec_eq_zero qdr_nd.point₁ qdr_nd.point₂).mpr, vec_same_eq_zero]
+       simp only [para, eq_iff_vec_eq_zero.mpr, vec_same_eq_zero]
      simp only [k₂₃.symm, ne_eq, not_true_eq_false] at hba
    have t : ¬ Collinear qdr_nd.point₂ qdr_nd.point₁ qdr_nd.point₃ := by
      by_contra k
@@ -202,29 +202,29 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr
      simp only [hca, hbc, hba.symm, or_self, dite_false] at t
      simp only [t, not_false_eq_true]
    have l₁ : qdr_nd.edgeND₁₂.toProj=VecND.toProj ⟨VEC qdr_nd.point₁ qdr_nd.point₂, _⟩ := by rfl
-   have l₁' : qdr_nd.edgeND₁₂.toProj=VecND.toProj ⟨VEC qdr_nd.point₂ qdr_nd.point₁, (ne_iff_vec_ne_zero _ _).mp hba.symm⟩ := by
-     have y₁:VecND.toProj ⟨VEC qdr_nd.point₂ qdr_nd.point₁, (ne_iff_vec_ne_zero _ _).mp hba.symm⟩=VecND.toProj ⟨VEC qdr_nd.point₁ qdr_nd.point₂, (ne_iff_vec_ne_zero _ _).mp hba⟩ := by
+   have l₁' : qdr_nd.edgeND₁₂.toProj=VecND.toProj ⟨VEC qdr_nd.point₂ qdr_nd.point₁, ne_iff_vec_ne_zero.mp hba.symm⟩ := by
+     have y₁:VecND.toProj ⟨VEC qdr_nd.point₂ qdr_nd.point₁, ne_iff_vec_ne_zero.mp hba.symm⟩=VecND.toProj ⟨VEC qdr_nd.point₁ qdr_nd.point₂, ne_iff_vec_ne_zero.mp hba⟩ := by
        have z₁: VEC qdr_nd.point₂ qdr_nd.point₁ =- VEC qdr_nd.point₁ qdr_nd.point₂ := by
          simp only [neg_vec]
        simp only [ne_eq, z₁, VecND.mk_neg', VecND.neg_toProj]
      simp only [l₁, ne_eq, y₁]
    have l₂ : qdr_nd.edgeND₂₃.toProj=VecND.toProj ⟨VEC qdr_nd.point₂ qdr_nd.point₃, _⟩ := by rfl
-   have l₂' : qdr_nd.edgeND₂₃.toProj=VecND.toProj ⟨VEC qdr_nd.point₃ qdr_nd.point₂, (ne_iff_vec_ne_zero _ _).mp hbc⟩ := by
-     have y₂:VecND.toProj ⟨VEC qdr_nd.point₃ qdr_nd.point₂, (ne_iff_vec_ne_zero _ _).mp hbc⟩=VecND.toProj ⟨VEC qdr_nd.point₂ qdr_nd.point₃, (ne_iff_vec_ne_zero _ _).mp hbc.symm⟩ := by
+   have l₂' : qdr_nd.edgeND₂₃.toProj=VecND.toProj ⟨VEC qdr_nd.point₃ qdr_nd.point₂, ne_iff_vec_ne_zero.mp hbc⟩ := by
+     have y₂:VecND.toProj ⟨VEC qdr_nd.point₃ qdr_nd.point₂, ne_iff_vec_ne_zero.mp hbc⟩=VecND.toProj ⟨VEC qdr_nd.point₂ qdr_nd.point₃, ne_iff_vec_ne_zero.mp hbc.symm⟩ := by
        have z₂: VEC qdr_nd.point₃ qdr_nd.point₂ =- VEC qdr_nd.point₂ qdr_nd.point₃ := by
          simp only[neg_vec]
        simp only [ne_eq, z₂, VecND.mk_neg', VecND.neg_toProj]
      simp only [l₂, ne_eq, y₂]
    have l₃ : qdr_nd.edgeND₃₄.toProj=VecND.toProj ⟨VEC qdr_nd.point₃ qdr_nd.point₄, _⟩ := by rfl
-   have l₃' : qdr_nd.edgeND₃₄.toProj=VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₃, (ne_iff_vec_ne_zero _ _).mp hcd⟩ := by
-     have y₃:VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₃, (ne_iff_vec_ne_zero _ _).mp hcd⟩=VecND.toProj ⟨VEC qdr_nd.point₃ qdr_nd.point₄, (ne_iff_vec_ne_zero _ _).mp hcd.symm⟩ := by
+   have l₃' : qdr_nd.edgeND₃₄.toProj=VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₃, ne_iff_vec_ne_zero.mp hcd⟩ := by
+     have y₃:VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₃, ne_iff_vec_ne_zero.mp hcd⟩=VecND.toProj ⟨VEC qdr_nd.point₃ qdr_nd.point₄, ne_iff_vec_ne_zero.mp hcd.symm⟩ := by
        have z₃: VEC qdr_nd.point₄ qdr_nd.point₃ =- VEC qdr_nd.point₃ qdr_nd.point₄ := by
          simp only [neg_vec]
        simp only [ne_eq, z₃, VecND.mk_neg', VecND.neg_toProj]
      simp only [l₃, ne_eq, y₃]
    have l₄ : qdr_nd.edgeND₁₄.toProj=VecND.toProj ⟨VEC qdr_nd.point₁ qdr_nd.point₄, _⟩ := by rfl
-   have l₄' : qdr_nd.edgeND₁₄.toProj=VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₁, (ne_iff_vec_ne_zero _ _).mp had⟩ := by
-     have y₄:VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₁, (ne_iff_vec_ne_zero _ _).mp had⟩=VecND.toProj ⟨VEC qdr_nd.point₁ qdr_nd.point₄, (ne_iff_vec_ne_zero _ _).mp had.symm⟩ := by
+   have l₄' : qdr_nd.edgeND₁₄.toProj=VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₁, ne_iff_vec_ne_zero.mp had⟩ := by
+     have y₄:VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₁, ne_iff_vec_ne_zero.mp had⟩=VecND.toProj ⟨VEC qdr_nd.point₁ qdr_nd.point₄, ne_iff_vec_ne_zero.mp had.symm⟩ := by
        have z₄: VEC qdr_nd.point₄ qdr_nd.point₁ =- VEC qdr_nd.point₁ qdr_nd.point₄ := by
          simp [neg_vec]
        simp only [ne_eq, z₄, VecND.mk_neg', VecND.neg_toProj]
@@ -235,7 +235,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr
      exact x
    have v₁ : qdr_nd.edgeND₁₂.toProj = qdr_nd.edgeND₃₄.toProj := by
      unfold Quadrilateral.IsParallelogram at para
-     have v₁₁₁:VecND.toProj ⟨VEC qdr_nd.point₁ qdr_nd.point₂, (ne_iff_vec_ne_zero _ _).mp hba⟩ = VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₃, (ne_iff_vec_ne_zero _ _).mp hcd⟩ := by
+     have v₁₁₁:VecND.toProj ⟨VEC qdr_nd.point₁ qdr_nd.point₂, ne_iff_vec_ne_zero.mp hba⟩ = VecND.toProj ⟨VEC qdr_nd.point₄ qdr_nd.point₃, ne_iff_vec_ne_zero.mp hcd⟩ := by
        simp only [ne_eq, para]
      simp only [l₁, ne_eq, v₁₁₁, l₃']
    have v₁₁ : toProj qdr_nd.edgeND₁₂ = toProj qdr_nd.edgeND₃₄ := by exact v₁
@@ -471,7 +471,7 @@ theorem qdr_nd_is_prg_nd_of_para_para_not_collinear₁₂₃ (h₁ : qdr_nd.edge
       by_contra is_zero
       rw [is_zero] at l₁
       have not_nd₁₂ : qdr_nd.point₂ = qdr_nd.point₁ := by
-        apply (eq_iff_vec_eq_zero qdr_nd.point₁ qdr_nd.point₂).mpr
+        apply eq_iff_vec_eq_zero.mpr
         rw [l₁]
         exact zero_smul ℝ (VEC qdr_nd.point₂ qdr_nd.point₃)
       exact qdr_nd.nd₁₂.out not_nd₁₂
@@ -513,7 +513,7 @@ theorem qdr_nd_is_prg_nd_of_para_para_not_collinear₁₂₃ (h₁ : qdr_nd.edge
     by_contra is_zero
     rw [is_zero] at l₁
     have not_nd₂₃ : qdr_nd.point₂ = qdr_nd.point₃ := by
-      apply (eq_iff_vec_eq_zero qdr_nd.point₃ qdr_nd.point₂).mpr
+      apply eq_iff_vec_eq_zero.mpr
       rw [l₁]
       exact zero_smul ℝ (VEC qdr_nd.point₁ qdr_nd.point₂)
     exact qdr_nd.nd₂₃.out not_nd₂₃.symm