mathlib3

637412df - feat(analysis/complex/schwarz): equality case in Schwarz lemma (#15861)

feat(analysis/complex/schwarz): equality case in Schwarz lemma (#15861) This partially addresses one of the TODO items in `analysis/complex/schwarz` by showing the equality case in the main statement of the Schwarz lemma.