structure EuclidGeom.Triangle.IsCongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.Triangle P) (tr₂ : EuclidGeom.Triangle P) : Prop

• intro :: (
• edge₁ : tr₁.edge₁.length = tr₂.edge₁.length
• edge₂ : tr₁.edge₂.length = tr₂.edge₂.length
• edge₃ : tr₁.edge₃.length = tr₂.edge₃.length
• angle₁ : if h : tr₁.IsND ∧ tr₂.IsND then { val := tr₁, property := (_ : tr₁.IsND) }.angle₁.value = { val := tr₂, property := (_ : tr₂.IsND) }.angle₁.value else True
• angle₂ : if h : tr₁.IsND ∧ tr₂.IsND then { val := tr₁, property := (_ : tr₁.IsND) }.angle₂.value = { val := tr₂, property := (_ : tr₂.IsND) }.angle₂.value else True
• angle₃ : if h : tr₁.IsND ∧ tr₂.IsND then { val := tr₁, property := (_ : tr₁.IsND) }.angle₃.value = { val := tr₂, property := (_ : tr₂.IsND) }.angle₃.value else True
• )

theorem EuclidGeom.Triangle.IsCongr.nd_of_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsCongr tr₁ tr₂) (nd : tr₁.IsND) : tr₂.IsND

theorem EuclidGeom.Triangle.IsCongr.refl {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : EuclidGeom.Triangle.IsCongr tr tr

theorem EuclidGeom.Triangle.IsCongr.symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsCongr tr₁ tr₂) : EuclidGeom.Triangle.IsCongr tr₂ tr₁

theorem EuclidGeom.Triangle.IsCongr.trans {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} {tr₃ : EuclidGeom.Triangle P} (h₁ : EuclidGeom.Triangle.IsCongr tr₁ tr₂) (h₂ : EuclidGeom.Triangle.IsCongr tr₂ tr₃) : EuclidGeom.Triangle.IsCongr tr₁ tr₃

instance EuclidGeom.Triangle.IsCongr.instHasCongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.HasCongr (EuclidGeom.Triangle P)

Equations

• One or more equations did not get rendered due to their size.

theorem EuclidGeom.Triangle.IsCongr.perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsCongr tr₁ tr₂) : EuclidGeom.Triangle.IsCongr tr₁.perm_vertices tr₂.perm_vertices

theorem EuclidGeom.Triangle.IsCongr.congr_iff_perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.Triangle P) (tr₂ : EuclidGeom.Triangle P) : EuclidGeom.Triangle.IsCongr tr₁ tr₂ ↔ EuclidGeom.Triangle.IsCongr tr₁.perm_vertices tr₂.perm_vertices

theorem EuclidGeom.Triangle.IsCongr.oarea {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsCongr tr₁ tr₂) : tr₁.oarea = tr₂.oarea

theorem EuclidGeom.Triangle.IsCongr.area {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsCongr tr₁ tr₂) : tr₁.area = tr₂.area

structure EuclidGeom.Triangle.IsACongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.Triangle P) (tr₂ : EuclidGeom.Triangle P) : Prop

• intro :: (
• edge₁ : tr₁.edge₁.length = tr₂.edge₁.length
• edge₂ : tr₁.edge₂.length = tr₂.edge₂.length
• edge₃ : tr₁.edge₃.length = tr₂.edge₃.length
• angle₁ : if h : tr₁.IsND ∧ tr₂.IsND then { val := tr₁, property := (_ : tr₁.IsND) }.angle₁.value = -{ val := tr₂, property := (_ : tr₂.IsND) }.angle₁.value else True
• angle₂ : if h : tr₁.IsND ∧ tr₂.IsND then { val := tr₁, property := (_ : tr₁.IsND) }.angle₂.value = -{ val := tr₂, property := (_ : tr₂.IsND) }.angle₂.value else True
• angle₃ : if h : tr₁.IsND ∧ tr₂.IsND then { val := tr₁, property := (_ : tr₁.IsND) }.angle₃.value = -{ val := tr₂, property := (_ : tr₂.IsND) }.angle₃.value else True
• )

