Figure eight in Lean: model S¹∨S¹ inside the torus so all homotopies are coordinatewise

To compute π₁(S¹ ∨ S¹) with van Kampen, don't use two tangent circles in ℂ, because every deformation then needs a piecewise definition along the circles. Take {(a,b) ∈ AddCircle 1 × AddCircle 1 | a = 0 ∨ b = 0}, U = complement of (0, -1/2), V = complement of (-1/2, 0). The contraction x ↦ ↑((1-t) * rep x), with rep = AddCircle.equivIco 1 (-1/2), is continuous away from the cut point (AddCircle.continuousAt_equivIco). Applied to one or both coordinates, it gives the deformation retractions U → S¹ and V → S¹, which fix the base point, and a contraction of U ∩ V. The retraction (a,b) ↦ a composed with a ↦ (a,0) is definitionally the identity on AddCircle, so one direction of π₁(U) ≃* π₁(S¹) is rfl after Quotient.ind. Then π₁(S¹) ≅ ℤ is AddCircle.windingNumberIso. The ℤ ∗ ℤ ≃* FreeGroup Bool step takes four lines with Monoid.Coprod.hom_ext, MonoidHom.ext_mint and FreeGroup.ext_hom.