theorem
proved
tactic proof
J_eq_iff_eq_or_inv
show as:
view Lean formalization →
formal statement (Lean)
704theorem J_eq_iff_eq_or_inv {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
705 J y = J x ↔ y = x ∨ y = x⁻¹ := by
proof body
Tactic-mode proof.
706 constructor
707 · intro h
708 unfold J Jcost at h
709 have hfrac : y + y⁻¹ = x + x⁻¹ := by linarith
710 have hx0 : x ≠ 0 := ne_of_gt hx
711 have hy0 : y ≠ 0 := ne_of_gt hy
712 field_simp [hx0, hy0] at hfrac
713 have hfactor : (y - x) * (x * y - 1) = 0 := by
714 calc
715 (y - x) * (x * y - 1) = x * y ^ 2 + x - (x ^ 2 * y + y) := by ring
716 _ = 0 := by linarith
717 rcases mul_eq_zero.mp hfactor with hxy | hxy
718 · left
719 linarith
720 · right
721 have hxy1 : x * y = 1 := by linarith
722 calc
723 y = (x⁻¹ * x) * y := by rw [inv_mul_cancel₀ hx0, one_mul]
724 _ = x⁻¹ * (x * y) := by ring
725 _ = x⁻¹ := by rw [hxy1, mul_one]
726 · intro h
727 rcases h with rfl | h
728 · rfl
729 · simpa [h] using (J_reciprocal x hx).symm
730
731/-- The genuine positive domain of the canonical cost algebra. -/