theorem EuclidGeom.Triangle.IsACongr.nd_of_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsACongr tr₁ tr₂) (nd : tr₁.IsND) : tr₂.IsND

theorem EuclidGeom.Triangle.IsACongr.symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsACongr tr₁ tr₂) : EuclidGeom.Triangle.IsACongr tr₂ tr₁

instance EuclidGeom.Triangle.IsACongr.instHasACongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.HasACongr (EuclidGeom.Triangle P)

Equations

• One or more equations did not get rendered due to their size.

theorem EuclidGeom.Triangle.IsACongr.perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsACongr tr₁ tr₂) : EuclidGeom.Triangle.IsACongr tr₁.perm_vertices tr₂.perm_vertices

theorem EuclidGeom.Triangle.IsACongr.acongr_iff_perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.Triangle P) (tr₂ : EuclidGeom.Triangle P) : EuclidGeom.Triangle.IsACongr tr₁ tr₂ ↔ EuclidGeom.Triangle.IsACongr tr₁.perm_vertices tr₂.perm_vertices

theorem EuclidGeom.Triangle.IsACongr.oarea {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsACongr tr₁ tr₂) : tr₁.oarea = -tr₂.oarea

theorem EuclidGeom.Triangle.IsACongr.area {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsACongr tr₁ tr₂) : tr₁.area = tr₂.area

theorem EuclidGeom.Triangle.congr_of_acongr_acongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} {tr₃ : EuclidGeom.Triangle P} (h₁ : EuclidGeom.Triangle.IsACongr tr₁ tr₂) (h₂ : EuclidGeom.Triangle.IsACongr tr₂ tr₃) : EuclidGeom.Triangle.IsCongr tr₁ tr₃

theorem EuclidGeom.Triangle.acongr_of_congr_acongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} {tr₃ : EuclidGeom.Triangle P} (h₁ : EuclidGeom.Triangle.IsCongr tr₁ tr₂) (h₂ : EuclidGeom.Triangle.IsACongr tr₂ tr₃) : EuclidGeom.Triangle.IsACongr tr₁ tr₃

theorem EuclidGeom.Triangle.acongr_of_acongr_congr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} {tr₃ : EuclidGeom.Triangle P} (h₁ : EuclidGeom.Triangle.IsACongr tr₁ tr₂) (h₂ : EuclidGeom.Triangle.IsCongr tr₂ tr₃) : EuclidGeom.Triangle.IsACongr tr₁ tr₃

structure EuclidGeom.TriangleND.IsCongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd₁ : EuclidGeom.TriangleND P) (tr_nd₂ : EuclidGeom.TriangleND P) : Prop

• intro :: (
• edge₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length
• edge₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length
• edge₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length
• angle₁ : tr_nd₁.angle₁.value = tr_nd₂.angle₁.value
• angle₂ : tr_nd₁.angle₂.value = tr_nd₂.angle₂.value
• angle₃ : tr_nd₁.angle₃.value = tr_nd₂.angle₃.value
• )

theorem EuclidGeom.TriangleND.IsCongr.refl {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.TriangleND.IsCongr tr_nd tr_nd

theorem EuclidGeom.TriangleND.IsCongr.symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsCongr tr_nd₁ tr_nd₂) : EuclidGeom.TriangleND.IsCongr tr_nd₂ tr_nd₁

theorem EuclidGeom.TriangleND.IsCongr.trans {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} {tr_nd₃ : EuclidGeom.TriangleND P} (h₁ : EuclidGeom.TriangleND.IsCongr tr_nd₁ tr_nd₂) (h₂ : EuclidGeom.TriangleND.IsCongr tr_nd₂ tr_nd₃) : EuclidGeom.TriangleND.IsCongr tr_nd₁ tr_nd₃

instance EuclidGeom.TriangleND.IsCongr.instHasCongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.HasCongr (EuclidGeom.TriangleND P)

Equations

• One or more equations did not get rendered due to their size.

theorem EuclidGeom.TriangleND.IsCongr.is_cclock_of_cclock {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsCongr tr_nd₁ tr_nd₂) (cc : tr_nd₁.is_cclock) : tr_nd₂.is_cclock

