theorem EuclidGeom.isoceles_tri_pts_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tri : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsIsoceles tri) (hne : tri.point₂ ≠ tri.point₃) : tri.point₁ ≠ tri.point₂ ∧ tri.point₁ ≠ tri.point₃

theorem EuclidGeom.is_isoceles_tri_ang_eq_ang_of_tri {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tri : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsIsoceles tri) (hne : tri.point₂ ≠ tri.point₃) : ∠ tri.point₃ tri.point₂ tri.point₁ (_ : tri.point₃ ≠ tri.point₂) (_ : tri.point₁ ≠ tri.point₂) = ∠ tri.point₁ tri.point₃ tri.point₂ (_ : tri.point₁ ≠ tri.point₃) hne

theorem EuclidGeom.ang_acute_of_is_isoceles {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (h : ¬EuclidGeom.Collinear A B C) (isoceles_ABC : EuclidGeom.Triangle.IsIsoceles { point₁ := A, point₂ := B, point₃ := C }) : (ANG C B A (_ : C ≠ B) (_ : A ≠ B)).IsAcu

theorem EuclidGeom.ang_acute_of_is_isoceles_variant {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (h : ¬EuclidGeom.Collinear A B C) (isoceles_ABC : EuclidGeom.Triangle.IsIsoceles { point₁ := A, point₂ := B, point₃ := C }) : (ANG A C B (_ : A ≠ C) (_ : B ≠ C)).IsAcu

theorem EuclidGeom.midpt_eq_perp_foot_of_isIsoceles {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [EuclidGeom.PtNe B C] (h : EuclidGeom.Triangle.IsIsoceles { point₁ := A, point₂ := B, point₃ := C }) : { source := B, target := C }.midpoint = EuclidGeom.perp_foot A (LIN B C)

theorem EuclidGeom.perp_foot_eq_midpt_of_is_isoceles {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (not_collinear_ABC : ¬EuclidGeom.Collinear A B C) (isoceles_ABC : EuclidGeom.Triangle.IsIsoceles { point₁ := A, point₂ := B, point₃ := C }) : EuclidGeom.perp_foot A (LIN B C (_ : C ≠ B)) = { source := B, target := C }.midpoint