eq_id_of_map_two_eq_two

formal source

 868  norm_num at hval
 869
 870/-- Any automorphism that fixes `2` is the identity everywhere. -/
 871theorem eq_id_of_map_two_eq_two (f : JAut) (h2 : f posTwo = posTwo) : f = id := by
 872  apply JAut.ext
 873  intro x
 874  rcases eq_self_or_inv f x with hfx | hfx
 875  · exact hfx
 876  · have hmul : f (posMul posTwo x) = posMul posTwo (posInv x) := by
 877      calc
 878        f (posMul posTwo x) = posMul (f posTwo) (f x) := f.multiplicative posTwo x
 879        _ = posMul posTwo (posInv x) := by rw [h2, hfx]
 880    rcases eq_self_or_inv f (posMul posTwo x) with htx | htx
 881    · have hx1 : x = posOne := (two_mul_inv_eq_two_mul_iff x).mp (hmul.symm.trans htx)
 882      subst x
 883      simpa [id] using hfx
 884    · exact False.elim ((two_mul_inv_ne_inv_two_mul x) (hmul.symm.trans htx))
 885
 886/-- The reciprocal automorphism is genuinely nontrivial. -/
 887theorem reciprocal_ne_id : reciprocal ≠ id := by
 888  intro h
 889  have htwo : reciprocal posTwo = id posTwo := congrArg (fun f : JAut => f posTwo) h
 890  have hval : ((reciprocal posTwo : PosReal) : ℝ) = ((id posTwo : PosReal) : ℝ) :=
 891    congrArg Subtype.val htwo
 892  norm_num [reciprocal, id, posInv, posTwo] at hval
 893
 894/-- Exact classification: every `J`-automorphism is either identity or reciprocal. -/
 895theorem eq_id_or_reciprocal (f : JAut) : f = id ∨ f = reciprocal := by
 896  rcases eq_self_or_inv f posTwo with h2 | h2
 897  · left
 898    exact eq_id_of_map_two_eq_two f h2
 899  · right
 900    have hcomp : comp reciprocal f = id := by
 901      apply eq_id_of_map_two_eq_two