theorem EuclidGeom.TriangleND.IsCongr.oarea {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsCongr tr_nd₁ tr_nd₂) : tr_nd₁.oarea = tr_nd₂.oarea

theorem EuclidGeom.TriangleND.IsCongr.area {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsCongr tr_nd₁ tr_nd₂) : tr_nd₁.area = tr_nd₂.area

theorem EuclidGeom.TriangleND.IsCongr.perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsCongr tr_nd₁ tr_nd₂) : EuclidGeom.TriangleND.IsCongr (EuclidGeom.TriangleND.perm_vertices tr_nd₁) (EuclidGeom.TriangleND.perm_vertices tr_nd₂)

theorem EuclidGeom.TriangleND.IsCongr.congr_iff_perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd₁ : EuclidGeom.TriangleND P) (tr_nd₂ : EuclidGeom.TriangleND P) : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₂ ↔ EuclidGeom.HasCongr.congr (EuclidGeom.TriangleND.perm_vertices tr_nd₁) (EuclidGeom.TriangleND.perm_vertices tr_nd₂)

theorem EuclidGeom.TriangleND.IsCongr.unique_of_eq_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsCongr tr_nd₁ tr_nd₂) (p₁ : tr_nd₁.point₁ = tr_nd₂.point₁) (p₂ : tr_nd₁.point₂ = tr_nd₂.point₂) : tr_nd₁.point₃ = tr_nd₂.point₃

structure EuclidGeom.TriangleND.IsACongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd₁ : EuclidGeom.TriangleND P) (tr_nd₂ : EuclidGeom.TriangleND P) : Prop

• intro :: (
• edge₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length
• edge₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length
• edge₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length
• angle₁ : tr_nd₁.angle₁.value = -tr_nd₂.angle₁.value
• angle₂ : tr_nd₁.angle₂.value = -tr_nd₂.angle₂.value
• angle₃ : tr_nd₁.angle₃.value = -tr_nd₂.angle₃.value
• )

theorem EuclidGeom.TriangleND.IsACongr.not_cclock_of_cclock {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsACongr tr_nd₁ tr_nd₂) (cc : tr_nd₁.is_cclock) : ¬tr_nd₂.is_cclock

theorem EuclidGeom.TriangleND.IsACongr.symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsACongr tr_nd₁ tr_nd₂) : EuclidGeom.TriangleND.IsACongr tr_nd₂ tr_nd₁

instance EuclidGeom.TriangleND.IsACongr.instHasACongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.HasACongr (EuclidGeom.TriangleND P)

Equations

• One or more equations did not get rendered due to their size.

theorem EuclidGeom.TriangleND.IsACongr.perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsACongr tr_nd₁ tr_nd₂) : EuclidGeom.TriangleND.IsACongr (EuclidGeom.TriangleND.perm_vertices tr_nd₁) (EuclidGeom.TriangleND.perm_vertices tr_nd₂)

theorem EuclidGeom.TriangleND.IsACongr.acongr_iff_perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd₁ : EuclidGeom.TriangleND P) (tr_nd₂ : EuclidGeom.TriangleND P) : EuclidGeom.TriangleND.IsACongr tr_nd₁ tr_nd₂ ↔ EuclidGeom.TriangleND.IsACongr (EuclidGeom.TriangleND.perm_vertices tr_nd₁) (EuclidGeom.TriangleND.perm_vertices tr_nd₂)

theorem EuclidGeom.TriangleND.IsACongr.oarea {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsACongr tr_nd₁ tr_nd₂) : tr_nd₁.oarea = -tr_nd₂.oarea

theorem EuclidGeom.TriangleND.IsACongr.area {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsACongr tr_nd₁ tr_nd₂) : tr_nd₁.area = tr_nd₂.area

theorem EuclidGeom.TriangleND.congr_of_acongr_acongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} {tr_nd₃ : EuclidGeom.TriangleND P} (h₁ : EuclidGeom.TriangleND.IsACongr tr_nd₁ tr_nd₂) (h₂ : EuclidGeom.TriangleND.IsACongr tr_nd₂ tr_nd₃) : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₃

