pith. machine review for the scientific record. sign in
theorem proved tactic proof

costCompose_left_cancel

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 496theorem costCompose_left_cancel {a b₁ b₂ : ℝ} (ha : 0 ≤ a)
 497    (h : a ★ b₁ = a ★ b₂) : b₁ = b₂ := by

proof body

Tactic-mode proof.

 498  have hsub : a ★ b₁ - a ★ b₂ = 0 := sub_eq_zero.mpr h
 499  rw [costCompose_sub_left] at hsub
 500  have hcoeff : 2 * a + 2 ≠ 0 := by
 501    linarith
 502  have hdiff : b₁ - b₂ = 0 := by
 503    rcases mul_eq_zero.mp hsub with hzero | hzero
 504    · exact False.elim (hcoeff hzero)
 505    · exact hzero
 506  linarith
 507
 508/-- Right-cancellation follows from commutativity of `★`. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.