eq_self_or_inv

formal source

 833
 834/-- Pointwise, a `J`-automorphism can only choose the identity branch or the
 835    reciprocal branch. -/
 836theorem eq_self_or_inv (f : JAut) (x : PosReal) :
 837    f x = x ∨ f x = posInv x := by
 838  have hJ : J (f x).1 = J x.1 := f.preserves_cost x
 839  rcases (J_eq_iff_eq_or_inv x.2 (f x).2).mp hJ with h | h
 840  · left
 841    exact Subtype.ext h
 842  · right
 843    exact Subtype.ext h
 844
 845/-- If `2 * x⁻¹ = 2 * x`, positivity forces `x = 1`. -/
 846theorem two_mul_inv_eq_two_mul_iff (x : PosReal) :
 847    posMul posTwo (posInv x) = posMul posTwo x ↔ x = posOne := by
 848  constructor
 849  · intro h
 850    apply Subtype.ext
 851    have hval : (2 : ℝ) * (x : ℝ)⁻¹ = 2 * (x : ℝ) := congrArg Subtype.val h
 852    have hx0 : (x : ℝ) ≠ 0 := ne_of_gt x.2
 853    field_simp [hx0] at hval
 854    have hsq : (x : ℝ) ^ 2 = 1 := by linarith
 855    have hx1 : (x : ℝ) = 1 := by nlinarith [x.2, hsq]
 856    simpa [posOne] using hx1
 857  · intro h
 858    subst x
 859    simp [posMul, posInv, posOne, posTwo]
 860
 861/-- The mixed equation `2 * x⁻¹ = (2x)⁻¹` is impossible on `ℝ_{>0}`. -/
 862theorem two_mul_inv_ne_inv_two_mul (x : PosReal) :
 863    posMul posTwo (posInv x) ≠ posInv (posMul posTwo x) := by
 864  intro h
 865  have hval : (2 : ℝ) * (x : ℝ)⁻¹ = ((2 : ℝ) * (x : ℝ))⁻¹ := congrArg Subtype.val h
 866  have hx0 : (x : ℝ) ≠ 0 := ne_of_gt x.2