theorem EuclidGeom.TriangleND.acongr_of_congr_acongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} {tr_nd₃ : EuclidGeom.TriangleND P} (h₁ : EuclidGeom.TriangleND.IsCongr tr_nd₁ tr_nd₂) (h₂ : EuclidGeom.TriangleND.IsACongr tr_nd₂ tr_nd₃) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₃

theorem EuclidGeom.TriangleND.acongr_of_acongr_congr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} {tr_nd₃ : EuclidGeom.TriangleND P} (h₁ : EuclidGeom.TriangleND.IsACongr tr_nd₁ tr_nd₂) (h₂ : EuclidGeom.TriangleND.IsCongr tr_nd₂ tr_nd₃) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₃

theorem EuclidGeom.Triangle.congr_of_congr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₂) : EuclidGeom.HasCongr.congr ↑tr_nd₁ ↑tr_nd₂

theorem EuclidGeom.Triangle.acongr_of_acongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂) : EuclidGeom.HasACongr.acongr ↑tr_nd₁ ↑tr_nd₂

theorem EuclidGeom.Triangle.nd_of_congr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr : EuclidGeom.Triangle P} {tr_nd : EuclidGeom.TriangleND P} (h : EuclidGeom.HasCongr.congr (↑tr_nd) tr) : tr.IsND

theorem EuclidGeom.TriangleND.congr_of_congr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr : EuclidGeom.Triangle P} {tr_nd : EuclidGeom.TriangleND P} (h : EuclidGeom.HasCongr.congr (↑tr_nd) tr) : EuclidGeom.HasCongr.congr tr_nd { val := tr, property := (_ : tr.IsND) }

theorem EuclidGeom.Triangle.IsCongr.not_nd_of_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.HasCongr.congr tr₁ tr₂) (nnd : ¬tr₁.IsND) : ¬tr₂.IsND

theorem EuclidGeom.Triangle.IsACongr.not_nd_of_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsACongr tr₁ tr₂) (nnd : ¬tr₁.IsND) : ¬tr₂.IsND

theorem EuclidGeom.Triangle.not_nd_of_acongr_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsACongr tr tr) : ¬tr.IsND

theorem EuclidGeom.Triangle.acongr_self_of_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr : EuclidGeom.Triangle P} (nnd : ¬tr.IsND) : EuclidGeom.Triangle.IsACongr tr tr

theorem EuclidGeom.Triangle.IsCongr.acongr_of_left_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsCongr tr₁ tr₂) (nnd : ¬tr₁.IsND) : EuclidGeom.Triangle.IsACongr tr₁ tr₂

theorem EuclidGeom.Triangle.IsCongr.acongr_of_right_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsCongr tr₁ tr₂) (nnd : ¬tr₂.IsND) : EuclidGeom.Triangle.IsACongr tr₁ tr₂

theorem EuclidGeom.Triangle.IsACongr.congr_of_left_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsACongr tr₁ tr₂) (nnd : ¬tr₁.IsND) : EuclidGeom.Triangle.IsCongr tr₁ tr₂

theorem EuclidGeom.Triangle.IsACongr.congr_of_right_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsACongr tr₁ tr₂) (nnd : ¬tr₂.IsND) : EuclidGeom.Triangle.IsCongr tr₁ tr₂

