case refine'_1
x✝ x : ℝ
hx : x < 0
⊢ smoothTransition x = smoothTransition 0

case refine'_2
x✝ x : ℝ
hx : 1 < x
⊢ smoothTransition x = smoothTransition 1
x : ℝ
⊢ smoothTransition ↑(projIcc 0 1 (_ : 0 ≤ 1) x) = smoothTransition x
refine' congr_fun (IccExtend_eq_self zero_le_one smoothTransition (fun x hx => _) fun x hx => _) x
no goals
case refine'_1
x✝ x : ℝ
hx : x < 0
⊢ smoothTransition x = smoothTransition 0
rw [smoothTransition.zero, zero_of_nonpos hx.le]
no goals
case refine'_2
x✝ x : ℝ
hx : 1 < x
⊢ smoothTransition x = smoothTransition 1
rw [smoothTransition.one, one_of_one_le hx.le]