Parallelism_implies_Equal_Alternate_Angles_Corresponding_Angles_and_Supplementary_Interior_Angles

⚠️ Retired — incorrect formalization

The Lean statement below does not express the problem its name refers to, so its Disproved status carries no information about that problem. Do not import it or use it as a dependency.

If two lines cut by a transversal are parallel, then the alternate angles are equal, the corresponding angles are equal, and the interior angles on the same side are supplementary.

Why this node was retired

The posted statement is

theorem … (α β : ℝ) (h_parallel : True) : α = β

The parallelism hypothesis is the placeholder (h_parallel : True), which assumes nothing. What remains is the claim that any two real numbers $\alpha$ and $\beta$ are equal — false, and refuted by taking $\alpha = 0$, $\beta = 1$. Its Disproved status is therefore a statement about the placeholder, not about the geometry: the Euclidean result is true.

No lines, no transversal, and no angle relation occur anywhere in the statement; $\alpha$ and $\beta$ are unconstrained reals with no geometric meaning attached.

What a faithful statement would require

An actual configuration — two lines and a transversal in a Euclidean plane, with a genuine parallelism hypothesis — and angles defined from that configuration, so that the equalities and the supplementary relation can be stated about them.

No corrected replacement node exists yet.