theorem EuclidGeom.TriangleND.cosine_eq_of_SSS {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (e₁ : (↑tr_nd₁).edge₁.length = (↑tr_nd₂).edge₁.length) (e₂ : (↑tr_nd₁).edge₂.length = (↑tr_nd₂).edge₂.length) (e₃ : (↑tr_nd₁).edge₃.length = (↑tr_nd₂).edge₃.length) : EuclidGeom.AngValue.cos tr_nd₁.angle₁.value = EuclidGeom.AngValue.cos tr_nd₂.angle₁.value

theorem EuclidGeom.TriangleND.congr_of_SSS_of_eq_orientation {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (e₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length) (e₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length) (c : tr_nd₁.is_cclock ↔ tr_nd₂.is_cclock) : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.acongr_of_SSS_of_ne_orientation {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (e₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length) (e₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length) (c : tr_nd₁.is_cclock = ¬tr_nd₂.is_cclock) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.congr_or_acongr_of_SSS {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (e₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length) (e₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length) : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₂ ∨ EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.congr_of_SAS {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length) (a₁ : tr_nd₁.angle₁.value = tr_nd₂.angle₁.value) (e₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length) : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.acongr_of_SAS {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length) (a₁ : tr_nd₁.angle₁.value = -tr_nd₂.angle₁.value) (e₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.congr_of_ASA {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (a₂ : tr_nd₁.angle₂.value = tr_nd₂.angle₂.value) (e₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) (a₃ : tr_nd₁.angle₃.value = tr_nd₂.angle₃.value) : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.acongr_of_ASA {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (a₂ : tr_nd₁.angle₂.value = -tr_nd₂.angle₂.value) (e₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) (a₃ : tr_nd₁.angle₃.value = -tr_nd₂.angle₃.value) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.congr_of_AAS {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (a₁ : tr_nd₁.angle₁.value = tr_nd₂.angle₁.value) (a₂ : tr_nd₁.angle₂.value = tr_nd₂.angle₂.value) (e₃ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.acongr_of_AAS {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (a₁ : tr_nd₁.angle₁.value = -tr_nd₂.angle₁.value) (a₂ : tr_nd₁.angle₂.value = -tr_nd₂.angle₂.value) (e₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.congr_of_HL {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h₁ : tr_nd₁.angle₁.value = ∠[Real.pi / 2]) (h₂ : tr_nd₂.angle₁.value = ∠[Real.pi / 2]) (e₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length) : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₂

theorem EuclidGeom.TriangleND.acongr_of_HL {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h₁ : tr_nd₁.angle₁.value = ∠[Real.pi / 2]) (h₂ : tr_nd₂.angle₁.value = ∠[-Real.pi / 2]) (e₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂

theorem EuclidGeom.Triangle.congr_of_SSS_of_left_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (e₁ : tr₁.edge₁.length = tr₂.edge₁.length) (e₂ : tr₁.edge₂.length = tr₂.edge₂.length) (e₃ : tr₁.edge₃.length = tr₂.edge₃.length) (nnd : ¬tr₁.IsND) : EuclidGeom.HasCongr.congr tr₁ tr₂

theorem EuclidGeom.Triangle.congr_of_SSS_of_right_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (e₁ : tr₁.edge₁.length = tr₂.edge₁.length) (e₂ : tr₁.edge₂.length = tr₂.edge₂.length) (e₃ : tr₁.edge₃.length = tr₂.edge₃.length) (nnd : ¬tr₂.IsND) : EuclidGeom.HasCongr.congr tr₁ tr₂

theorem EuclidGeom.Triangle.acongr_of_SSS_of_left_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (e₁ : tr₁.edge₁.length = tr₂.edge₁.length) (e₂ : tr₁.edge₂.length = tr₂.edge₂.length) (e₃ : tr₁.edge₃.length = tr₂.edge₃.length) (nnd : ¬tr₁.IsND) : EuclidGeom.HasACongr.acongr tr₁ tr₂

theorem EuclidGeom.Triangle.acongr_of_SSS_of_right_not_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (e₁ : tr₁.edge₁.length = tr₂.edge₁.length) (e₂ : tr₁.edge₂.length = tr₂.edge₂.length) (e₃ : tr₁.edge₃.length = tr₂.edge₃.length) (nnd : ¬tr₂.IsND) : EuclidGeom.HasACongr.acongr tr₁ tr₂

theorem EuclidGeom.Triangle.congr_or_acongr_of_SSS {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (e₁ : tr₁.edge₁.length = tr₂.edge₁.length) (e₂ : tr₁.edge₂.length = tr₂.edge₂.length) (e₃ : tr₁.edge₃.length = tr₂.edge₃.length) : EuclidGeom.HasCongr.congr tr₁ tr₂ ∨ EuclidGeom.HasACongr.acongr tr₁ tr₂